Displacements and commutator traces in SL(2, ℝ)

For g = !![a, b; c, d] ∈ SL(2, ℝ) the hyperbolic distance moved by the base point I is determined by the sum of the squares of the entries: cosh (dist (g • I) I) = (a² + b² + c² + d²) / 2.

From this we compute two quantities attached to an element g fixing a point z ∈ ℍ, that is, an elliptic element or ±1. Write κ = (4 - tr² g) / 2, so that κ = 2 sin² θ when g acts as the rotation through angle 2θ about z.

• Displacement. g moves a point w a distance δ with cosh δ = 1 + κ sinh² (dist w z). This is the hyperbolic law of cosines for the isosceles triangle z, w, g • w.
• Commutator trace. For every h ∈ SL(2, ℝ), tr ⁅g, h⁆ = 2 + κ (cosh (dist (h • z) z) - 1).

Both are proved by conjugating z to I, where g becomes !![a, b; -b, a] with a² + b² = 1. They are the computations behind Jørgensen's inequality for elliptic elements.

For arbitrary g, h ∈ SL(2, ℝ) and z ∈ ℍ, the displacements δ_g = dist (g • z) z and δ_h = dist (h • z) z bound the traces appearing in Jørgensen's inequality:

• tr² g - 4 ≤ 2 (cosh δ_g - 1);
• |tr ⁅g, h⁆ - 2| ≤ 4 (cosh δ_g cosh δ_h - 1).

At z = I, write g = p + q J + r S₁ + s S₂ with J the rotation generator and S₁, S₂ the traceless symmetric matrices !![1, 0; 0, -1] and !![0, 1; 1, 0]. Then cosh δ_g = 1 + 2 (r² + s²), and tr ⁅g, h⁆ - 2 = -det (g h - h g) is 4 ((q' s - q s')² + (q r' - q' r)² - (r s' - s r')²), which vanishes when both elements are rotations about I. These bounds feed the Margulis lemma for Fuchsian groups.

Two further computations concern elements translating along the imaginary axis or reversing it. The dilation z ↦ exp s * z moves z a distance δ with cosh δ = 1 + (cosh s - 1) (1 + (Re z / Im z)²); the quantity 1 + (Re z / Im z)² is cosh² ρ for the distance ρ from z to the axis. An antidiagonal matrix !![0, b; c, 0], which exchanges the endpoints 0 and ∞ of the axis, moves z a distance δ with cosh δ ≥ 1 + 2 (Re z / Im z)², that is δ ≥ 2 ρ. Thus points far from the axis are moved far by both kinds of element, except by dilations with s close to 0.

Main results

• Matrix.SpecialLinearGroup.cosh_dist_smul_I: the distance moved by I.
• Matrix.SpecialLinearGroup.cosh_dist_smul_of_smul_eq_self: the displacement of a point by an element fixing z.
• Matrix.SpecialLinearGroup.cosh_dist_dilation_smul: the displacement of a point by a dilation, at least |s| by Matrix.SpecialLinearGroup.abs_le_dist_dilation_smul.
• Matrix.SpecialLinearGroup.abs_le_dist_conj_dilation_smul, Matrix.SpecialLinearGroup.dist_conj_dilation_smul_smul_I: the same for a conjugate σ (z ↦ exp s * z) σ⁻¹ in PSL(2, ℝ), translating along the geodesic through σ • I.
• Matrix.SpecialLinearGroup.one_add_two_mul_sq_le_cosh_dist_smul: a lower bound for the displacement of a point by an antidiagonal matrix.
• Matrix.SpecialLinearGroup.trace_commutatorElement_of_smul_eq_self: the trace of a commutator with an element fixing z.
• Matrix.SpecialLinearGroup.trace_sq_sub_four_le: the trace of an element is controlled by the distance it moves any point.
• Matrix.SpecialLinearGroup.abs_trace_commutatorElement_sub_two_le: the trace of a commutator is controlled by the distances its two factors move a common point.
• Matrix.ProjectiveSpecialLinearGroup.dist_smul_le_dist_smul_of_smul_eq_self: two elements fixing a common point compare their displacements in the same way at every point.
• Matrix.ProjectiveSpecialLinearGroup.isBounded_setOf_dist_smul_le_of_smul_eq_self: a nontrivial element fixing a point moves only a bounded set of points a bounded distance.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 7 (the hyperbolic metric and the trigonometry of hyperbolic triangles).

