OAI/Analysis/KadisonKastler/MatrixCornerConjugation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Independent unitary actions on an off-diagonal corner

Two orthogonal isometries identify the ambient algebra with its two-by-two amplification. Block-diagonal conjugations then act independently on the two sides of an off-diagonal coefficient. Convexity extends this action to multiplication by small contractions.

  1. def OAI.KadisonKastler.twoBlockUnitary line 22
  2. theorem OAI.KadisonKastler.CuntzFamily.matrixEquiv_symm_eq_assemble line 37
  3. def OAI.KadisonKastler.CuntzFamily.liftedTwoBlockUnitary line 42
  4. theorem OAI.KadisonKastler.CuntzFamily.matrix_liftedTwoBlockUnitary line 45
  5. theorem OAI.KadisonKastler.CuntzFamily.liftedTwoBlockUnitary_mem line 50
  6. theorem OAI.KadisonKastler.CuntzFamily.exists_corner_conjugate line 65
  7. def OAI.KadisonKastler.CuntzFamily.upperRightLinearMap line 91
  8. theorem OAI.KadisonKastler.CuntzFamily.small_contraction_corner_mem line 96