OAI/GroupTheory/PolycyclicRecognition/Finiteness/ProjectiveTowerCohomology.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Cohomology along a projective syzygy tower

  1. theorem OAI.PolycyclicRecognition.cohomologyConnecting_projective_factor line 13
  2. abbrev OAI.PolycyclicRecognition.IntegralProjectiveTower.cohomologyStage line 33
  3. def OAI.PolycyclicRecognition.IntegralProjectiveTower.connecting line 36
  4. def OAI.PolycyclicRecognition.IntegralProjectiveTower.forward line 40
  5. instance OAI.PolycyclicRecognition.IntegralProjectiveTower.(instance at line 54) line 54
  6. abbrev OAI.PolycyclicRecognition.IntegralProjectiveTower.Cohomology line 59
  7. def OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.stageMap line 65
  8. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.connecting_natural line 68
  9. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.forward_natural line 74
  10. def OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.cohomologyMap line 92
  11. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.Map.cohomologyMap_of line 97