OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalHomologyActionComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The canonical quotient action agrees with conjugation

The comparison uses the actual inclusion of subgroup bar chains. Inner bar translation is homotopic to the identity before passing to coinvariants.

  1. abbrev OAI.PolycyclicRecognition.normalBarComplex line 20
  2. abbrev OAI.PolycyclicRecognition.normalBarInnerMap line 24
  3. theorem OAI.PolycyclicRecognition.normalSubgroupBarChains_conjugation line 32
  4. theorem OAI.PolycyclicRecognition.normalBarInnerMap_homology line 67
  5. theorem OAI.PolycyclicRecognition.normalSubgroupBarHomology_conjugation line 79