CentralTypeIIInheritance.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Type II inheritance by central corners

An abelian subcorner remains abelian in the ambient algebra. Consequently the type I condition on a corner lifts to its ambient projection, and absence of a type I central part passes to central corners. No trace is used.

lemma OAI.BoundedHochschild.KadisonRingrose.abelianProjection_corner_to_ambient line 25

Source documentation

Abelianness of a projection in a corner is its ambient abelianness.

lemma abelianProjection_corner_to_ambient {p : M} (hp : IsStarProjection p)
    (q : Corner p hp) (hq : IsStarProjection q)
    (hab : PopaTypeII.AbelianProjection hq) :
    PopaTypeII.AbelianProjection (corner_projection_coe p hp hq) := by
…

Mentions: OAI.PopaTypeII.AbelianProjection

lemma OAI.BoundedHochschild.KadisonRingrose.typeICorner_corner_to_ambient line 46

Source documentation

A type I corner of a corner is type I at its ambient projection.

lemma typeICorner_corner_to_ambient {p : M} (hp : IsStarProjection p)
    (z : Corner p hp) (hz : IsStarProjection z)
    (hI : PopaTypeII.TypeICorner hz) :
    PopaTypeII.TypeICorner (corner_projection_coe p hp hz) := by
…

Mentions: OAI.PopaTypeII.TypeICorner

theorem OAI.BoundedHochschild.KadisonRingrose.noTypeICentralPart_centralCorner line 63

Source documentation

The absence of a type I central part passes to a central corner.

theorem noTypeICentralPart_centralCorner {p : M} (hp : IsStarProjection p)
    (hc : ∀ a : M, p * a = a * p)
    (hM : PopaTypeII.NoTypeICentralPart M) :
    PopaTypeII.NoTypeICentralPart (Corner p hp) := by
…

Mentions: OAI.PopaTypeII.NoTypeICentralPart

theorem OAI.BoundedHochschild.KadisonRingrose.noTypeICentralPart_smaller_centralCorner line 76
Source documentation
A smaller ambient central corner inherits the type II condition from a larger corner. Centrality of the larger projection is not needed.
```
theorem noTypeICentralPart_smaller_centralCorner {p q : M}
    (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p ≤ q)
    (hcp : ∀ a : M, p * a = a * p)
    (hQ : PopaTypeII.NoTypeICentralPart (Corner q hq)) :
    PopaTypeII.NoTypeICentralPart (Corner p hp) := by
…
```
Mentions: OAI.PopaTypeII.NoTypeICentralPart

theorem OAI.BoundedHochschild.KadisonRingrose.noTypeICentralPart_centralCorner_mono line 91

Source documentation

Central-corner inheritance with both ambient centrality witnesses.

theorem noTypeICentralPart_centralCorner_mono {p q : M}
    (hp : IsStarProjection p) (hq : IsStarProjection q)
    (hcp : ∀ a : M, p * a = a * p) (_hcq : ∀ a : M, q * a = a * q)
    (hpq : p ≤ q) (hQ : PopaTypeII.NoTypeICentralPart (Corner q hq)) :
    PopaTypeII.NoTypeICentralPart (Corner p hp) :=
…

Mentions: OAI.PopaTypeII.NoTypeICentralPart