PartialIsoCornerEquivalence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Equivalence of corners joined by a partial isometry

Conjugation by a partial isometry identifies its initial and final corners as actual star algebras. In particular abelianness passes between these corners and to smaller projections.

def OAI.BoundedHochschild.KadisonRingrose.partialIsoCornerEquiv line 23
Source documentation
Conjugation identifies the initial and final corners of a partial isometry.
```
def partialIsoCornerEquiv (v : PartialIso M) :
    PopaCorner.algebra v.initial_proj ≃⋆ₐ[ℂ] PopaCorner.algebra v.final_proj where
…
```
Mentions: OAI.PopaCorner.algebra
lemma OAI.BoundedHochschild.KadisonRingrose.partialIsoCornerEquiv_apply line 79
lemma OAI.BoundedHochschild.KadisonRingrose.abelianProjection_partialIso line 85
Source documentation
Equivalent projections have simultaneously abelian corners.
```
lemma abelianProjection_partialIso (v : PartialIso M)
    (hab : PopaTypeII.AbelianProjection v.initial_proj) :
    PopaTypeII.AbelianProjection v.final_proj := by
…
```
Mentions: OAI.PopaTypeII.AbelianProjection

lemma OAI.BoundedHochschild.KadisonRingrose.abelian_projection_mono line 93

Source documentation

A subprojection of an abelian projection is abelian.

lemma abelian_projection_mono {p q : M} (hp : IsStarProjection p)
    (hq : IsStarProjection q) (hqp : q ≤ p)
    (hab : PopaTypeII.AbelianProjection hp) : PopaTypeII.AbelianProjection hq := by
…

Mentions: OAI.PopaTypeII.AbelianProjection