OAI/GroupTheory/PolycyclicRecognition/Lattices/PolycyclicLatticeRealization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The lattice-realization consequence of Dekimpe's theorem

All extensions used here are actual group extensions. The nilshadow construction supplies the connected Lie model without a splitting premise.

  1. theorem OAI.PolycyclicRecognition.IsPolycyclic.exists_solvable_finiteDimension line 16
  2. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_uniform_lattice line 31
  3. theorem OAI.PolycyclicRecognition.dekimpeLatticeRealizationInput line 55

    Source documentation

    Dekimpe's lattice-realization conclusion follows from nilpotent completion and the invariant graph construction.

    theorem dekimpeLatticeRealizationInput : DekimpeLatticeRealizationInput := by
…

    Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput