OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalFirstHomologyAbelianization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual quotient action on first homology is abelianization

The comparison intertwines ambient conjugation, including for a nonabelian normal subgroup. It identifies the first-homology representation used to control the rank of a nilpotent normal subgroup.

  1. theorem OAI.PolycyclicRecognition.normalAbelianizationRepresentation_map line 20
  2. def OAI.PolycyclicRecognition.normalFirstHomologyAbelianizationIso line 27