OAI/GroupTheory/PolycyclicRecognition/RecognitionFromGromov.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Recognition from the polynomial-growth theorem

The geometric height estimate, lattice realization, finiteness, and duality combine with the exact polynomial-growth statement of Gromov's theorem.

  1. theorem OAI.PolycyclicRecognition.recognition_and_lattice_of_gromov line 17
  2. theorem OAI.PolycyclicRecognition.group_recognition_of_gromov line 77
  3. theorem OAI.PolycyclicRecognition.uniform_lattice_recognition_of_gromov line 106

    Source documentation

    In particular a group quasi-isometric to a uniform solvable Lie lattice has a finite-index subgroup which is a uniform solvable Lie lattice.

    theorem uniform_lattice_recognition_of_gromov
    (gromov : ∀ (K : Type) [Group K] [DecidableEq K], GromovPolynomialGrowthInput K)
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsUniformLattice Λ)
    {J : Type} [Group J] [Group.FG J] (e : GroupCoarseEquivalence Λ J) :
    ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
      ∃ (R : SimplyConnectedSolvableLieModel) (Δ : Subgroup R.carrier),
        IsUniformLattice Δ ∧ Nonempty (Γ ≃* Δ) := by
…

    Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.GroupCoarseEquivalence