OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalNormalExtensionHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rational homology comparison for the actual normal extension

These results apply exact rationalization to the constructed bar bicomplex. They retain all second-page hypotheses and do not infer finite rational rank from finite generation over the quotient group ring.

  1. theorem OAI.PolycyclicRecognition.normalExtension_rational_homology_finite_of_secondPage line 20
  2. theorem OAI.PolycyclicRecognition.normalExtension_rational_homology_isZero_of_secondPage line 44
  3. theorem OAI.PolycyclicRecognition.normalExtension_rational_homology_isZero_above line 64