OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentRootExhaustion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exhausting a countable nilpotent group by finite-index extensions of a core

Finite integral dimension supplies a finitely generated root core. Every finitely generated overgroup of that core contains it with finite index. This gives the directed family needed to compute the kernel's homology.

  1. theorem OAI.PolycyclicRecognition.nilpotent_rootCore_finiteIndex line 20
  2. theorem OAI.PolycyclicRecognition.exists_nilpotent_root_exhaustion line 31