OAI/Analysis/KadisonKastler/MatrixQuotientLifts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Diagonal unitary lifts for concretely represented matrix ultrapowers

  1. def OAI.KadisonKastler.TraceQuotientMap.matrixSource line 25

    Source documentation

    Present the concrete matrix quotient as a quotient of abstract C⋆-matrices.

    def TraceQuotientMap.matrixSource
    (R : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω) :
…

    Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace

  2. theorem OAI.KadisonKastler.TraceQuotientMap.matrixSource_scalar line 31

    Source documentation

    The change of representation fixes every constant scalar matrix.

    theorem TraceQuotientMap.matrixSource_scalar
    (R : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…

    Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace

  3. theorem OAI.KadisonKastler.exists_concrete_scalar_commutant_lift line 47

    Source documentation

    A quotient unitary in the scalar-matrix commutant has a concrete bounded diagonal-unitary lift with coefficients in the original factor.

    theorem exists_concrete_scalar_commutant_lift
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (Qbase : TraceQuotientMap τ σbase ω)
    (R : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…

    Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace