OAI/GroupTheory/PolycyclicRecognition/Finiteness/StableSyzygyMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Syzygy maps modulo projective factors

A lift through the projective middle term induces an endomorphism of the next syzygy. Changing the lift changes that endomorphism by a projective factor.

  1. abbrev OAI.PolycyclicRecognition.resolutionSyzygy line 19
  2. def OAI.PolycyclicRecognition.resolutionSyzygyLift line 21
  3. theorem OAI.PolycyclicRecognition.resolutionSyzygyLift_comm line 26
  4. def OAI.PolycyclicRecognition.resolutionSyzygyMap line 30
  5. theorem OAI.PolycyclicRecognition.resolutionSyzygyMap_comm line 43
  6. theorem OAI.PolycyclicRecognition.resolutionSyzygyMap_stable_of_lift line 49
  7. theorem OAI.PolycyclicRecognition.resolutionSyzygyMap_stable_identity line 75
  8. def OAI.PolycyclicRecognition.resolutionSyzygyStableMap line 82
  9. theorem OAI.PolycyclicRecognition.resolutionSyzygyStableMap_eq_zero_of_projective_factor line 97
  10. def OAI.PolycyclicRecognition.resolutionStableSyzygyTransition line 115
  11. theorem OAI.PolycyclicRecognition.resolutionStableSyzygyTransition_class line 124
  12. theorem OAI.PolycyclicRecognition.resolutionStableSyzygyTransition_identity line 129