OAI/GroupTheory/PolycyclicRecognition/Geometry/PresentationRotation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Rotating a short exact sequence using a projective cover

  1. abbrev OAI.PolycyclicRecognition.rotationMiddle line 14
  2. def OAI.PolycyclicRecognition.rotationFst line 17
  3. def OAI.PolycyclicRecognition.rotationSnd line 20
  4. def OAI.PolycyclicRecognition.rotationInl line 24
  5. def OAI.PolycyclicRecognition.rotationInr line 27
  6. def OAI.PolycyclicRecognition.rotationProjection line 31
  7. def OAI.PolycyclicRecognition.rotationInclusion line 35
  8. theorem OAI.PolycyclicRecognition.rotationProjection_apply line 40
  9. theorem OAI.PolycyclicRecognition.rotationInclusion_apply line 44
  10. theorem OAI.PolycyclicRecognition.rotation_zero line 49
  11. def OAI.PolycyclicRecognition.presentationRotation line 62
  12. theorem OAI.PolycyclicRecognition.rotationProjection_g line 66
  13. theorem OAI.PolycyclicRecognition.rotationInclusion_injective line 71
  14. theorem OAI.PolycyclicRecognition.rotationProjection_surjective line 80
  15. theorem OAI.PolycyclicRecognition.presentationRotation_exact line 93
  16. theorem OAI.PolycyclicRecognition.presentationRotation_shortExact line 119
  17. theorem OAI.PolycyclicRecognition.rotationInclusion_fst line 126
  18. theorem OAI.PolycyclicRecognition.rotationInclusion_snd line 130
  19. theorem OAI.PolycyclicRecognition.rotationInl_fst line 134
  20. theorem OAI.PolycyclicRecognition.rotationInl_projection line 138
  21. theorem OAI.PolycyclicRecognition.rotation_fst_inl_stable line 148
  22. def OAI.PolycyclicRecognition.rotationToNormalized line 160