FiniteCentralDecomposition.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The maximal finite central cut, constructed without an assumed trace.

def OAI.BoundedHochschild.KadisonRingrose.FiniteCorner line 19
Source documentation
Finiteness of a corner, expressed in the ambient algebra.
```
def FiniteCorner (p : M) : Prop :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_iff line 23
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_zero line 34
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_of_finiteAlgebra line 40
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_compressed_final line 63
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_orthogonal_sum line 78
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_chain_sup line 92
theorem OAI.BoundedHochschild.KadisonRingrose.exists_maximal_finite_central_cut line 112
Source documentation
Every W*-algebra has a finite central cut with no finite central subprojection in its complement. This part of the classical type decomposition needs no trace.
```
theorem exists_maximal_finite_central_cut (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    ∃ p : M, IsStarProjection p ∧ (∀ a : M, p * a = a * p) ∧ FiniteCorner p ∧
      ∀ q : M, IsStarProjection q → (∀ a : M, q * a = a * q) →
        FiniteCorner q → q ≤ 1 - p → q = 0 := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner
lemma OAI.BoundedHochschild.KadisonRingrose.centralCorner_central line 140
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_trans line 155
lemma OAI.BoundedHochschild.KadisonRingrose.finiteCorner_mono line 172
Source documentation
Finiteness passes to every subprojection, without a centrality hypothesis.
```
lemma finiteCorner_mono {p q : M} (hp : IsStarProjection p)
    (hq : IsStarProjection q) (hpq : p ≤ q) (hfinite : FiniteCorner q) :
    FiniteCorner p := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner
theorem OAI.BoundedHochschild.KadisonRingrose.exists_finite_central_cut_noTypeII1 line 183
Source documentation
The complementary corner of a maximal finite central cut has no II₁ summand.
```
theorem exists_finite_central_cut_noTypeII1 (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    ∃ (p : M) (hp : IsStarProjection p), (∀ a : M, p * a = a * p) ∧
      FiniteAlgebra (HochschildCorners.Corner p hp) ∧
      NoTypeII1Summand (HochschildCorners.Corner (1 - p) hp.one_sub) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.HochschildCorners.Corner, OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand