OAI/GroupTheory/PolycyclicRecognition/Algebra/AscendingExtensionDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The ascending virtually nilpotent case of the finiteness endgame

The hypotheses describe an actual ascending exhaustion of the kernel, with conjugation by a chosen lift as the transition automorphism. The construction produces a solvable subgroup of finite index and finite integral dimension. It does not assume any finiteness theorem for arbitrary elementary amenable groups of type FP-infinity.

  1. theorem OAI.PolycyclicRecognition.map_subtype_conjNormal line 21
  2. theorem OAI.PolycyclicRecognition.exists_finiteIndex_solvable_finiteDimension_of_ascending line 27