FiniteModelEmbedding.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Embedding the finite free model in the factor ultrapower

Coordinate matrix units preserve the trace and the outer scalar matrix copy. Their induced quotient embedding therefore carries the first free Haar model to the desired ultrapower, retaining its finite representatives.

def OAI.KadisonKastler.concreteScalarMatrixHom line 27
Source documentation
The concrete constant outer scalar matrix copy.
```
def concreteScalarMatrixHom : CStarMatrix (Fin n) (Fin n) ℂ →⋆ₐ[ℂ]
    Algebra (matrixVonNeumann (ι := Fin n) M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.FiniteMatrixUltraproduct.modelEmbedding line 35
theorem OAI.KadisonKastler.FiniteMatrixUltraproduct.modelEmbedding_trace line 39
theorem OAI.KadisonKastler.FiniteMatrixUltraproduct.modelEmbedding_scalar line 46
Source documentation
The quotient embedding fixes the entire scalar matrix base.
```
theorem FiniteMatrixUltraproduct.modelEmbedding_scalar
    (a : CStarMatrix (Fin n) (Fin n) ℂ) :
    Q.modelEmbedding τ R E (Q.scalarHom a) = R.constant (concreteScalarMatrixHom (M := M) a) := by
…
```
Mentions: OAI.KadisonKastler.concreteScalarMatrixHom
theorem OAI.KadisonKastler.modelEmbedding_base line 59
theorem OAI.KadisonKastler.FiniteMatrixUltraproduct.exists_embedded_freeHaar_lift line 67
Source documentation
The embedded free model retains its coordinate finite-matrix lifts.
```
theorem FiniteMatrixUltraproduct.exists_embedded_freeHaar_lift
    (hind : FiniteBaseIndependence (concreteFactorTrace Q.factor)) :
    ∃ v : unitary (VaryingBoundedSequence (FiniteMatrixModel n)),
      FreeHaarMoments σ
        (R.constant.comp (concreteScalarMatrixHom (M := M) (n := n))).range
…
```
Mentions: OAI.KadisonKastler.FiniteBaseIndependence, OAI.KadisonKastler.concreteFactorTrace, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.concreteScalarMatrixHom