LatticeCharacterization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Virtual polycyclicity and finite-index solvable lattices

Dekimpe's realization and polycyclicity of solvable Lie lattices identify virtual polycyclicity with a finite-index solvable-lattice realization.

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_finiteIndex_solvableLattice line 16
Source documentation
A group with a finite-index subgroup isomorphic to a uniform solvable Lie lattice is virtually polycyclic.
```
theorem virtuallyPolycyclic_of_finiteIndex_solvableLattice
    (fw : FarbWeinbergerLatticeInput) {H : Type} [Group H]
    (Γ : Subgroup H) (hΓ : Γ.FiniteIndex)
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsUniformLattice Λ) (e : Γ ≃* Λ) :
    IsVirtuallyPolycyclic H :=
…
```
Mentions: OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel
theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_iff_finiteIndex_solvableLattice line 26
Source documentation
Virtual polycyclicity is equivalent to finite-index realization as a discrete uniform lattice in a simply connected solvable Lie group.
```
theorem virtuallyPolycyclic_iff_finiteIndex_solvableLattice
    (dekimpe : DekimpeLatticeRealizationInput) (fw : FarbWeinbergerLatticeInput)
    (H : Type) [Group H] :
    IsVirtuallyPolycyclic H ↔
      ∃ Γ : Subgroup H, Γ.FiniteIndex ∧
        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),
          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) := by
…
```
Mentions: OAI.PolycyclicRecognition.DekimpeLatticeRealizationInput, OAI.PolycyclicRecognition.FarbWeinbergerLatticeInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel