Poincaré's polygon theorem

Let σ be a side pairing of a convex hyperbolic polygon P, whose vertices may be finite or ideal, and let Γ be the subgroup of PSL(2, ℝ) generated by the side-pairing maps. Suppose that every finite vertex cycle satisfies the angle condition: its cycle transformation has finite order m, and the interior angles of P along the cycle add up to 2π / m. Suppose also that the cycle transformation of every ideal vertex is parabolic. Then

• Γ is a cofinite Fuchsian group, in particular discrete;
• P is a measurable fundamental domain for Γ in the sense of MeasureTheory.IsFundamentalDomain: its translates cover the upper half-plane up to a null set, and distinct translates overlap only in a null set;
• Γ is presented by generators indexed by the sides, subject to the side relations map (pair i) * map i = 1 and the cycle relations cycleWord j ^ m = 1 at the finite vertices.

The theorems state the angle condition as orderOf (cycleMap j) * cycleAngleSum j = 2 * π. This is equivalent to the classical form, that the angles along the cycle add up to 2π / t for some positive integer t: such a t is the order of the cycle transformation (ConvexPolygon.SidePairing.orderOf_cycleMap_of_cycleAngleSum).

The cycle conditions make the tiles predicted by the side pairings a local tiling of the upper half-plane with uniform charts, and the theorem follows from the global tessellation theorem for local tilings. The exact tessellation is proved along the way: the translates of P form a locally finite family (ConvexPolygon.SidePairing.locallyFinite_smul_carrier_of_isParabolic), so they cover the upper half-plane (ConvexPolygon.SidePairing.iUnion_smul_carrier_eq_univ), and distinct translates of its interior are disjoint (ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_of_isParabolic). Conversely, the cycle conditions hold for every locally finite fundamental polygon (ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_and_locallyFinite_iff).

Main results

• ConvexPolygon.SidePairing.isFundamentalDomain_carrier_of_isParabolic: P is a measurable fundamental domain for the group generated by the side-pairing maps.
• ConvexPolygon.SidePairing.isCofinite_of_isParabolic: this group is a cofinite Fuchsian group.
• ConvexPolygon.SidePairing.relatorQuotientTo_bijective_of_isParabolic: this group is presented by the side and cycle relations.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.8 (Poincaré's theorem).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §4.3.
• Bernard Maskit, On Poincaré's theorem for fundamental polygons, Adv. Math. 7 (1971), 219–230.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isFundamentalDomain_carrier_of_isParabolic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) : MeasureTheory.IsFundamentalDomain (↥(Subgroup.closure (Set.range σ.map))) P.carrier MeasureTheory.volume

The fundamental-set part of Poincaré's polygon theorem. If a side-paired polygon satisfies the angle condition at every finite vertex cycle and has parabolic cycle transformations at its ideal vertices, then it is a measurable fundamental domain for the group generated by its side-pairing maps.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite_of_isParabolic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) : (Subgroup.closure (Set.range σ.map)).IsCofinite

The discreteness part of Poincaré's polygon theorem. If a side-paired polygon satisfies the angle condition at every finite vertex cycle and has parabolic cycle transformations at its ideal vertices, then the group generated by its side-pairing maps is a cofinite Fuchsian group: it is discrete and has finite covolume.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective_of_isParabolic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) : Function.Bijective ⇑(σ.relatorQuotientTo ⋯)

The presentation part of Poincaré's polygon theorem. If a side-paired polygon satisfies the angle condition at every finite vertex cycle and has parabolic cycle transformations at its ideal vertices, then evaluating the side generators at the side-pairing maps is an isomorphism from the group presented by the side relations and the finite vertex cycle relations onto the group generated by the side-pairing maps.