OAI/GroupTheory/PolycyclicRecognition/Finiteness/IteratedCoinvariantsHomology.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Iterated coinvariants of an ambient resolution

The natural degree-zero comparison extends to complexes and identifies their homology with actual group homology. This retains the ambient resolution for the subsequent filtration argument.

  1. def OAI.PolycyclicRecognition.iteratedCoinvariantsFunctorIso line 20
  2. def OAI.PolycyclicRecognition.iteratedCoinvariantsComplexIso line 33
  3. def OAI.PolycyclicRecognition.groupTrivialCoinvariantsTensorIso line 41
  4. def OAI.PolycyclicRecognition.iteratedResolutionHomologyIso line 54