OAI/GroupTheory/PolycyclicRecognition/Finiteness/QuotientResolutionHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normal coinvariants of an ambient projective resolution

Forgetting the quotient action recovers the ordinary integral homology of the normal subgroup. The comparison retains the chosen ambient resolution.

  1. def OAI.PolycyclicRecognition.quotientCoinvariantsUnderlyingIso line 18
  2. def OAI.PolycyclicRecognition.trivialCoinvariantsTensorIso line 24
  3. def OAI.PolycyclicRecognition.quotientResolutionHomologyIso line 37