PublishedMatrixUltraproduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The published varying finite-matrix ultraproduct

Popa, Independence properties in subalgebras of ultraproduct II1 factors, J. Funct. Anal. 266 (2014), §1.6, printed pp. 7–8 (arXiv:1308.3982v3), recalls the bounded-product quotient and its canonical trace. For finite factors of dimension tending to infinity, the result is a II1 factor. Here the coordinates are precisely M_n(M_(j+1)(C)), the only varying product used in the application.

structure OAI.KadisonKastler.FiniteMatrixUltraproduct line 30
Source documentation
The represented quotient of the particular finite-matrix sequence. Only its operator-algebra structure and the canonical trace formula are assumed; no independent unitary or controlled representative is a field.
```
structure FiniteMatrixUltraproduct (n : ℕ) [NeZero n] (ω : Ultrafilter ℕ) where
…
```
def OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct line 47
Source documentation
Popa §1.6 specialized to the increasing finite matrix coordinates.
```
def PublishedFiniteMatrixUltraproduct : Prop :=
…
```
def OAI.KadisonKastler.FiniteMatrixUltraproduct.traceQuotient line 53
Source documentation
The trace quotient interface used by the constructed coordinate embedding into the original factor ultrapower.
```
def FiniteMatrixUltraproduct.traceQuotient {n : ℕ} [NeZero n] {ω : Ultrafilter ℕ}
    (Q : FiniteMatrixUltraproduct n ω) :
    VaryingTraceQuotient (finiteMatrixModelTrace n) (concreteFactorTrace Q.factor) ω where
…
```
Mentions: OAI.KadisonKastler.FiniteMatrixUltraproduct, OAI.KadisonKastler.VaryingTraceQuotient, OAI.KadisonKastler.finiteMatrixModelTrace, OAI.KadisonKastler.concreteFactorTrace