OAI/Analysis/KadisonSimilarity/Tracial/MatrixDiagonalEmbedding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed diffuse matrix-generated factor is embedded diagonally in its finite matrix amplifications. The normalized trace is unchanged.

  1. def OAI.KadisonSimilarity.matrixDiagonalHom line 15

    Source documentation

    The unital diagonal embedding into a finite C-star matrix algebra.

    def matrixDiagonalHom : A →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A :=
…
  2. theorem OAI.KadisonSimilarity.matrixDiagonalHom_apply line 27
  3. theorem OAI.KadisonSimilarity.matrixDiagonalHom_diagonal line 32
  4. theorem OAI.KadisonSimilarity.matrixDiagonalHom_injective line 37
  5. theorem OAI.KadisonSimilarity.normalizedMatrixTrace_diagonal line 44
  6. theorem OAI.KadisonSimilarity.matrixEntryHom_diagonal line 55

    Source documentation

    Diagonal inclusion and entrywise subfactor inclusion commute.

    theorem matrixEntryHom_diagonal (φ : A →⋆ₐ[ℂ] B) (a : A) :
    matrixEntryHom φ (matrixDiagonalHom n a) = matrixDiagonalHom n (φ a) := by
…

    Mentions: OAI.KadisonSimilarity.matrixEntryHom, OAI.KadisonSimilarity.matrixDiagonalHom