ConditionalGroupRecognition.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The metric-free group formulation of conditional recognition

For finitely generated groups, GroupCoarseEquivalence expresses the finite-difference control of quasi-isometry in word metrics. The proof constructs the finite word metrics and their linear chains explicitly.

theorem OAI.PolycyclicRecognition.group_recognition_of_published_inputs line 18

Source documentation

Recognition of a finitely generated group coarsely equivalent to a virtually polycyclic group, with no auxiliary metric assumptions.

theorem group_recognition_of_published_inputs
    (inputs : PublishedRecognitionInputs)
    {P J : Type} [Group P] [Group J] [Group.FG P] [Group.FG J]
    (e : GroupCoarseEquivalence P J) (hP : IsVirtuallyPolycyclic P) :
    IsVirtuallyPolycyclic J ∧
      ∃ Γ : Subgroup J, Γ.FiniteIndex ∧
        ∃ (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier),
          IsUniformLattice Λ ∧ Nonempty (Γ ≃* Λ) := by
…

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

theorem OAI.PolycyclicRecognition.uniform_lattice_recognition_of_published_inputs line 47

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_published_inputs
    (inputs : PublishedRecognitionInputs)
    (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.PublishedRecognitionInputs, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.GroupCoarseEquivalence