OAI/Analysis/BoundedHochschild/AbelianSupportEquivalence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Abelian projections with the same central support are equivalent.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.central_initial_zero_iff_final_zero line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport.partialIso line 34
  3. theorem OAI.BoundedHochschild.KadisonRingrose.abelian_subprojection_central_cut line 49

    Source documentation

    Each subprojection of an abelian projection is a central cut of it.

    theorem abelian_subprojection_central_cut (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p q : M} (hp : AbelianProjection p) (hq : IsStarProjection q) (hqp : q ≤ p) :
    ∃ c : M, CentralProjection c ∧ c * p = q := by
…
  4. theorem OAI.BoundedHochschild.KadisonRingrose.abelian_equivalent_of_central_support line 64

    Source documentation

    Full abelian projections over the same central support are equivalent.

    theorem abelian_equivalent_of_central_support (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p q z : M} (hp : AbelianProjection p) (hq : AbelianProjection q)
    (hpz : IsCentralSupport p z) (hqz : IsCentralSupport q z) :
    ∃ v : PartialIso M, v.initial = p ∧ v.final = q := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.IsCentralSupport