OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalNormalExtensionBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A rational homology bound for a finite-rank nilpotent extension

The bound is obtained from the actual normal-extension bicomplex. Its kernel rank hypothesis is explicit, and kernel torsion is permitted.

  1. theorem OAI.PolycyclicRecognition.normalExtension_rational_homology_isZero_of_kernel_bound line 20
  2. theorem OAI.PolycyclicRecognition.nilpotentNormal_rational_homology_bounded line 35
  3. theorem OAI.PolycyclicRecognition.torsionNilpotentNormal_rational_homology_isZero line 47