SolvableLatticeRecognition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The algebraic endgame for recognition of solvable Lie lattices

B. Farb and S. Weinberger, Isometries, rigidity and universal covers, Annals of Mathematics 168 (2008), 915–940, Proposition 3.4, p.932, states that every lattice in a connected solvable Lie group is polycyclic. The lattice-polycyclicity predicate specializes this statement to uniform lattices in connected simply connected solvable Lie groups.

Elementary amenability and the finiteness and duality theorems give virtual polycyclicity. Dekimpe's realization then produces a finite-index lattice in a possibly different solvable Lie group. Elementary amenability remains an explicit premise of these conditional recognition theorems.

def OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput line 26
Source documentation
The simply connected uniform-lattice specialization of Farb–Weinberger (2008), Proposition 3.4.
```
def FarbWeinbergerLatticeInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_elementaryAmenable_coarse_solvableLattice line 32
Source documentation
Coarse comparison with an actual solvable Lie lattice supplies the polycyclic comparison group for the elementary-amenable endgame.
```
theorem virtuallyPolycyclic_of_elementaryAmenable_coarse_solvableLattice
    (fw : FarbWeinbergerLatticeInput)
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsUniformLattice Λ)
    (H : Type) [Group H] [Group.FG H] (hEA : IsElementaryAmenable H)
    (e : GroupCoarseEquivalence Λ H) : IsVirtuallyPolycyclic H := by
…
```
Mentions: OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsElementaryAmenable, OAI.PolycyclicRecognition.GroupCoarseEquivalence
theorem OAI.PolycyclicRecognition.exists_solvableLattice_of_elementaryAmenable_coarse_solvableLattice line 48
Source documentation
The lattice realization follows from the algebraic endgame and the precisely stated published realization theorem. The ambient Lie group is allowed to change, as in the manuscript's lattice-recognition statement.
```
theorem exists_solvableLattice_of_elementaryAmenable_coarse_solvableLattice
    (dekimpe : DekimpeLatticeRealizationInput) (fw : FarbWeinbergerLatticeInput)
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsUniformLattice Λ)
    (H : Type) [Group H] [Group.FG H] (hEA : IsElementaryAmenable H)
    (e : GroupCoarseEquivalence Λ H) :
    ∃ Γ : Subgroup H, Γ.FiniteIndex ∧
      ∃ (S' : SimplyConnectedSolvableLieModel) (Λ' : Subgroup S'.carrier),
        IsUniformLattice Λ' ∧ Nonempty (Γ ≃* Λ') := by
…
```
Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput, OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsElementaryAmenable, OAI.PolycyclicRecognition.GroupCoarseEquivalence