OAI/GroupTheory/PolycyclicRecognition/Finiteness/SequentialResolutionVanishing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Vanishing coefficient limits in finite resolution degrees

A finite group-ring module sends a coefficient system with zero direct limit to an eventually zero Hom system. Applying this to a cocycle in a projective resolution proves the corresponding zero-finitary cohomology statement.

  1. abbrev OAI.PolycyclicRecognition.resolutionCochainCoefficientMap line 24
  2. theorem OAI.PolycyclicRecognition.homologyMap_cycle_eq_zero_of_component line 29
  3. abbrev OAI.PolycyclicRecognition.coefficientModuleTransition line 45
  4. theorem OAI.PolycyclicRecognition.finiteRepresentation_eventually_zero line 52
  5. theorem OAI.PolycyclicRecognition.finiteResolutionCohomology_eventually_zero line 75
  6. theorem OAI.PolycyclicRecognition.TypeFP.cohomology_eventually_zero line 90
  7. theorem OAI.PolycyclicRecognition.TypeFPInfinity.cohomology_eventually_zero line 107