OAI/Analysis/KadisonKastler/SignedMatrixRefinement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compatible finite signed groups under matrix refinement

Keeping the first matrix coordinates as sums over the new coordinates keeps the old signed-permutation group inside the new finite group.

  1. def OAI.KadisonKastler.matrixSignedGroup line 21

    Source documentation

    The finite subgroup actually represented by the matrix units.

    def matrixSignedGroup (E : Generator.MatrixUnitSystem ι A) : Subgroup (unitary A) :=
…

    Mentions: OAI.Generator.MatrixUnitSystem

  2. instance OAI.KadisonKastler.matrixSignedGroup_finite line 24
  3. theorem OAI.KadisonKastler.signedRepresentation_diagonal line 27
  4. theorem OAI.KadisonKastler.signedRepresentation_permutation line 33
  5. theorem OAI.KadisonKastler.signedDiagonal_refinement line 47
  6. theorem OAI.KadisonKastler.signedPermutation_refinement line 54
  7. theorem OAI.KadisonKastler.matrixSignedGroup_refinement line 64

    Source documentation

    Every old signed unitary is a new signed unitary after compatible refinement.

    theorem matrixSignedGroup_refinement : matrixSignedGroup E ≤ matrixSignedGroup F := by
…

    Mentions: OAI.KadisonKastler.matrixSignedGroup