OAI/GroupTheory/PolycyclicRecognition/Algebra/IteratedCoinvariants.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Iterating normal-subgroup and quotient coinvariants

The two successive quotient maps have exactly the same quotient as taking coinvariants of the original group. This is the degree-zero comparison used in the central-filtration homology construction.

  1. def OAI.PolycyclicRecognition.normalCoinvariantsToCoinvariants line 19
  2. def OAI.PolycyclicRecognition.iteratedCoinvariantsToCoinvariants line 28
  3. def OAI.PolycyclicRecognition.coinvariantsToIteratedCoinvariants line 42
  4. def OAI.PolycyclicRecognition.iteratedCoinvariantsEquiv line 57
  5. theorem OAI.PolycyclicRecognition.iteratedCoinvariantsEquiv_mk line 75