OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalizedStableSyzygyMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Additivity of normalized syzygy maps modulo projective factors

The normalized free cover is not additive. Its induced syzygy map is additive in the stable quotient; changing a lift produces a map through a free module.

  1. theorem OAI.PolycyclicRecognition.normalizedSyzygy_stable_of_lift line 19
  2. def OAI.PolycyclicRecognition.normalizedSyzygyStableLinearMap line 38
  3. theorem OAI.PolycyclicRecognition.normalizedSyzygyStableLinearMap_eq_zero line 51
  4. def OAI.PolycyclicRecognition.normalizedStableSyzygyMap line 63
  5. theorem OAI.PolycyclicRecognition.normalizedStableSyzygyMap_class line 72
  6. def OAI.PolycyclicRecognition.normalizedStableSyzygyIterate line 76
  7. theorem OAI.PolycyclicRecognition.normalizedStableSyzygyIterate_class line 85