OAI/Analysis/BoundedHochschild/SignedMatrixUnitaries.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A finite group of signed permutation unitaries in a matrix system.

  1. def OAI.HochschildMatrixSystems.MatrixSystem.signScalar line 16
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.signScalar_xor line 18
  3. lemma OAI.HochschildMatrixSystems.MatrixSystem.signScalar_star line 21
  4. def OAI.HochschildMatrixSystems.MatrixSystem.signedPermutation line 24
  5. lemma OAI.HochschildMatrixSystems.MatrixSystem.signedPermutation_one line 27
  6. lemma OAI.HochschildMatrixSystems.MatrixSystem.signedPermutation_mul line 31
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.signedPermutation_star line 39
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.signedPermutation_mem_unitary line 48
  9. def OAI.HochschildMatrixSystems.MatrixSystem.signedPermutationUnitary line 56
  10. def OAI.HochschildMatrixSystems.MatrixSystem.signedPermutationGroup line 60

    Source documentation

    The actual finite subgroup used in the matrix separability homotopy.

    def signedPermutationGroup : Subgroup (unitary M) where
…
  11. instance OAI.HochschildMatrixSystems.MatrixSystem.signedPermutationGroup_finite line 71
  12. lemma OAI.HochschildMatrixSystems.MatrixSystem.signedPermutation_flip line 74
  13. lemma OAI.HochschildMatrixSystems.MatrixSystem.entry_mem_signedPermutation_span line 86

    Source documentation

    Signed permutation unitaries linearly span every matrix entry.

    lemma entry_mem_signedPermutation_span (i j : Fin n) :
    E.entry i j ∈ Submodule.span ℂ
      (Set.range (fun u : E.signedPermutationGroup => ((u : unitary M) : M))) := by
…
  14. lemma OAI.HochschildMatrixSystems.MatrixSystem.neg_one_mem_signedPermutationGroup line 100