OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralExtensionTransgressionKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The transgression vanishes on homology lifted from the extension

The section coordinate gives an explicit coboundary after pullback to the extension group. All maps below are maps on the actual bar complex.

  1. theorem OAI.PolycyclicRecognition.centralExtension_coordinate_mul line 21
  2. theorem OAI.PolycyclicRecognition.centralExtensionTwoCocycle_pullback line 43
  3. def OAI.PolycyclicRecognition.centralExtensionCoordinateChains line 56
  4. theorem OAI.PolycyclicRecognition.centralExtensionTwoCocycle_chains_pullback line 62
  5. theorem OAI.PolycyclicRecognition.centralExtensionTransgression_lift line 90