OAI/Analysis/KadisonKastler/MatrixFixedCorners.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A matrix automorphism fixing the two diagonal projections

Its off-diagonal coefficient is unitary and conjugates the two corner actions. This is the finite algebraic step in the modular cocycle argument.

  1. def OAI.KadisonKastler.matrixSlot line 17
  2. theorem OAI.KadisonKastler.matrixSlot_injective line 20
  3. theorem OAI.KadisonKastler.matrixSlot_mul line 25
  4. theorem OAI.KadisonKastler.matrixSlot_star line 29
  5. theorem OAI.KadisonKastler.matrixSlot_sandwich line 33
  6. theorem OAI.KadisonKastler.matrixSlot_reconstruct line 41
  7. theorem OAI.KadisonKastler.matrixSlot_image_reconstruct line 50
  8. def OAI.KadisonKastler.matrixOffDiagonalCoefficient line 58
  9. theorem OAI.KadisonKastler.matrixOffDiagonalCoefficient_unitary line 60
  10. theorem OAI.KadisonKastler.matrixCorner_actions_conjugate line 73