OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompletedCohomologyAdditive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Additivity of complete cohomology

The free-cover construction is nonlinear, but its error is a projective factor. The next connecting homomorphism kills that error, so the limit is additive.

  1. theorem OAI.PolycyclicRecognition.cohomology_connecting_zero_of_projective_factor line 17
  2. theorem OAI.PolycyclicRecognition.completedCohomologyMap_add line 34
  3. instance OAI.PolycyclicRecognition.completedCohomologyFunctor_additive line 75