OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalRootCoreHomology.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rational homology is controlled by a finite nilpotent root core

Every class is represented at a finitely generated stage. The core has finite index in that stage, so rational transfer lifts the class to the fixed core. No stabilization or injectivity of integral homology maps is assumed.

  1. theorem OAI.PolycyclicRecognition.rational_homology_core_surjective line 23
  2. theorem OAI.PolycyclicRecognition.rational_homology_finite_of_core line 44
  3. theorem OAI.PolycyclicRecognition.finitelyGenerated_nilpotent_rational_homology_finite line 53
  4. theorem OAI.PolycyclicRecognition.nilpotent_rational_homology_finite_of_abelianization line 67
  5. theorem OAI.PolycyclicRecognition.nilpotent_rational_homology_finite line 91
  6. theorem OAI.PolycyclicRecognition.nilpotent_rational_homology_finite_of_first_homology line 103