OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentRationalConjugation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent conjugation has a dimension-bounded unipotence exponent

On an abelian normal subgroup, conjugation minus the identity is the commutator map. Its successive powers lie in successive lower-central terms. Rationalization therefore gives a nilpotent operator, whose exponent is bounded by the rational rank rather than by a chosen group nilpotency class.

  1. def OAI.PolycyclicRecognition.integralConjugationDifference line 22
  2. theorem OAI.PolycyclicRecognition.integralConjugationDifference_apply line 25
  3. theorem OAI.PolycyclicRecognition.integralConjugationDifference_pow_mem line 34
  4. theorem OAI.PolycyclicRecognition.integralConjugationDifference_nilpotent line 44
  5. theorem OAI.PolycyclicRecognition.rationalConjugationDifference_baseChange line 55
  6. theorem OAI.PolycyclicRecognition.rationalConjugationDifference_nilpotent line 64
  7. theorem OAI.PolycyclicRecognition.nilpotentEnd_pow_finrank_eq_zero line 71
  8. theorem OAI.PolycyclicRecognition.rationalConjugationDifference_pow_rank line 81