AbelianTypeI.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Type I structure of abelian algebras

Every projection in an abelian C⋆-algebra has a commutative corner. Therefore an abelian algebra, as well as each of its central corners, has no nonzero type II₁ summand. This verifies the structural hypothesis of the classical vanishing input for the abelian case.

instance OAI.BoundedHochschild.KadisonRingrose.commutativeCorner line 24
Source documentation
A corner of a commutative C⋆-algebra is commutative.
```
instance commutativeCorner (p : M) (hp : IsStarProjection p) :
    CommCStarAlgebra (Corner p hp) where
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.abelian_projection line 30
Source documentation
Every projection in a commutative algebra is abelian.
```
lemma abelian_projection {p : M} (hp : IsStarProjection p) :
    PopaTypeII.AbelianProjection hp := by
…
```
Mentions: OAI.PopaTypeII.AbelianProjection
lemma OAI.BoundedHochschild.KadisonRingrose.abelian_typeICorner line 37
Source documentation
Every projection in a commutative algebra has a type I corner.
```
lemma abelian_typeICorner {z : M} (hz : IsStarProjection z) :
    PopaTypeII.TypeICorner hz := by
…
```
Mentions: OAI.PopaTypeII.TypeICorner
theorem OAI.BoundedHochschild.KadisonRingrose.abelian_noTypeII1Summand line 43
Source documentation
A commutative C⋆-algebra has no type II₁ central summand.
```
theorem abelian_noTypeII1Summand : NoTypeII1Summand M := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand