OAI/GroupTheory/PolycyclicRecognition/Finiteness/CountableUnionCohomology.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cohomology above a uniform dimension bound on an exhaustive sequence

Two consecutive local vanishings suffice. The primitive-correction argument accounts for the one extra dimension in a countable increasing union.

  1. theorem OAI.PolycyclicRecognition.cochain_primitive_of_isZero line 19
  2. def OAI.PolycyclicRecognition.subgroupCochainStep line 30
  3. theorem OAI.PolycyclicRecognition.subgroupCochainStep_surjective line 36
  4. theorem OAI.PolycyclicRecognition.groupCohomology_isZero_of_exhaustion line 46