TracialDecomposition.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedHochschild.KadisonRingrose.unitCornerEquiv line 20
Source documentation
The unit corner is canonically the original algebra.
```
def unitCornerEquiv : Corner (1 : M) (IsStarProjection.one M) ≃⋆ₐ[ℂ] M where
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.unitCornerEquiv_apply line 31

lemma OAI.BoundedHochschild.KadisonRingrose.noAbelianCorners_of_equiv line 35

Source documentation

Absence of abelian corners is invariant under a star algebra equivalence.

lemma noAbelianCorners_of_equiv
    {N : Type u} [CStarAlgebra N] [PartialOrder N] [StarOrderedRing N]
    (φ : N ≃⋆ₐ[ℂ] M) (hM : PopaTypeII.NoAbelianCorners M) :
    PopaTypeII.NoAbelianCorners N := by
…

Mentions: OAI.PopaTypeII.NoAbelianCorners

def OAI.BoundedHochschild.KadisonRingrose.unitCornerTrace line 76
Source documentation
The original trace restricted along the canonical unit-corner equivalence.
```
def unitCornerTrace : Corner (1 : M) (IsStarProjection.one M) →ₚ[ℂ] ℂ where
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.unitCornerTrace_apply line 81
lemma OAI.BoundedHochschild.KadisonRingrose.unitCornerTrace_normal line 84
theorem OAI.BoundedHochschild.KadisonRingrose.tracialTypeII_unitCorner line 93
Source documentation
All data required by the tracial primitive theorem survives passing to the unit corner.
```
theorem tracialTypeII_unitCorner
    (hτ : TraceInPredual e τ) (htr : ∀ a b : M, τ (a * b) = τ (b * a))
    (hfaith : ∀ a : M, τ (star a * a) = 0 → a = 0) (h1 : τ 1 = 1)
    (hII : PopaTypeII.NoTypeICentralPart M) :
    TracialTypeII (Corner (1 : M) (IsStarProjection.one M)) := by
…
```
Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.PopaTypeII.NoTypeICentralPart, OAI.BoundedHochschild.KadisonRingrose.TracialTypeII
lemma OAI.BoundedHochschild.KadisonRingrose.zeroCorner_subsingleton line 119
Source documentation
Every element of the zero corner is zero.
```
lemma zeroCorner_subsingleton : Subsingleton (Corner (0 : M) (IsStarProjection.zero M)) := by
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.zeroCorner_noTypeII1Summand line 126
Source documentation
The zero corner cannot contain a nonzero type II₁ central summand.
```
lemma zeroCorner_noTypeII1Summand :
    NoTypeII1Summand (Corner (0 : M) (IsStarProjection.zero M)) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoTypeII1Summand
theorem OAI.BoundedHochschild.KadisonRingrose.centralDecompositionInput_of_tracialTypeII line 132