OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralTransgressionNaturality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Naturality of the central transgression

The two squares of a morphism of extensions suffice. No compatibility between the arbitrarily chosen sections is required.

  1. theorem OAI.PolycyclicRecognition.centralExtension_cocycle_natural line 24
  2. theorem OAI.PolycyclicRecognition.centralExtension_cocycle_natural_chains line 45
  3. theorem OAI.PolycyclicRecognition.centralExtensionTransgression_natural line 74