TypeICentralDecomposition.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The central type I cut

Central type I summands are closed under chain suprema and orthogonal sums. A maximal one therefore has a complementary corner with no abelian projections, and in particular no type I central part. All constructions use the given predual and require no trace.

lemma OAI.BoundedHochschild.KadisonRingrose.typeICentral_witness line 30

Source documentation

A central projection meeting a type I summand contains an abelian projection.

lemma typeICentral_witness {p c : M} (hp : TypeICentralSummand p)
    (hc : CentralProjection c) (hzero : c * p ≠ 0) :
    ∃ a : M, AbelianProjection a ∧ a ≤ c ∧ a ≠ 0 := by
…

lemma OAI.BoundedHochschild.KadisonRingrose.typeICentral_chain_sup line 42
lemma OAI.BoundedHochschild.KadisonRingrose.typeICentral_orthogonal_sum line 59

theorem OAI.BoundedHochschild.KadisonRingrose.exists_maximal_typeI_central_cut line 76

Source documentation

There is a maximal central type I summand.

theorem exists_maximal_typeI_central_cut (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    ∃ p : M, TypeICentralSummand p ∧
      ∀ q : M, TypeICentralSummand q → q ≤ 1 - p → q = 0 := by
…

lemma OAI.BoundedHochschild.KadisonRingrose.finitePath_abelian_of_popa line 100
Source documentation
The two corner formulations of an abelian projection agree in the direction needed here.
```
lemma finitePath_abelian_of_popa {p : M} (hp : IsStarProjection p)
    (h : PopaTypeII.AbelianProjection hp) : AbelianProjection p := by
…
```
Mentions: OAI.PopaTypeII.AbelianProjection

lemma OAI.BoundedHochschild.KadisonRingrose.centralCorner_abelian_to_ambient line 109

Source documentation

An abelian projection in a central corner is abelian in the ambient algebra.

lemma centralCorner_abelian_to_ambient {p : M} (hp : IsStarProjection p)
    (hc : ∀ a : M, p * a = a * p) (q : Corner p hp)
    (hq : AbelianProjection q) : AbelianProjection (q : M) := by
…

lemma OAI.BoundedHochschild.KadisonRingrose.centralCorner_typeI_to_ambient line 127

Source documentation

A central type I summand of a central corner remains type I in the ambient algebra.

lemma centralCorner_typeI_to_ambient {p : M} (hp : IsStarProjection p)
    (hc : ∀ a : M, p * a = a * p) (q : Corner p hp)
    (hq : TypeICentralSummand q) : TypeICentralSummand (q : M) := by
…

theorem OAI.BoundedHochschild.KadisonRingrose.exists_typeI_central_cut line 153

Source documentation

The complement of a maximal type I cut has no nonzero abelian corner.

theorem exists_typeI_central_cut (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    ∃ (p : M) (hp : IsStarProjection p), (∀ a : M, p * a = a * p) ∧
      TypeICentralSummand p ∧
      PopaTypeII.NoAbelianCorners (Corner (1 - p) hp.one_sub) ∧
      PopaTypeII.NoTypeICentralPart (Corner (1 - p) hp.one_sub) := by
…

Mentions: OAI.PopaTypeII.NoAbelianCorners, OAI.PopaTypeII.NoTypeICentralPart