FiniteMatrixFreeModel.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A free Haar unitary with finite-matrix representatives

This is the first stage of the controlled-lift construction. The scalar matrix base is embedded in the varying product, the published independence identity produces the free unitary, and finite polar decomposition gives actual unitary representatives at every coordinate.

def OAI.KadisonKastler.varyingSequenceHom line 25
Source documentation
A uniformly contractive family of star homomorphisms defines a homomorphism into the bounded varying product.
```
def varyingSequenceHom (φ : ∀ j, A →⋆ₐ[ℂ] B j) : A →⋆ₐ[ℂ] VaryingBoundedSequence B where
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence
theorem OAI.KadisonKastler.varyingSequenceHom_apply line 37
instance OAI.KadisonKastler.freeMatrixModelCStar line 42
instance OAI.KadisonKastler.freeMatrixSequenceCStar line 43
instance OAI.KadisonKastler.freeMatrixSequenceStarRing line 45
def OAI.KadisonKastler.finiteMatrixScalarSequence line 61
Source documentation
The same outer scalar matrix is inserted in every finite coordinate.
```
def finiteMatrixScalarSequence :
    CStarMatrix (Fin n) (Fin n) ℂ →⋆ₐ[ℂ] VaryingBoundedSequence (FiniteMatrixModel n) :=
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel
def OAI.KadisonKastler.FiniteMatrixUltraproduct.scalarHom line 66
theorem OAI.KadisonKastler.FiniteMatrixUltraproduct.exists_freeHaar_lift line 72
Source documentation
The first model unitary is free from the scalar outer matrices and has genuine finite-matrix unitary representatives.
```
theorem FiniteMatrixUltraproduct.exists_freeHaar_lift
    (Q : FiniteMatrixUltraproduct n ω)
    (hind : FiniteBaseIndependence (concreteFactorTrace Q.factor)) :
    ∃ v : unitary (VaryingBoundedSequence (FiniteMatrixModel n)),
      FreeHaarMoments (concreteFactorTrace Q.factor) Q.scalarHom.range
        (Unitary.map (StarMonoidHom.ofClass Q.quotient) v) := by
…
```
Mentions: OAI.KadisonKastler.FiniteMatrixUltraproduct, OAI.KadisonKastler.FiniteBaseIndependence, OAI.KadisonKastler.concreteFactorTrace, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.FreeHaarMoments