The interior of a polygon as a fundamental set

Let P be a compact convex hyperbolic polygon and let Γ ≤ PSL(2, ℝ). One of the local hypotheses in the Poincaré polygon theorem is that distinct Γ-translates of the interior of P.carrier are disjoint. This file records the two immediate global consequences of that hypothesis. The orbit projection is an open embedding on the polygon interior, and, provided the interior is nonempty, Γ is a discrete subgroup.

These are the injectivity and discreteness parts of the fundamental-set argument. Showing that the translates cover the upper half-plane, and deriving the presentation from side pairings and vertex cycles, require the cycle and angle hypotheses of the Poincaré polygon theorem.

Main results

• CompactConvexPolygon.isOpenEmbedding_quotientMk_domRestrict_interior: the orbit projection restricts to an open embedding on the polygon interior.
• CompactConvexPolygon.discreteTopology_of_disjoint_smul_interior: a subgroup with disjoint translates of a nonempty polygon interior is discrete.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 9.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, Chapter 3.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.isOpenEmbedding_quotientMk_domRestrict_interior {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (γ • interior P.carrier) (interior P.carrier)) : Topology.IsOpenEmbedding ((interior P.carrier).domRestrict Quotient.mk'')

If distinct Γ-translates of the interior of a polygon are disjoint, the orbit projection restricts to an open embedding on that interior. In particular, no two distinct points in the interior are identified in the quotient.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.discreteTopology_of_disjoint_smul_interior {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (hP : (interior P.carrier).Nonempty) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (γ • interior P.carrier) (interior P.carrier)) : DiscreteTopology ↥Γ

Discreteness from polygon-interior no-overlap. A subgroup of PSL(2, ℝ) is discrete if the interior of a polygon is nonempty and disjoint from all of its translates by nonidentity elements of the subgroup. This is the discreteness step in the Poincaré polygon theorem.