Fundamental polygons of Fuchsian groups

Let σ be a side pairing of a convex hyperbolic polygon P, whose vertices may be finite or ideal, and let Γ ≤ PSL(2, ℝ) contain the side-pairing maps. Suppose that the translates γ • P, γ ∈ Γ, form a locally finite family and that distinct translates of the interior of P are disjoint. These are the tessellation hypotheses of Poincaré's polygon theorem. Then the carrier of P is a measurable fundamental domain for Γ: the translates cover ℍ, and two of them meet only along the boundary of P, a finite union of geodesic pieces, which is null.

Consequently Γ is a cofinite Fuchsian group, and its covolume is the hyperbolic area of P, given by the Gauss–Bonnet formula (n - 2) π - ∑ αᵢ in terms of the number n of vertices and the interior angles αᵢ, an ideal vertex contributing angle 0. This is the area of the quotient Γ \ ℍ read off from a fundamental polygon.

Main results

Under interior disjointness, local finiteness is equivalent to the parabolic cycle condition at every ideal vertex. In one direction local finiteness excludes a hyperbolic ideal cycle. In the other, each ideal vertex is a cusp, and compact truncation together with uniform local cusp height bounds proves local finiteness. Thus parabolic cycles supply the tessellation hypothesis needed by the fundamental-domain and area results, without assuming coverage separately.

• ConvexPolygon.SidePairing.locallyFinite_smul_carrier_iff_isParabolic_cycleMap: local finiteness is equivalent to the ideal cycle transformations being parabolic.
• ConvexPolygon.SidePairing.isFundamentalDomain_carrier: a side-paired polygon with locally finite, interior-disjoint translates is a measurable fundamental domain.
• ConvexPolygon.SidePairing.isCofinite: Γ is a cofinite Fuchsian group.
• ConvexPolygon.SidePairing.covolume_eq: the covolume of Γ is (n - 2) π - ∑ αᵢ.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 9 (locally finite fundamental polygons).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§3.1 and 4.1 (fundamental regions, and the area of Γ \ ℍ as the area of a fundamental region).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.locallyFinite_smul_carrier_iff_isParabolic_cycleMap {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hcycle : ∀ (i : Fin n), (P.vertex i).isRight = true → σ.cycleMap i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : (LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) ↔ ∀ (i : Fin n), (P.vertex i).isRight = true → (σ.cycleMap i).IsParabolic

For a side-paired convex polygon whose ideal vertex cycle transformations lie in Γ and whose translated interiors are disjoint, the translates are locally finite exactly when every ideal vertex cycle transformation is parabolic. No local finiteness, discreteness, or coverage assumption is needed for the reverse implication.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isFundamentalDomain_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : MeasureTheory.IsFundamentalDomain (↥Γ) P.carrier MeasureTheory.volume

A locally finite side-paired polygon with disjoint translated interiors is a fundamental domain. If a subgroup Γ of PSL(2, ℝ) contains every side-pairing map, its translates of the polygon are locally finite, and distinct translates of the interior are disjoint, then the polygon is a measurable fundamental domain for Γ.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Γ.IsCofinite

A group with a fundamental polygon is cofinite. Under the hypotheses of isFundamentalDomain_carrier, the subgroup Γ is discrete and Γ \ ℍ has finite area.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.covolume_eq {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : MeasureTheory.covolume (↥Γ) UpperHalfPlane MeasureTheory.volume = ENNReal.ofReal ((↑n - 2) * Real.pi - ∑ i : Fin n, P.interiorAngle i)

The covolume of a group with a fundamental polygon. Under the hypotheses of isFundamentalDomain_carrier, the hyperbolic area of Γ \ ℍ is (n - 2) π minus the sum of the interior angles of the polygon, the angle at an ideal vertex being 0.