MatrixUltrapower.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Entrywise identification of matrix tracial ultrapowers

Two surjective trace quotients of the same bounded-sequence algebra have identical kernels, by faithfulness of their traces. Applying this to the entrywise matrix quotient gives the finite-matrix ultrapower identity.

theorem OAI.KadisonKastler.TraceQuotientMap.same_source_trace line 28
theorem OAI.KadisonKastler.TraceQuotientMap.same_source_kernel line 32
def OAI.KadisonKastler.TraceQuotientMap.comparison line 40
Source documentation
The canonical comparison between faithful trace quotients of the same bounded-sequence algebra.
```
def comparison : B →⋆ₐ[ℂ] C :=
…
```
theorem OAI.KadisonKastler.TraceQuotientMap.comparison_quotient line 44
theorem OAI.KadisonKastler.TraceQuotientMap.comparison_trace line 48
theorem OAI.KadisonKastler.TraceQuotientMap.comparison_bijective line 54
def OAI.KadisonKastler.TraceQuotientMap.comparisonEquiv line 62
Source documentation
Uniqueness, up to a trace-preserving star equivalence, of faithful tracial quotients with the same coordinate trace formula.
```
def comparisonEquiv : B ≃⋆ₐ[ℂ] C :=
…
```
theorem OAI.KadisonKastler.TraceQuotientMap.comparisonEquiv_quotient line 66
theorem OAI.KadisonKastler.TraceQuotientMap.comparisonEquiv_trace line 70
def OAI.KadisonKastler.matrixUltrapowerEquiv line 85
Source documentation
The represented quotient of matrices is the matrix algebra over the scalar represented quotient, with its normalized matrix trace.
```
def matrixUltrapowerEquiv (Q : TraceQuotientMap τ σ ω)
    (P : TraceQuotientMap (matrixTrace (ι := ι) τ) ρ ω) :
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixTrace
theorem OAI.KadisonKastler.matrixUltrapowerEquiv_quotient line 91
theorem OAI.KadisonKastler.matrixUltrapowerEquiv_trace line 100
theorem OAI.KadisonKastler.matrixUltrapowerEquiv_constant line 107
Source documentation
Scalar matrix entries descend to the same constant entries under the matrix-ultrapower identification.
```
theorem matrixUltrapowerEquiv_constant (Q : TraceQuotientMap τ σ ω)
    (P : TraceQuotientMap (matrixTrace (ι := ι) τ) ρ ω)
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixTrace