OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalCentralTransgression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The central-extension comparison after rationalization

Flatness of the rationals preserves both exact pairs of the integral comparison. The source remains explicitly the rationalization of actual integral group homology.

  1. def OAI.PolycyclicRecognition.rationalCentralTransgression line 20
  2. theorem OAI.PolycyclicRecognition.rationalCentralTransgression_exact_H2 line 24
  3. theorem OAI.PolycyclicRecognition.rationalCentralTransgression_exact_kernel line 33