OAI/GroupTheory/PolycyclicRecognition/Finiteness/ShiftedCompletedCohomology.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative degree shifts of complete cohomology

The hierarchy argument uses positive connecting degrees. The n-th stage is H^(n+p)(G, Omega^n A), with the actual coefficient connecting maps.

  1. def OAI.PolycyclicRecognition.shiftedSyzygyConnecting line 16
  2. abbrev OAI.PolycyclicRecognition.shiftedCohomologyStage line 22
  3. def OAI.PolycyclicRecognition.shiftedCohomologyStageMap line 25
  4. theorem OAI.PolycyclicRecognition.shiftedCohomologyStageMap_id line 30
  5. theorem OAI.PolycyclicRecognition.shiftedCohomologyStageMap_comp line 36
  6. theorem OAI.PolycyclicRecognition.shiftedSyzygyConnecting_natural line 44
  7. def OAI.PolycyclicRecognition.shiftedCohomologyForward line 54
  8. instance OAI.PolycyclicRecognition.shiftedCohomologyForward_directed line 68
  9. theorem OAI.PolycyclicRecognition.shiftedCohomologyForward_natural line 74
  10. abbrev OAI.PolycyclicRecognition.ShiftedCompletedCohomology line 98
  11. def OAI.PolycyclicRecognition.shiftedCompletedCohomologyMap line 101
  12. theorem OAI.PolycyclicRecognition.shiftedCompletedCohomologyMap_of line 110
  13. def OAI.PolycyclicRecognition.shiftedCompletedCohomologyFunctor line 121