OAI/Topology/CoarseAssembly/K1TwoByTwo.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The two-by-two stabilization used for spatial K₁ representatives

  1. theorem OAI.CoarseAssembly.TopologicalK1.matrixClass_inv line 14
  2. theorem OAI.CoarseAssembly.TopologicalK1.matrixClass_conjugate line 20
  3. def OAI.CoarseAssembly.TopologicalK1.scalarUnitMatrix line 25
  4. def OAI.CoarseAssembly.TopologicalK1.diagonalTwoUnits line 28
  5. theorem OAI.CoarseAssembly.TopologicalK1.diagonalTwo_stabilizes line 36
  6. theorem OAI.CoarseAssembly.TopologicalK1.diagonalTwo_matrixClass_one line 44
  7. def OAI.CoarseAssembly.TopologicalK1.flipTwoUnits line 48
  8. theorem OAI.CoarseAssembly.TopologicalK1.diagonalTwo_flip line 59
  9. theorem OAI.CoarseAssembly.TopologicalK1.diagonalTwo_matrixClass_swap line 69
  10. theorem OAI.CoarseAssembly.TopologicalK1.diagonalTwo_mul line 75
  11. theorem OAI.CoarseAssembly.TopologicalK1.diagonalTwo_matrixClass line 84

    Source documentation

    The exact stabilization identity for two relative unitaries.

    theorem diagonalTwo_matrixClass (g h : Rˣ) :
    matrixClass R (diagonalTwoUnits g h) =
      matrixClass R (scalarUnitMatrix g) + matrixClass R (scalarUnitMatrix h) := by
…

    Mentions: OAI.CoarseAssembly.TopologicalK1.matrixClass, OAI.CoarseAssembly.TopologicalK1.diagonalTwoUnits, OAI.CoarseAssembly.TopologicalK1.scalarUnitMatrix