OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompletedCohomology.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Degree-zero complete cohomology from normalized syzygies

The transition maps are the actual connecting homomorphisms of the natural short exact free-cover sequences. No vanishing theorem is assumed here.

  1. abbrev OAI.PolycyclicRecognition.normalizedCohomologyStage line 16
  2. def OAI.PolycyclicRecognition.normalizedCohomologyStageMap line 19
  3. theorem OAI.PolycyclicRecognition.normalizedCohomologyStageMap_id line 24
  4. theorem OAI.PolycyclicRecognition.normalizedCohomologyStageMap_comp line 30
  5. theorem OAI.PolycyclicRecognition.normalizedSyzygyConnecting_natural line 38
  6. def OAI.PolycyclicRecognition.normalizedCohomologyForward line 48
  7. instance OAI.PolycyclicRecognition.normalizedCohomologyForward_directed line 62
  8. theorem OAI.PolycyclicRecognition.normalizedCohomologyForward_natural line 68
  9. abbrev OAI.PolycyclicRecognition.CompletedCohomology line 92
  10. def OAI.PolycyclicRecognition.completedCohomologyMap line 95
  11. theorem OAI.PolycyclicRecognition.completedCohomologyMap_of line 104
  12. def OAI.PolycyclicRecognition.completedCohomologyFunctor line 115