Shimizu's lemma

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup containing the translation z ↦ z + w with w ≠ 0. Shimizu's lemma says that the lower-left entry c of any element of Γ satisfies c = 0 or |c| ≥ |w|⁻¹: the elements of Γ that do not fix ∞ are bounded away from the parabolic ones. Equivalently, in geometric form, an element of Γ that does not fix ∞ satisfies (g • z).im * z.im ≤ w ^ 2 for every z in the upper half-plane, so it cannot map a point high above the real axis to another such point. This is what makes sufficiently high horodiscs at a cusp precisely invariant under the cusp stabilizer.

The proof is Jørgensen's: if w * |c| < 1, the iteration A ↦ A T A⁻¹ starting from a lift A of g, where T = !![1, w; 0, 1], stays in Γ, its lower-left entries satisfy c_{n+1} = -w * c_n ^ 2 and hence tend to 0 very fast, and the whole sequence converges to T. Discreteness forces the sequence to reach T, whose lower-left entry vanishes, while c_{n+1} = -w * c_n ^ 2 keeps every c_n nonzero.

Main results

• Subgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem: Shimizu's lemma in coordinates.
• Subgroup.im_smul_mul_im_le_sq_of_upperRightHom_mem: its geometric form.
• Subgroup.im_smul_mul_im_le_abs_mul_of_upperRightHom_mem: the geometric form for a transformation conjugating a second translation into Γ, which compares the heights above two cusps.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §5.4.
• Hideo Shimizu, On discontinuous groups operating on the product of the upper half planes, Annals of Mathematics 77 (1963), 33–71.

The entries of Jørgensen's iteration

Convergence of the iteration

Shimizu's lemma

theorem Subgroup.inv_le_abs_apply_one_zero_of_upperRightHom_mem {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {w : ℝ} {A : Matrix.SpecialLinearGroup (Fin 2) ℝ} [DiscreteTopology ↥Γ] (hw : w ≠ 0) (hT : Matrix.ProjectiveSpecialLinearGroup.upperRightHom w ∈ Γ) (hA : ↑A ∈ Γ) (hA0 : ↑A 1 0 ≠ 0) : |w|⁻¹ ≤ |↑A 1 0|

Shimizu's lemma. Let Γ ≤ PSL(2, ℝ) be a discrete subgroup containing the translation z ↦ z + w with w ≠ 0, and let A ∈ SL(2, ℝ) lift an element of Γ. If the lower-left entry of A does not vanish, that is, if the element does not fix ∞, then that entry has absolute value at least |w|⁻¹. Both lifts of the element give the same absolute value.

theorem Subgroup.im_smul_mul_im_le_abs_mul_of_upperRightHom_mem {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {w : ℝ} [DiscreteTopology ↥Γ] {w' : ℝ} (hw : w ≠ 0) (hw' : w' ≠ 0) (hT : Matrix.ProjectiveSpecialLinearGroup.upperRightHom w ∈ Γ) {h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hh : h * Matrix.ProjectiveSpecialLinearGroup.upperRightHom w' * h⁻¹ ∈ Γ) (hinf : h • OnePoint.infty ≠ OnePoint.infty) (z : UpperHalfPlane) : (h • z).im * z.im ≤ |w * w'|

Shimizu's lemma for two parabolic fixed points, geometric form. Let Γ ≤ PSL(2, ℝ) be a discrete subgroup containing the translation z ↦ z + w with w ≠ 0, and let h ∈ PSL(2, ℝ) conjugate the translation z ↦ z + w', w' ≠ 0, into Γ. If h does not fix ∞, then (h • z).im * z.im ≤ |w * w'| for every z in the upper half-plane.

Applied to h = σ g σ'⁻¹, where σ and σ' send two cusps of Γ to ∞ and g ∈ Γ, this bounds the heights above two cusps simultaneously; for h ∈ Γ and w' = w it is Subgroup.im_smul_mul_im_le_sq_of_upperRightHom_mem.

theorem Subgroup.im_smul_mul_im_le_sq_of_upperRightHom_mem {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {w : ℝ} [DiscreteTopology ↥Γ] (hw : w ≠ 0) (hT : Matrix.ProjectiveSpecialLinearGroup.upperRightHom w ∈ Γ) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) (hginf : g • OnePoint.infty ≠ OnePoint.infty) (z : UpperHalfPlane) : (g • z).im * z.im ≤ w ^ 2

Shimizu's lemma, geometric form. Let Γ ≤ PSL(2, ℝ) be a discrete subgroup containing the translation z ↦ z + w with w ≠ 0. An element of Γ that does not fix ∞ moves every point z of the upper half-plane to a point with (g • z).im * z.im ≤ w ^ 2; in particular it cannot keep a point of imaginary part greater than |w| that high.