theorem Matrix.SpecialLinearGroup.cosh_dist_smul_I (g : SpecialLinearGroup (Fin 2) ℝ) : Real.cosh (dist (g • UpperHalfPlane.I) UpperHalfPlane.I) = (↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 + ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2) / 2

The distance moved by I. For g = !![a, b; c, d] ∈ SL(2, ℝ), cosh (dist (g • I) I) = (a² + b² + c² + d²) / 2.

theorem Matrix.SpecialLinearGroup.cosh_dist_smul_of_smul_eq_self {g : SpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hz : g • z = z) (w : UpperHalfPlane) : Real.cosh (dist (g • w) w) = 1 + (4 - (↑g).trace ^ 2) / 2 * Real.sinh (dist w z) ^ 2

Displacement by an element fixing a point. If g ∈ SL(2, ℝ) fixes z ∈ ℍ, it moves every w ∈ ℍ a hyperbolic distance δ with cosh δ = 1 + (4 - tr² g) / 2 · sinh² (dist w z). For g acting as the rotation through angle 2θ about z this is cosh δ = 1 + 2 sin² θ sinh² (dist w z).

theorem Matrix.SpecialLinearGroup.trace_commutatorElement_of_smul_eq_self {g : SpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hz : g • z = z) (h : SpecialLinearGroup (Fin 2) ℝ) : (↑⁅g, h⁆).trace = 2 + (4 - (↑g).trace ^ 2) / 2 * (Real.cosh (dist (h • z) z) - 1)

The trace of a commutator with an element fixing a point. If g ∈ SL(2, ℝ) fixes z ∈ ℍ, then for every h ∈ SL(2, ℝ), tr ⁅g, h⁆ = 2 + (4 - tr² g) / 2 · (cosh (dist (h • z) z) - 1).

theorem Matrix.SpecialLinearGroup.two_lt_trace_commutatorElement_of_smul_eq_self {g h : SpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hz : g • z = z) (hg : ↑g ≠ 1) (hh : h • z ≠ z) : 2 < (↑⁅g, h⁆).trace

The commutator of a noncentral element fixing z with an element moving z is hyperbolic, with trace strictly greater than two.

Bounds from the displacement of a point

theorem Matrix.SpecialLinearGroup.trace_sq_sub_four_le (g : SpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) : (↑g).trace ^ 2 - 4 ≤ 2 * (Real.cosh (dist (g • z) z) - 1)

The trace of an element and the displacement of a point. For g ∈ SL(2, ℝ) and z ∈ ℍ, tr² g - 4 ≤ 2 (cosh (dist (g • z) z) - 1). In particular an element moving some point a small distance has trace close to ±2 unless it is elliptic.

theorem Matrix.SpecialLinearGroup.abs_trace_commutatorElement_sub_two_le (g h : SpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) : |(↑⁅g, h⁆).trace - 2| ≤ 4 * (Real.cosh (dist (g • z) z) * Real.cosh (dist (h • z) z) - 1)

The commutator trace and the displacement of a point. For g, h ∈ SL(2, ℝ) and z ∈ ℍ, |tr ⁅g, h⁆ - 2| ≤ 4 (cosh (dist (g • z) z) cosh (dist (h • z) z) - 1). Thus two elements both moving a common point a small distance have commutator trace close to 2, whatever their rotational parts are.

theorem Matrix.SpecialLinearGroup.cosh_dist_dilation_smul (s : ℝ) (z : UpperHalfPlane) : Real.cosh (dist (dilation s • z) z) = 1 + (Real.cosh s - 1) * (1 + (z.re / z.im) ^ 2)

