OAI/Analysis/BoundedHochschild/AbelianCentralSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Central support and comparison of abelian projections for type I reduction.

  1. def OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport line 22

    Source documentation

    The central support of a projection, expressed by its central annihilators.

    def IsCentralSupport (p z : M) : Prop :=
…
  2. theorem OAI.BoundedHochschild.KadisonRingrose.exists_central_support line 26
  3. theorem OAI.BoundedHochschild.KadisonRingrose.central_support_full line 61
  4. theorem OAI.BoundedHochschild.KadisonRingrose.trace_free_abelian_subequivalent line 78