MatrixCommutantLifts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Unitary lifts respecting the scalar matrix commutant

The matrix ultrapower equivalence identifies the scalar-matrix commutant with the diagonal coefficient quotient. The proved coordinatewise finite polar construction then gives a lift which is diagonal at every coordinate.

def OAI.KadisonKastler.sequenceScalarHom line 32
Source documentation
Diagonal amplification of a bounded sequence, as an actual star homomorphism.
```
def sequenceScalarHom : BoundedSequence A →⋆ₐ[ℂ] BoundedSequence (CStarMatrix ι ι A) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.sequenceScalarHom_apply line 36
theorem OAI.KadisonKastler.matrixUltrapowerEquiv_sequenceScalar line 51
theorem OAI.KadisonKastler.matrixUltrapowerEquiv_scalarMatrix line 74
Source documentation
The matrix-ultrapower identification fixes the scalar matrix copy.
```
theorem matrixUltrapowerEquiv_scalarMatrix (Q : TraceQuotientMap τ σ ω)
    (P : TraceQuotientMap (matrixTrace (ι := ι) τ) ρ ω) (s : CStarMatrix ι ι ℂ) :
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixTrace
theorem OAI.KadisonKastler.exists_scalar_commutant_unitary_lift line 96
Source documentation
A unitary commuting with the constant scalar matrices has unitary representatives commuting with those matrices at every coordinate.
```
theorem exists_scalar_commutant_unitary_lift
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (Q : TraceQuotientMap τM σ ω)
    (P : TraceQuotientMap (matrixTrace (ι := ι) τM) ρ ω)
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixTrace