Truncating a convex polygon at its ideal vertices

A convex hyperbolic polygon with ideal vertices is not compact: it runs off to the boundary of ℍ at each ideal vertex. This file proves that this is the only way in which it fails to be compact. Removing from the carrier an open horodisc at each ideal vertex, of arbitrary size, leaves a compact set (ConvexPolygon.isCompact_carrier_diff_iUnion).

The set removed at an ideal vertex ξ is described by an element g ∈ PSL(2, ℝ) with g • ξ = ∞ and a real threshold A, as {z | A < Im (g • z)}. For A > 0 this is an open horodisc at ξ; for A ≤ 0 it is all of ℍ, and the theorem then holds trivially, so it is stated for every real A. For a cusp datum of a Fuchsian group this set is the horodisc TauCeti.Subgroup.CuspDatum.horodisc at the cusp, with g the scaling of the datum. This is the compactness of the truncated fundamental polygon that feeds the compactness criterion Subgroup.CompactifiedQuotient.compactSpace_of_compact_truncations for cusp compactifications.

Proof

The statement is invariant under PSL(2, ℝ) and under relabelling the vertices, so either all vertices lie in ℍ, and the carrier is compact already, or vertex 0 is ∞ and the set removed there is {z | A < Im z}. In the second case the carrier lies in a vertical strip, and is the union of the triangles ∞, vertex k, vertex (k + 1) of the fan from ∞, each of them the region above a semicircle of centre m and radius ρ (ConvexPolygon.exists_carrier_inter_strip_eq). Above such a semicircle, between its centre and a finite endpoint p, the height is at least Im p. Between its centre and a real endpoint x it satisfies ρ |Re z - x| ≤ (Im z)², so that a point outside a horodisc at x, where Im z ≤ K |z - x|², has height at least min ρ (1 / (2K)). These two estimates are im_le_im_of_normSq_sub_eq and min_le_im_of_sq_sub_eq. Every truncated triangle therefore lies in a compact rectangle of ℍ.

Main result

• ConvexPolygon.isCompact_carrier_diff_iUnion: a convex polygon minus open horodiscs at its ideal vertices is compact.

References

• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §4.2 (a fundamental region minus cusp neighbourhoods is compact).
• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §2.4.

The truncated carrier

A polygon with an ideal vertex at ∞

The truncation theorem

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isCompact_carrier_diff_iUnion {n : ℕ} [NeZero n] (P : ConvexPolygon n) (g : Fin n → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (hg : ∀ (i : Fin n) (ξ : OnePoint ℝ), P.vertex i = Sum.inr ξ → g i • ξ = OnePoint.infty) (A : Fin n → ℝ) : IsCompact (P.carrier \ ⋃ (i : Fin n), ⋃ (_ : (P.vertex i).isRight = true), {z : UpperHalfPlane | A i < (g i • z).im})

A convex polygon truncated at its ideal vertices is compact. For each ideal vertex vertex i = ξ of a convex polygon P, let g i ∈ PSL(2, ℝ) carry ξ to ∞, and let A i be any real number. For A i > 0 the set {z | A i < Im (g i • z)} is an open horodisc at ξ, and for A i ≤ 0 it is all of ℍ. Then the carrier of P minus these sets is compact. The values of g i and A i at the vertices in ℍ play no role.