OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentAbelianQuotientRank.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rank bounds for abelian quotients of nilpotent groups

A finite independent family in a quotient lifts inside a finitely generated nilpotent subgroup. Its lattice quotient is bounded by the cohomological dimension of that subgroup. No finite generation of the original kernel or quotient is required.

  1. theorem OAI.PolycyclicRecognition.nilpotent_abelian_quotient_lattice_rank_le line 21
  2. theorem OAI.PolycyclicRecognition.nilpotent_abelian_quotient_rank_le line 45