OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalLocallyNilpotentDimension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integral dimension from a rational bound for locally nilpotent groups

A finitely generated torsion-free nilpotent subgroup is an integral duality group. Its orientation class detects its dimension over the rationals. The countable exhaustion therefore has uniformly bounded integral dimension.

  1. theorem OAI.PolycyclicRecognition.RationalHomologyDimensionLE.nilpotent_subgroup_dimension line 19
  2. theorem OAI.PolycyclicRecognition.RationalHomologyDimensionLE.nilpotent_subgroup_rank line 29
  3. theorem OAI.PolycyclicRecognition.RationalHomologyDimensionLE.locallyNilpotent_integralDimension line 36
  4. theorem OAI.PolycyclicRecognition.RationalHomologyDimensionLE.locallyNilpotent_isNilpotent line 47