OAI/GroupTheory/PolycyclicRecognition/Finiteness/CentralTransgressionHomologyExact.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exactness of the central transgression at second homology

When the transgression of a two-cycle vanishes, its corrected section lift is completed to a cycle by an actual bar chain in the abelian kernel. Degenerate chains supply the explicit homotopy after projection.

  1. theorem OAI.PolycyclicRecognition.centralExtension_cycle_lift line 19
  2. theorem OAI.PolycyclicRecognition.centralExtensionTransgression_exact_H2 line 58