MatrixUnitsExistence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Full matrix subalgebras of every finite size in a II₁ factor

The existing continuous-dimension construction gives an equivalent partition of the identity of every positive finite size. Its displayed partial-isometry legs give the required actual matrix units.

theorem OAI.KadisonKastler.exists_matrixUnits_of_size line 21
Source documentation
Every positive finite matrix size occurs unitally inside the factor.
```
theorem exists_matrixUnits_of_size (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (k : ℕ) (hk : 0 < k) :
    Nonempty (Generator.MatrixUnitSystem (Fin k) (Algebra M)) := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.factorMatrixUnits line 38
Source documentation
Fixed choices of the (j+1)-dimensional coordinate matrix algebras.
```
def factorMatrixUnits (hM : Generator.IsII1Factor M.toStarSubalgebra) (j : ℕ) :
    Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M) :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.factorMatrixUnits_trace_diagonal line 43
Source documentation
Every diagonal coordinate has the required normalized trace.
```
theorem factorMatrixUnits_trace_diagonal (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τ : FaithfulTracialState (Algebra M)) (j : ℕ) (i : Fin (j + 1)) :
    τ.toLinearMap ((factorMatrixUnits hM j).entry i i) = ((j + 1 : ℕ) : ℂ)⁻¹ := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.factorMatrixUnits