OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralExtensionTransgressionExact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exactness of the central transgression at the kernel group

The image in the central kernel is exactly the kernel of its map to the abelianization of the extension group. The reverse containment is constructed from an actual integral bar boundary.

  1. def OAI.PolycyclicRecognition.centralExtensionAbelianizationMap line 21
  2. def OAI.PolycyclicRecognition.centralExtensionSectionAbelianChains line 24
  3. theorem OAI.PolycyclicRecognition.centralExtensionAbelianization_cocycle line 28
  4. theorem OAI.PolycyclicRecognition.centralExtensionAbelianization_chains line 39
  5. theorem OAI.PolycyclicRecognition.centralExtensionTransgression_abelianization line 61
  6. theorem OAI.PolycyclicRecognition.centralExtensionTransgression_exact line 69
  7. theorem OAI.PolycyclicRecognition.centralExtensionTransgression_range line 107