OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentFiniteRankRootCore.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite root cores from the rational abelianization of a nilpotent group

Induction uses the last lower-central layer. Its commutator tensor presentation is finite because the preceding layer is an abelian subgroup of the quotient, where a finite root core has already been constructed.

  1. theorem OAI.PolycyclicRecognition.abelianization_map_surjective line 19

    Distinct definitions of this name: OAI/GroupTheory/PolycyclicRecognition/Analysis/AscendingBaseTransport.lean:48 (different declaration text). Qualify references as OAI.PolycyclicRecognition.abelianization_map_surjective@path.

  2. theorem OAI.PolycyclicRecognition.rational_abelianization_finite_of_surjective line 26
  3. theorem OAI.PolycyclicRecognition.lowerCentral_rootCore_of_finite_abelianization line 34
  4. theorem OAI.PolycyclicRecognition.nilpotent_rootCore_of_finite_abelianization line 116