OAI/Analysis/KadisonSimilarity/FreeProduct/FreeMatrixExtension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The matrix-factor automorphism extends to the actual normal tracial algebra by conjugating its left representation with the free-word unitary.

  1. def OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionUnitary line 24
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.conjugate_eq_of_intertwining line 28
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionUnitary_base line 40
  4. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionUnitary_other line 46
  5. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionUnitary_one line 53
  6. def OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionRepresentation line 57
  7. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionRepresentation_apply line 60
  8. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionRepresentation_mem line 68
  9. def OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionHom line 83

    Source documentation

    The algebraic extension in the original algebra, using its faithful normal coordinates.

    def freeMatrixExtensionHom : P →⋆ₐ[ℂ] P :=
…
  10. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionHom_left line 90
  11. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionHom_base line 100
  12. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionHom_other line 106
  13. theorem OAI.KadisonSimilarity.TracialCornerGeometry.vectorTrace_conjugate line 113
  14. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixExtensionHom_trace line 123
  15. theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixConjugationExtensionInput_of_normal_range line 134

    Source documentation

    Blanchard--Dykema's two-factor extension specialization, constructed for the given faithful normal tracial free product.

    theorem matrixConjugationExtensionInput_of_normal_range :
    G.MatrixConjugationExtensionInput D ι A := by
…