OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentClassBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A uniform nilpotency-class bound from integral dimension

A maximal abelian normal subgroup of a nilpotent group is self-centralizing. The faithful rational conjugation action bounds the lower central series modulo that subgroup. Its pulled-back rational filtration bounds the remaining series inside it. Each part has length at most the rational rank.

  1. def OAI.PolycyclicRecognition.rationalConjugationLinear line 21
  2. theorem OAI.PolycyclicRecognition.rationalConjugationLinear_ker line 25
  3. theorem OAI.PolycyclicRecognition.nilpotencyClass_le_twice_rationalRank line 33
  4. theorem OAI.PolycyclicRecognition.nilpotencyClass_le_twice_cohomologicalDimension line 52
  5. theorem OAI.PolycyclicRecognition.nilpotent_subgroup_class_le line 66