OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentGeneratorRank.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform generator bounds for nilpotent subgroups

Along a torsion-free cyclic series the duality dimension counts the infinite factors, each of which adds at most one generator. Thus an ambient integral cohomological-dimension bound controls the number of generators of every finitely generated nilpotent subgroup.

  1. theorem OAI.PolycyclicRecognition.exists_poincareDuality_rank_bound_of_cyclic_quotient line 20
  2. theorem OAI.PolycyclicRecognition.IsPolyZ.exists_poincareDuality_rank_bound line 45
  3. theorem OAI.PolycyclicRecognition.nilpotent_subgroup_generator_rank_le line 84
  4. theorem OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension.bounds_nilpotent_generator_rank line 93