OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalNilpotentTorsion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A nilpotent group with zero rational abelianization is torsion

The last lower-central layer is a quotient of a tensor product whose first factor is the abelianization. The proof works for every nilpotency class and does not require finite generation.

  1. theorem OAI.PolycyclicRecognition.rational_abelianization_isZero_of_surjective line 19
  2. theorem OAI.PolycyclicRecognition.lowerCentral_torsion_of_rational_abelianization_isZero line 26
  3. theorem OAI.PolycyclicRecognition.nilpotent_torsion_of_rational_abelianization_isZero line 112