The Margulis lemma for Fuchsian groups

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup. Two elements of Γ that both move some point z ∈ ℍ a small distance cannot be in general position: if one of them, g, fixes no point of ℍ, then the other, h, conjugates g to itself or to its inverse. Thus h fixes the fixed point of g on the ideal boundary when g is parabolic, and preserves the pair of fixed points of g when g is hyperbolic. This is the Margulis lemma for discrete subgroups of PSL(2, ℝ), in the pairwise form used to describe the thin part of a Fuchsian quotient: the points moved a small distance by some nonidentity element.

The proof combines Jørgensen's inequality Subgroup.one_le_abs_trace_sq_sub_four_add_abs_trace_commutatorElement_sub_two, which bounds |tr² A - 4| + |tr [A, B] - 2| below by 1 outside these exceptional cases, with two upper bounds in terms of the displacements δ_A = dist (A • z) z and δ_B = dist (B • z) z:

• |tr [A, B] - 2| ≤ 4 (cosh δ_A cosh δ_B - 1) (Matrix.SpecialLinearGroup.abs_trace_commutatorElement_sub_two_le), and
• tr² A - 4 ≤ 2 (cosh δ_A - 1) (Matrix.SpecialLinearGroup.trace_sq_sub_four_le).

The first bound holds for all A and B. The second controls |tr² A - 4| only when tr² A ≥ 4, that is when A is not elliptic. An elliptic element rotating through a large angle about a point near z moves z very little while 4 - tr² A stays large, so the general statement keeps |tr² A - 4| as a hypothesis, and the fixed-point-free statement uses the explicit radius 1 / 4.

Main results

• Subgroup.conj_eq_or_conj_eq_inv_of_cosh_dist: if |tr² A - 4| + 4 (cosh δ_A cosh δ_B - 1) < 1, then B A B⁻¹ = A or B A B⁻¹ = A⁻¹.
• Subgroup.smul_eq_self_of_cosh_dist: in the same situation, if A ≠ 1 fixes a point w, then B fixes w as well.
• Subgroup.conj_eq_or_conj_eq_inv_of_dist_le: the Margulis lemma. If g, h ∈ Γ both move z a distance at most 1 / 4 and g fixes no point of ℍ, then h g h⁻¹ = g or h g h⁻¹ = g⁻¹.

References

• Troels Jørgensen, On discrete groups of Möbius transformations, American Journal of Mathematics 98 (1976), 739–749.
• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §5.4 (Jørgensen's inequality and its consequences).
• Riccardo Benedetti and Carlo Petronio, Lectures on Hyperbolic Geometry, Universitext, Springer, 1992, Chapter D (the Margulis lemma and the thick-thin decomposition).

theorem Subgroup.conj_eq_or_conj_eq_inv_of_cosh_dist {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {A B : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hA : ↑A ∈ Γ) (hB : ↑B ∈ Γ) (z : UpperHalfPlane) (h : |(↑A).trace ^ 2 - 4| + 4 * (Real.cosh (dist (A • z) z) * Real.cosh (dist (B • z) z) - 1) < 1) : ↑B * ↑A * (↑B)⁻¹ = ↑A ∨ ↑B * ↑A * (↑B)⁻¹ = (↑A)⁻¹

Two elements moving a point a small distance, in trace form. Let Γ ≤ PSL(2, ℝ) be a discrete subgroup, let A, B ∈ SL(2, ℝ) lift elements of Γ, and let z ∈ ℍ. If |tr² A - 4| + 4 (cosh (dist (A • z) z) cosh (dist (B • z) z) - 1) < 1, then B conjugates the class of A to itself or to its inverse in PSL(2, ℝ).

theorem Subgroup.conj_eq_or_conj_eq_inv_of_dist_le {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) (hh : h ∈ Γ) (hfix : ∀ (w : UpperHalfPlane), g • w ≠ w) {z : UpperHalfPlane} (hgz : dist (g • z) z ≤ 1 / 4) (hhz : dist (h • z) z ≤ 1 / 4) : h * g * h⁻¹ = g ∨ h * g * h⁻¹ = g⁻¹

The Margulis lemma for Fuchsian groups. Let Γ ≤ PSL(2, ℝ) be a discrete subgroup and let g, h ∈ Γ both move a point z ∈ ℍ a distance at most 1 / 4. If g fixes no point of ℍ, that is, if g is parabolic or hyperbolic, then h g h⁻¹ = g or h g h⁻¹ = g⁻¹.

theorem Subgroup.smul_eq_self_of_cosh_dist {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {A B : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : ↑A ∈ Γ) (hk : ↑B ∈ Γ) (hg₁ : ↑A ≠ 1) {w : UpperHalfPlane} (hgw : ↑A • w = w) (y : UpperHalfPlane) (h : |(↑A).trace ^ 2 - 4| + 4 * (Real.cosh (dist (A • y) y) * Real.cosh (dist (B • y) y) - 1) < 1) : ↑B • w = w

Margulis step at an elliptic point. In a discrete Γ ≤ PSL(2, ℝ), if a nonidentity A ∈ Γ fixes w and B ∈ Γ is such that the Margulis inequality holds at some point y, then B fixes w as well, since it conjugates A to A or A⁻¹.