CentralColumnCuts.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extracting homogeneous central pieces from finite column families.

theorem OAI.BoundedHochschild.KadisonRingrose.homogeneousCorner_of_annihilated_residual line 21

Source documentation

If a central cut annihilates the residual of a finite abelian column family, the cut is a finite homogeneous type I summand.

theorem homogeneousCorner_of_annihilated_residual {p z : M} (hp : AbelianProjection p)
    (hz : CentralProjection z) (hz0 : z ≠ 0) {n : ℕ}
    (v : Fin n → PartialIso M) (hi : ∀ i, (v i).initial = p)
    (ho : ∀ i j, i ≠ j → (v i).final * (v j).final = 0)
    (hann : z * (1 - ∑ i, (v i).final) = 0) : HomogeneousTypeICorner z := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.HomogeneousTypeICorner