OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralCocycleSplitting.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Splitting a cocycle into central fixed and moving summands

  1. def OAI.PolycyclicRecognition.centralFixedUnitary line 14
  2. def OAI.PolycyclicRecognition.centralMovingUnitary line 17
  3. theorem OAI.PolycyclicRecognition.centralFixedUnitary_center line 21
  4. theorem OAI.PolycyclicRecognition.centralFixedUnitary_no_fixed line 25
  5. theorem OAI.PolycyclicRecognition.centralMovingUnitary_no_central_fixed line 33
  6. def OAI.PolycyclicRecognition.centralFixedProjection line 42
  7. def OAI.PolycyclicRecognition.centralMovingProjection line 45
  8. theorem OAI.PolycyclicRecognition.centralFixedProjection_intertwines line 48
  9. theorem OAI.PolycyclicRecognition.centralMovingProjection_intertwines line 52
  10. theorem OAI.PolycyclicRecognition.centralProjections_add line 56
  11. theorem OAI.PolycyclicRecognition.centralFixedCocycle line 60
  12. theorem OAI.PolycyclicRecognition.centralMovingCocycle line 64
  13. theorem OAI.PolycyclicRecognition.centralFixedUnitary_continuous line 71
  14. theorem OAI.PolycyclicRecognition.centralMovingUnitary_continuous line 76