Locally finite tessellations by a side-paired polygon

Let σ be a side pairing of a convex hyperbolic polygon P, and let Γ ≤ PSL(2, ℝ) contain the side-pairing maps. If the translates γ • P with γ ∈ Γ form a locally finite family, they cover the upper half-plane. Near a point of P other than a vertex, P and the translates of P by the side-pairing maps contain a neighbourhood, so the union of all translates is a neighbourhood of each of its points off the countably many translated vertices. Local finiteness makes the union closed, and the complement of a countable set in ℍ is connected and dense; hence the union is everything. No angle or cycle condition enters, and the vertices may be finite or ideal.

If moreover distinct translates of the interior of P are disjoint, then P is a fundamental polygon for Γ, and Γ is generated by the side-pairing maps: an element of Γ carries an interior point of P into a translate by the generated subgroup, and disjointness of interiors forces the two elements to agree.

These are the covering half of the fundamental-set theorem in Poincaré's polygon theorem, whose hypotheses include local finiteness and no overlap of the translated interiors, and the statement that the side pairings of a locally finite fundamental polygon generate the group, which is the first step in reading off the presentation of Γ from the polygon.

Main results

• ConvexPolygon.SidePairing.mem_interior_carrier_union_iUnion_smul_carrier: the polygon and its paired translates contain a neighbourhood of each of its points other than a vertex.
• ConvexPolygon.SidePairing.iUnion_smul_carrier_eq_univ: locally finite translates by a group containing the side-pairing maps cover the upper half-plane.
• ConvexPolygon.eq_of_smul_interior_inter_smul_carrier_nonempty: when distinct translated interiors are disjoint, two translates one of whose interiors meets the other are equal.
• ConvexPolygon.SidePairing.closure_range_map_eq: the side-pairing maps generate the group of a locally finite fundamental polygon.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 9 (locally finite fundamental polygons, side pairings, and Poincaré's theorem).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, Chapter 3 (fundamental regions and generators of Fuchsian groups).
• Bernard Maskit, On Poincaré's theorem for fundamental polygons, Adv. Math. 7 (1971), 219–230.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.eq_of_smul_interior_inter_smul_carrier_nonempty {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {g g' : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) (hg' : g' ∈ Γ) (h : (g • interior P.carrier ∩ g' • P.carrier).Nonempty) : g = g'

Overlapping translates of a polygon with disjoint translated interiors coincide. Let distinct translates of the interior of P by Γ be disjoint. If the interior of a translate g • P meets a translate g' • P, with g, g' ∈ Γ, then g = g'.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_carrier_union_iUnion_smul_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {z : UpperHalfPlane} (hz : z ∈ P.carrier) (hv : ∀ (i : Fin n), P.vertex i ≠ Sum.inl z) : z ∈ interior (P.carrier ∪ ⋃ (i : Fin n), σ.map i • P.carrier)

Near a point of the polygon other than a vertex, the polygon and its translates by the side-pairing maps together contain a neighbourhood.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.iUnion_smul_carrier_eq_univ {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ

Locally finite translates of a side-paired polygon cover ℍ. If a subgroup Γ of PSL(2, ℝ) contains every side-pairing map and its translates of the polygon form a locally finite family, then these translates cover the upper half-plane.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.closure_range_map_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)) : Subgroup.closure (Set.range σ.map) = Γ

The side pairings generate the group of a locally finite fundamental polygon. Let a subgroup Γ of PSL(2, ℝ) contain every side-pairing map, let its translates of the polygon be locally finite, and let distinct translates of the interior be disjoint. Then Γ is generated by the side-pairing maps.