OAI/Analysis/KadisonKastler/MatrixEmbedding.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.matrixUnitsEmbedding line 20

   Source documentation

   The existing algebraic matrix-unit representation with the C⋆-matrix domain.

   def matrixUnitsEmbedding (E : Generator.MatrixUnitSystem ι A) : CStarMatrix ι ι ℂ →⋆ₐ[ℂ] A :=
   …

   Mentions: OAI.Generator.MatrixUnitSystem

2. theorem OAI.KadisonKastler.matrixUnitsEmbedding_apply line 23
3. theorem OAI.KadisonKastler.matrixUnitsEmbedding_single line 27
4. theorem OAI.KadisonKastler.matrixUnitsEmbedding_injective line 34
5. theorem OAI.KadisonKastler.norm_matrixUnitsEmbedding line 39
6. theorem OAI.KadisonKastler.matrixUnits_trace_diagonal line 44
7. theorem OAI.KadisonKastler.matrixUnits_trace_offDiagonal line 58
8. theorem OAI.KadisonKastler.matrixUnitsEmbedding_trace line 64
9. theorem OAI.KadisonKastler.matrixTrace_coefficientMatrixMap line 89
10. def OAI.KadisonKastler.finiteMatrixEmbedding line 104

    Source documentation

    The concrete finite model embeds by the chosen inner matrix units, with the outer matrix coordinates represented on the Hilbert direct sum.

    def finiteMatrixEmbedding (E : Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M)) :
        FiniteMatrixModel n j →⋆ₐ[ℂ] Algebra (matrixVonNeumann (ι := Fin n) M) :=
    …

    Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.matrixVonNeumann

11. theorem OAI.KadisonKastler.matrixVonNeumannTrace_map line 108
12. theorem OAI.KadisonKastler.finiteMatrixEmbedding_trace line 116
13. theorem OAI.KadisonKastler.finiteMatrixEmbedding_scalar line 129

    Source documentation

    The outer scalar matrix algebra is fixed by every choice of inner matrix units.

    theorem finiteMatrixEmbedding_scalar
        (E : Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
        (x : CStarMatrix (Fin n) (Fin n) ℂ) :
        finiteMatrixEmbedding E
            (coefficientMatrixMap (StarAlgHom.ofId ℂ (CStarMatrix (Fin (j + 1)) (Fin (j + 1)) ℂ)) x) =
          matrixAlgebraHom M (coefficientMatrixMap (StarAlgHom.ofId ℂ (Algebra M)) x) := by
    …

    Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.finiteMatrixEmbedding, OAI.KadisonKastler.coefficientMatrixMap, OAI.KadisonKastler.matrixAlgebraHom