OAI/GroupTheory/PolycyclicRecognition/Finiteness/IntegralProjectiveTower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Integral projective syzygy towers

This records the successive projective presentations used by the normalized and horseshoe constructions. Maps lift recursively, and their induced stable maps depend only on the stable map at the initial coefficient.

  1. structure OAI.PolycyclicRecognition.IntegralProjectiveTower line 17
  2. def OAI.PolycyclicRecognition.IntegralProjectiveTower.sequence line 28
  3. instance OAI.PolycyclicRecognition.IntegralProjectiveTower.(instance at line 31) line 31
  4. instance OAI.PolycyclicRecognition.IntegralProjectiveTower.(instance at line 33) line 33
  5. structure OAI.PolycyclicRecognition.IntegralProjectiveTower.Map line 35
  6. def OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.sequenceMap line 44
  7. def OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.identity line 51
  8. def OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.comp line 57
  9. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.stable_eq line 65
  10. def OAI.PolycyclicRecognition.IntegralProjectiveTower.liftedApp line 77
  11. def OAI.PolycyclicRecognition.IntegralProjectiveTower.liftMap line 83
  12. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.liftMap_zero line 93