OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalDerivedHomologyFiniteness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

FP finiteness of the canonical quotient action on subgroup homology

The action is defined by deriving normal-subgroup coinvariants. Its underlying integral module is the usual subgroup homology. Its finite generation follows from the actual finite terms in an ambient projective resolution.

  1. def OAI.PolycyclicRecognition.normalDerivedHomology line 19
  2. def OAI.PolycyclicRecognition.normalDerivedHomologyIso line 22
  3. theorem OAI.PolycyclicRecognition.typeFP_normalDerivedHomology_finite line 30
  4. theorem OAI.PolycyclicRecognition.typeFPInfinity_normalDerivedHomology_finite line 37