SolvableLatticeModel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Solvable-lattice realization

K. Dekimpe, Solvable Lie Algebras, Lie Groups and Polynomial Structures, Compositio Mathematica 121 (2000), 183–204, Theorem 4.1, p.199, DOI 10.1023/A:1001738932743, gives a finite-index subgroup of a polycyclic-by-finite group as a uniform lattice in a connected simply connected solvable Lie group. We use only this consequence, omitting the additional equality with the Fitting subgroup and omitting normality.

The realization predicate specifies a finite-dimensional smooth Lie structure and a discrete lattice with compact coset quotient.

structure OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel line 31
Source documentation
A connected simply connected finite-dimensional real solvable Lie group. No metric or lattice is part of this record.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:82 (same declaration text).
```
structure SimplyConnectedSolvableLieModel where
…
```
def OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput line 56
Source documentation
The exact lattice-realization consequence of Dekimpe's Theorem 4.1 needed for the paper's lattice formulation.
```
def DekimpeLatticeRealizationInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.exists_uniform_solvable_lattice_of_virtuallyPolycyclic line 64
Source documentation
Restate the published realization using the equivalent compact-cover definition used by the metric lattice lemmas.
```
theorem exists_uniform_solvable_lattice_of_virtuallyPolycyclic
    (dekimpe : DekimpeLatticeRealizationInput)
    (P : Type) [Group P] (hP : IsVirtuallyPolycyclic P) :
    ∃ Γ : Subgroup P, Γ.FiniteIndex ∧
      ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),
        IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) := by
…
```
Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel