OAI/GroupTheory/PolycyclicRecognition/Finiteness/FreeRightCoefficientHomology.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Homology in the ambient-resolution direction

Fixing a free right tensor factor gives the actual finite-support functor. The comparison computes the columns of the normal-extension bicomplex, with the normal subgroup's ordinary integral homology as coefficients.

  1. def OAI.PolycyclicRecognition.rightCoinvariantsFunctor line 20
  2. instance OAI.PolycyclicRecognition.(instance at line 32) line 32
  3. def OAI.PolycyclicRecognition.rightFreeCoinvariantsIso line 38
  4. instance OAI.PolycyclicRecognition.rightFreeCoinvariants_preservesHomology line 60
  5. def OAI.PolycyclicRecognition.normalExtensionColumnHomologyIso line 78