Dirichlet polygons of cofinite Fuchsian groups

Let Γ ≤ PSL(2, ℝ) be cofinite and p ∈ ℍ. This file shows that the Dirichlet domain of Γ centred at p becomes bounded after removing finitely many cusp horodiscs. Consequently it is the carrier of a finite-sided convex polygon whose ideal vertices are cusp points of Γ, and, if p has trivial stabilizer, this polygon carries a side pairing by elements of Γ. Conversely, the area of a convex polygon with finitely many vertices is finite by the Gauss–Bonnet formula, so a discrete group is cofinite exactly when one (equivalently, every) Dirichlet domain centred at a point with trivial stabilizer is such a polygon. Its translates are locally finite with disjoint interiors, so its side pairing satisfies the hypotheses of Poincaré's polygon theorem, generates Γ, and presents it.

The bounded truncation also gives compactness of the cusp compactification of Γ: the polygon minus cusp horodiscs is a compact set meeting every orbit outside the corresponding cusp neighbourhoods, and there are finitely many cusp orbits.

Fix δ > 0 so that every element of Γ moving some point less than δ fixes a point of ℍ or is parabolic (Subgroup.IsCofinite.exists_pos_exists_smul_eq_or_isParabolic_of_dist_smul_lt). A point of the Dirichlet domain lies in one of three parts.

• Thick part. The points moved at least δ by every nonidentity element form a bounded part of the domain, by a packing argument (Subgroup.IsCofinite.isBounded_dirichletDomain_inter_thickPart).
• Elliptic part. A nonidentity element fixing a point w moves only a bounded set of points less than δ. There are finitely many elliptic orbits (Subgroup.IsCofinite.finite_ellipticOrbits), and each stabilizer is finite, so the points moved less than δ by a nonidentity element fixing a point lie in the Γ-orbit of a bounded set. Its intersection with the Dirichlet domain is bounded, because a point of the domain is the point of its orbit closest to p (Subgroup.isBounded_dirichletDomain_inter_setOf_dist_smul_le).
• Parabolic part. A parabolic element fixes a cusp point. There are finitely many cusp orbits (Subgroup.IsCofinite.finite_cuspOrbit), and for a cusp datum of each of them the points of the domain moved less than δ by a parabolic element fixing a cusp of that orbit lie in finitely many translates of a horodisc, apart from a bounded set, by the lemma CuspDatum.exists_finset_isBounded_dirichletDomain_inter_setOf_dist_smul_lt_diff. The translate of a horodisc by an element of Γ is a horodisc of the transported cusp datum.

No hypothesis that Γ is non-elementary is needed, and the centre p is arbitrary except where the side pairing and the characterization of cofiniteness are concerned.

Main results

• Subgroup.IsCofinite.exists_isBounded_dirichletDomain_diff_iUnion_horodisc: a Dirichlet domain of a cofinite group is bounded outside finitely many cusp horodiscs.
• Subgroup.IsCofinite.exists_convexPolygon_carrier_eq_dirichletDomain: a Dirichlet domain of a cofinite group is a finite-sided convex polygon whose ideal vertices are cusp points.
• Subgroup.IsCofinite.compactSpace_compactifiedQuotient: the cusp compactification of a cofinite group is compact.
• Subgroup.IsCofinite.exists_sidePairing_of_mem_freeLocus: for a centre with trivial stabilizer this polygon has a side pairing by elements of Γ.
• Subgroup.isCofinite_iff_exists_convexPolygon_carrier_eq_dirichletDomain: a discrete group is cofinite exactly when its Dirichlet domain at a point with trivial stabilizer is a finite-sided convex polygon.
• Subgroup.IsCofinite.exists_sidePairing_closure_range_map_eq: the converse of Poincaré's polygon theorem; the side pairing of this polygon generates Γ and satisfies the angle condition at finite vertex cycles and the parabolic condition at ideal vertex cycles.
• Subgroup.IsCofinite.exists_sidePairing_relatorQuotientTo_bijective: Γ is presented by the side pairing of this polygon.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §§9.4 and 10.1 (geometrically finite groups; finite area implies finitely many sides) and §9.8 (Poincaré's theorem; the side pairing of a Dirichlet polygon generates and presents the group).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, Theorem 4.1.1 (Siegel's theorem), §4.2, and §4.3 (the converse of Poincaré's theorem and the presentation by side pairings).
• Riccardo Benedetti and Carlo Petronio, Lectures on Hyperbolic Geometry, Universitext, Springer, 1992, Chapter D (the thick-thin decomposition of a finite-volume hyperbolic manifold).

theorem Subgroup.IsCofinite.exists_isBounded_dirichletDomain_diff_iUnion_horodisc {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) (p : UpperHalfPlane) : ∃ (n : ℕ) (D : Fin n → Γ.CuspDatum) (A : Fin n → ℝ), (∀ (i : Fin n), 0 < A i) ∧ Bornology.IsBounded (TauCeti.dirichletDomain (↥Γ) p \ ⋃ (i : Fin n), TauCeti.Subgroup.CuspDatum.horodisc (D i) (A i))

Dirichlet domains of cofinite groups have bounded cusp truncations. For a cofinite Γ ≤ PSL(2, ℝ) and any centre p, the Dirichlet domain of Γ centred at p is bounded after removing finitely many horodiscs of cusp data of Γ, at positive heights.

theorem Subgroup.IsCofinite.compactSpace_compactifiedQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (hΓ : Γ.IsCofinite) : CompactSpace Γ.CompactifiedQuotient

Compactness for cofinite groups. For a cofinite Γ ≤ PSL(2, ℝ), the quotient Γ \ ℍ with its finitely many cusp orbits adjoined is compact. Together with Subgroup.CompactifiedQuotient.instT2Space and Subgroup.CompactifiedQuotient.instSecondCountableTopology, it is a compact Hausdorff second-countable space. The discreteness instance is part of Γ.IsCofinite; it is assumed separately only because the topology on Γ.CompactifiedQuotient is defined from it.

theorem Subgroup.IsCofinite.exists_convexPolygon_carrier_eq_dirichletDomain {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) (p : UpperHalfPlane) : ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.ConvexPolygon n), P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧ ∀ (i : Fin n) (c : OnePoint ℝ), P.vertex i = Sum.inr c → Γ.IsCuspPoint c

