CornerEquivalences.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Structural transport for actual corners and algebra equivalences

Nested corners flatten to the corresponding ambient corner. Type I corners and the absence of a type I central part are invariant under an actual star algebra equivalence. These facts are algebraic and require no trace.

def OAI.BoundedHochschild.KadisonRingrose.nestedCornerEquiv line 24

Source documentation

A corner within a corner is the corner of its ambient projection.

def nestedCornerEquiv {p : M} (hp : IsStarProjection p)
    (q : Corner p hp) (hq : IsStarProjection q) :
    Corner q hq ≃⋆ₐ[ℂ] Corner (q : M) (corner_projection_coe p hp hq) where
…

lemma OAI.BoundedHochschild.KadisonRingrose.nestedCornerEquiv_apply line 46
def OAI.BoundedHochschild.KadisonRingrose.popaCornerEquiv line 58
Source documentation
An algebra equivalence induces an equivalence between corresponding corners.
```
def popaCornerEquiv (φ : M ≃⋆ₐ[ℂ] N) {p : M} (hp : IsStarProjection p) :
    PopaCorner.algebra hp ≃⋆ₐ[ℂ] PopaCorner.algebra (hp.map φ) where
…
```
Mentions: OAI.PopaCorner.algebra
lemma OAI.BoundedHochschild.KadisonRingrose.abelianProjection_map_equiv line 84
Source documentation
Abelianness of a projection is transported by a star algebra equivalence.
```
lemma abelianProjection_map_equiv (φ : M ≃⋆ₐ[ℂ] N) {p : M}
    (hp : IsStarProjection p) (hab : PopaTypeII.AbelianProjection hp) :
    PopaTypeII.AbelianProjection (hp.map φ) := by
…
```
Mentions: OAI.PopaTypeII.AbelianProjection
lemma OAI.BoundedHochschild.KadisonRingrose.typeICorner_map_equiv line 92
Source documentation
The type I condition is invariant under changing the algebra presentation.
```
lemma typeICorner_map_equiv (φ : M ≃⋆ₐ[ℂ] N) {z : M}
    (hz : IsStarProjection z) (hI : PopaTypeII.TypeICorner hz) :
    PopaTypeII.TypeICorner (hz.map φ) := by
…
```
Mentions: OAI.PopaTypeII.TypeICorner
theorem OAI.BoundedHochschild.KadisonRingrose.noTypeICentralPart_map_equiv line 111
Source documentation
Absence of a type I central part needs no trace for transport.
```
theorem noTypeICentralPart_map_equiv (φ : M ≃⋆ₐ[ℂ] N)
    (hM : PopaTypeII.NoTypeICentralPart M) : PopaTypeII.NoTypeICentralPart N := by
…
```
Mentions: OAI.PopaTypeII.NoTypeICentralPart
theorem OAI.BoundedHochschild.KadisonRingrose.noTypeICentralPart_equiv line 128
Source documentation
The type I central condition is a property of the star algebra.
```
theorem noTypeICentralPart_equiv (φ : M ≃⋆ₐ[ℂ] N) :
    PopaTypeII.NoTypeICentralPart M ↔ PopaTypeII.NoTypeICentralPart N :=
…
```
Mentions: OAI.PopaTypeII.NoTypeICentralPart