OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalNilpotentHomologyVanishing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform rational homology bounds for nilpotent root extensions

A fixed finitely generated root core bounds rational homology with every coefficient representation. Torsion is allowed, and no finiteness assumption on the coefficient representation is needed for vanishing.

  1. theorem OAI.PolycyclicRecognition.rational_homology_isZero_of_surjective line 22
  2. theorem OAI.PolycyclicRecognition.rational_homology_surjective_of_nilpotent_roots line 33
  3. theorem OAI.PolycyclicRecognition.rational_homology_isZero_of_finiteIndex line 55
  4. theorem OAI.PolycyclicRecognition.finitelyGenerated_nilpotent_rational_homology_bounded line 63
  5. theorem OAI.PolycyclicRecognition.nilpotent_rational_homology_bounded_of_rootCore line 77
  6. theorem OAI.PolycyclicRecognition.nilpotent_rational_homology_bounded_of_abelianization line 91
  7. theorem OAI.PolycyclicRecognition.torsion_nilpotent_rational_homology_isZero line 99