OAI/Analysis/KadisonKastler/MatrixVonNeumann.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The concrete von Neumann algebra of finite matrices

The commutant of the diagonal copy of M' consists exactly of the operators all of whose matrix entries lie in M. This identifies it with the usual C⋆-matrix algebra, including the represented normalized trace.

  1. def OAI.KadisonKastler.FaithfulTracialState.comapStarAlgEquiv line 20

    Source documentation

    Pull a faithful tracial state back along a star-algebra equivalence.

    def FaithfulTracialState.comapStarAlgEquiv {A B : Type*} [CStarAlgebra A] [CStarAlgebra B]
    (τ : FaithfulTracialState B) (e : A ≃⋆ₐ[ℂ] B) : FaithfulTracialState A where
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState

  2. def OAI.KadisonKastler.matrixVonNeumann line 47
  3. theorem OAI.KadisonKastler.mem_matrixVonNeumann_iff_diagonal line 53
  4. theorem OAI.KadisonKastler.mem_matrixVonNeumann_iff_entries line 69
  5. def OAI.KadisonKastler.matrixOperatorHom line 91
  6. theorem OAI.KadisonKastler.matrixOperatorHom_apply line 96
  7. theorem OAI.KadisonKastler.operatorEntry_matrixOperatorHom line 100
  8. theorem OAI.KadisonKastler.matrixOperatorHom_mem line 107
  9. theorem OAI.KadisonKastler.matrixOperatorHom_injective line 114
  10. theorem OAI.KadisonKastler.norm_matrixOperatorHom line 123
  11. def OAI.KadisonKastler.matrixFromOperator line 127
  12. theorem OAI.KadisonKastler.matrixOperatorHom_matrixFromOperator line 133
  13. def OAI.KadisonKastler.matrixAlgebraHom line 144
  14. def OAI.KadisonKastler.matrixAlgebraEquiv line 154
  15. theorem OAI.KadisonKastler.matrixAlgebraEquiv_apply line 162
  16. theorem OAI.KadisonKastler.matrixAlgebraEquiv_symm_operator line 166
  17. def OAI.KadisonKastler.matrixVonNeumannTrace line 173
  18. theorem OAI.KadisonKastler.matrixVonNeumannTrace_finiteVector line 178
  19. def OAI.KadisonKastler.matrixDiagonalProjection line 192

    Source documentation

    The actual coordinate projections in the represented matrix algebra.

    def matrixDiagonalProjection (M : VonNeumannAlgebra H) (i : ι) :
    Algebra (matrixVonNeumann (ι := ι) M) :=
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann

  20. theorem OAI.KadisonKastler.matrixDiagonalProjection_isStarProjection line 197
  21. theorem OAI.KadisonKastler.matrixVonNeumannTrace_diagonal line 201
  22. theorem OAI.KadisonKastler.finiteAverage_matrixDiagonalProjection line 210