OAI/GroupTheory/PolycyclicRecognition/Finiteness/ProjectiveCoefficientHomology.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive group homology vanishes for projective coefficients

Free coefficients reduce to finite-support sums of an exact bar resolution. Projective coefficients are handled by an actual split free cover.

  1. instance OAI.PolycyclicRecognition.freeCoefficientCoinvariants_preservesHomology line 19
  2. theorem OAI.PolycyclicRecognition.freeCoefficient_groupHomology_succ_isZero line 35
  3. theorem OAI.PolycyclicRecognition.projectiveCoefficient_groupHomology_succ_isZero line 45
  4. theorem OAI.PolycyclicRecognition.normalExtensionRowHomology_succ_isZero line 66