OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalizedSyzygyFunctor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Functorial syzygies from the normalized free cover

  1. abbrev OAI.PolycyclicRecognition.normalizedSyzygy line 13
  2. def OAI.PolycyclicRecognition.normalizedSyzygyMap line 16
  3. theorem OAI.PolycyclicRecognition.normalizedSyzygyMap_ι line 22
  4. def OAI.PolycyclicRecognition.normalizedSyzygyFunctor line 27
  5. theorem OAI.PolycyclicRecognition.normalizedSyzygyMap_zero line 39
  6. def OAI.PolycyclicRecognition.normalizedSyzygySequence line 44
  7. theorem OAI.PolycyclicRecognition.normalizedSyzygySequence_shortExact line 48
  8. def OAI.PolycyclicRecognition.normalizedSyzygySequenceMap line 59
  9. def OAI.PolycyclicRecognition.iteratedNormalizedSyzygy line 67
  10. def OAI.PolycyclicRecognition.normalizedSyzygyConnecting line 71