OAI/GroupTheory/PolycyclicRecognition/Finiteness/SequentialCohomologyKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Detecting a zero cohomology class at a finite coefficient stage

For positive degrees, a boundary in the coefficient colimit can be lifted to one finite stage. Finite presentation lifts the cochain, and finite generation kills the resulting error at a later stage.

  1. theorem OAI.PolycyclicRecognition.cochain_class_zero_of_boundary line 20
  2. theorem OAI.PolycyclicRecognition.resolution_cohomologyMap_zero_of_boundary line 30
  3. theorem OAI.PolycyclicRecognition.finiteResolutionCohomology_colimit_kernel line 52
  4. theorem OAI.PolycyclicRecognition.TypeFPInfinity.cohomology_colimit_kernel line 99