OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalCentralQuotientAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Quotient actions on a normal subgroup's central extension

Inner automorphisms act trivially on second homology, and the central kernel is fixed by the normal subgroup. Thus both actions descend to the actual ambient quotient, as does the transgression intertwiner.

  1. theorem OAI.PolycyclicRecognition.integralSecondHomologyMap_conj line 19
  2. def OAI.PolycyclicRecognition.normalCentralHomologyRepresentation line 31
  3. def OAI.PolycyclicRecognition.normalCentralKernelRepresentation line 36
  4. theorem OAI.PolycyclicRecognition.normalCentralHomologyRepresentation_subgroup line 41
  5. theorem OAI.PolycyclicRecognition.normalCentralKernelRepresentation_subgroup line 57
  6. def OAI.PolycyclicRecognition.normalCentralQuotientHomologyAction line 67
  7. def OAI.PolycyclicRecognition.normalCentralQuotientKernelAction line 72
  8. def OAI.PolycyclicRecognition.normalCentralQuotientTransgression line 77