OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalizedProjectiveTower.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Comparison with the normalized complete-cohomology construction

  1. def OAI.PolycyclicRecognition.normalizedProjectiveTower line 12
  2. def OAI.PolycyclicRecognition.normalizedProjectiveTowerCohomology line 21
  3. def OAI.PolycyclicRecognition.IntegralProjectiveTower.completeCohomologyEquiv line 25
  4. def OAI.PolycyclicRecognition.normalizedProjectiveTowerMap line 31
  5. theorem OAI.PolycyclicRecognition.normalizedProjectiveTowerMap_cohomology line 38
  6. def OAI.PolycyclicRecognition.IntegralProjectiveTower.normalization line 51
  7. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.completeCohomologyEquiv_apply line 55
  8. theorem OAI.PolycyclicRecognition.IntegralProjectiveTower.completeCohomologyEquiv_natural line 60