Dirichlet polygons of cofinite groups. For a cofinite Γ ≤ PSL(2, ℝ) and any centre p, the Dirichlet domain of Γ centred at p is the carrier of a convex polygon with finitely many vertices, possibly ideal. Every ideal vertex is a cusp point of Γ.

theorem Subgroup.IsCofinite.exists_sidePairing_of_mem_freeLocus {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) : ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.ConvexPolygon n) (σ : P.SidePairing), (∀ (i : Fin n), σ.map i ∈ Γ) ∧ P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧ ∀ (i : Fin n) (c : OnePoint ℝ), P.vertex i = Sum.inr c → Γ.IsCuspPoint c

Side pairings of Dirichlet polygons of cofinite groups. For a cofinite Γ ≤ PSL(2, ℝ) and a centre p with trivial stabilizer, the Dirichlet domain of Γ centred at p is the carrier of a convex polygon with finitely many vertices, whose ideal vertices are cusp points of Γ, and whose sides are paired by elements of Γ. This side pairing is unique, by TauCeti.UpperHalfPlane.ConvexPolygon.existsUnique_sidePairing_of_carrier_eq_dirichletDomain.

theorem Subgroup.IsCofinite.exists_sidePairing_closure_range_map_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) : ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.ConvexPolygon n) (σ : P.SidePairing), P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧ closure (Set.range σ.map) = Γ ∧ (∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) ∧ ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic

The converse of Poincaré's polygon theorem. Every cofinite Γ ≤ PSL(2, ℝ) arises from Poincaré's polygon theorem. For a centre p with trivial stabilizer, the Dirichlet domain of Γ centred at p is the carrier of a convex polygon with finitely many vertices and a side pairing whose maps generate Γ. The cycle transformation of each finite vertex has finite order m and the interior angles along its cycle add up to 2π / m, and the cycle transformation of each ideal vertex is parabolic. These are the hypotheses of TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite_of_isParabolic.

theorem Subgroup.IsCofinite.exists_sidePairing_relatorQuotientTo_bijective {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) : ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.ConvexPolygon n) (σ : P.SidePairing) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ), P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧ Function.Bijective ⇑(σ.relatorQuotientTo hmap)

Dirichlet presentations of cofinite Fuchsian groups. For a cofinite Γ ≤ PSL(2, ℝ) and a centre p with trivial stabilizer, the Dirichlet domain of Γ centred at p is the carrier of a convex polygon with finitely many vertices and a side pairing by elements of Γ, and Γ is presented by the side-pairing maps, subject to the side relations and the finite-vertex cycle relations.

theorem Subgroup.isCofinite_iff_exists_convexPolygon_carrier_eq_dirichletDomain {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) : Γ.IsCofinite ↔ ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.ConvexPolygon n), P.carrier = TauCeti.dirichletDomain (↥Γ) p

Cofiniteness from Dirichlet polygons. A discrete subgroup Γ ≤ PSL(2, ℝ) is cofinite exactly when its Dirichlet domain centred at a point p with trivial stabilizer is the carrier of a convex polygon with finitely many vertices, possibly ideal. The converse direction is the Gauss–Bonnet formula: such a polygon has finite area.