OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentRootDimension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite integral dimension from a finite nilpotent root core

A finitely generated subgroup containing a positive power of every element has finite index in each finitely generated overgroup. Those overgroups have one common duality dimension. The countable-union theorem then supplies a finite integral dimension for the original, possibly infinitely generated, nilpotent group. No ambient dimension bound is assumed.

  1. theorem OAI.PolycyclicRecognition.nilpotent_rootCore_finiteIndex_of_torsionFree line 22
  2. theorem OAI.PolycyclicRecognition.nilpotent_rootCore_common_duality line 34
  3. theorem OAI.PolycyclicRecognition.nilpotent_finiteDimension_of_rootCore line 54