Displacement by a dilation. The dilation z ↦ exp s * z moves z ∈ ℍ a hyperbolic distance δ with cosh δ = 1 + (cosh s - 1) (1 + (Re z / Im z)²). In particular it moves every point of the imaginary axis the distance |s|, and every other point at least as far.

theorem Matrix.SpecialLinearGroup.abs_le_dist_dilation_smul (s : ℝ) (z : UpperHalfPlane) : |s| ≤ dist (dilation s • z) z

The dilation z ↦ exp s * z moves every point of ℍ at least the distance |s|.

@[simp]

theorem Matrix.SpecialLinearGroup.dist_dilation_smul_I (s : ℝ) : dist (dilation s • UpperHalfPlane.I) UpperHalfPlane.I = |s|

The dilation z ↦ exp s * z moves I exactly the distance |s|.

theorem Matrix.SpecialLinearGroup.abs_le_dist_conj_dilation_smul (σ : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) (z : UpperHalfPlane) : |s| ≤ dist ((σ * ↑(dilation s) * σ⁻¹) • z) z

A conjugate σ (z ↦ exp s * z) σ⁻¹ in PSL(2, ℝ) moves every point of ℍ at least the distance |s|.

theorem Matrix.SpecialLinearGroup.dist_conj_dilation_smul_smul_I (σ : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) : dist ((σ * ↑(dilation s) * σ⁻¹) • σ • UpperHalfPlane.I) (σ • UpperHalfPlane.I) = |s|

A conjugate σ (z ↦ exp s * z) σ⁻¹ in PSL(2, ℝ) moves σ • I exactly the distance |s|.

theorem Matrix.SpecialLinearGroup.one_add_two_mul_sq_le_cosh_dist_smul {g : SpecialLinearGroup (Fin 2) ℝ} (h₀₀ : ↑g 0 0 = 0) (h₁₁ : ↑g 1 1 = 0) (z : UpperHalfPlane) : 1 + 2 * (z.re / z.im) ^ 2 ≤ Real.cosh (dist (g • z) z)

Displacement by an antidiagonal matrix. A matrix g = !![0, b; c, 0] ∈ SL(2, ℝ), acting as z ↦ -b² / z and so exchanging the endpoints 0 and ∞ of the imaginary axis, moves z ∈ ℍ a hyperbolic distance δ with cosh δ ≥ 1 + 2 (Re z / Im z)².

theorem Matrix.ProjectiveSpecialLinearGroup.dist_smul_le_dist_smul_of_smul_eq_self {g k : ProjectiveSpecialLinearGroup (Fin 2) ℝ} {w y₀ : UpperHalfPlane} (hg : g • w = w) (hk : k • w = w) (hy₀ : y₀ ≠ w) (h : dist (g • y₀) y₀ ≤ dist (k • y₀) y₀) (y : UpperHalfPlane) : dist (g • y) y ≤ dist (k • y) y

Elements fixing a common point compare their displacements uniformly. If g, k ∈ PSL(2, ℝ) fix w ∈ ℍ and g moves some point y₀ ≠ w at most as far as k does, then g moves every point of ℍ at most as far as k does. Indeed each of them moves y a distance δ with cosh δ = 1 + κ sinh² (dist y w), for a constant κ depending only on the element (Matrix.SpecialLinearGroup.cosh_dist_smul_of_smul_eq_self).

theorem Matrix.ProjectiveSpecialLinearGroup.isBounded_setOf_dist_smul_le_of_smul_eq_self {g : ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg₁ : g ≠ 1) {w : UpperHalfPlane} (hg : g • w = w) (ε : ℝ) : Bornology.IsBounded {y : UpperHalfPlane | dist (g • y) y ≤ ε}

A nontrivial element fixing a point moves far points far. If g ≠ 1 in PSL(2, ℝ) fixes w ∈ ℍ, then the points moved a distance at most ε by g form a bounded set. Indeed g moves y a distance δ with cosh δ = 1 + κ sinh² (dist y w) for a constant κ > 0 (Matrix.SpecialLinearGroup.cosh_dist_smul_of_smul_eq_self).