OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentQuotientRank.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform rank bounds persist in nilpotent quotients

The inverse image of a subgroup need not be finitely generated. For the generator bound we lift only a finite generating set. The abelian rank bound uses the full inverse image and needs no finite-generation assumption.

  1. def OAI.PolycyclicRecognition.quotientSubgroupMap line 19
  2. theorem OAI.PolycyclicRecognition.quotientSubgroupMap_surjective line 25
  3. theorem OAI.PolycyclicRecognition.nilpotent_quotient_subgroup_generator_rank_le line 32
  4. theorem OAI.PolycyclicRecognition.nilpotent_quotient_abelian_subgroup_rank_le line 42