OAI/GroupTheory/PolycyclicRecognition/Finiteness/AscendingFinitenessEndgame.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The algebraic conclusion of the ascending structural alternative

These are concrete data for the ascending virtually nilpotent groups in Kropholler--Martínez-Pérez--Nucinkis, J. reine angew. Math. 637 (2009), Theorem 1.1(x). The ascending structure is an explicit hypothesis.

  1. structure OAI.PolycyclicRecognition.AscendingVirtuallyNilpotentData line 17
  2. theorem OAI.PolycyclicRecognition.AscendingVirtuallyNilpotentData.finitelyGenerated line 30
  3. theorem OAI.PolycyclicRecognition.AscendingVirtuallyNilpotentData.virtualSolvableFiniteDimension line 68
  4. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_ascending_normal_subgroup line 76