Intersecting translates of a fundamental polygon

For a side-paired convex hyperbolic polygon with disjoint translated interiors, the translates meeting the polygon in the upper half-plane are exactly the polygon itself, its side neighbours, and the inverse partial cycle tiles around its finite vertices. There are finitely many such translates, even when the polygon has ideal vertices. Intersections only at the ideal boundary are not counted.

Three distinct tiles can meet only at a finite vertex. These pair and triple intersection results supply the geometric generator and relation localization for a presentation obtained from a neighbourhood of the polygon: side intersections involve two adjacent tiles, and triple intersections occur in finite vertex cycles. No local finiteness or discreteness is assumed.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9.
• Svetlana Katok, Fuchsian Groups, Chapter 3.
• A. M. Macbeath, Groups of homeomorphisms of a simply connected space, Ann. of Math. (2) 79 (1964), 473–488.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inter_smul_carrier_nonempty_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) : (P.carrier ∩ g • P.carrier).Nonempty ↔ g = 1 ∨ (∃ (i : Fin n), g = σ.map i) ∨ ∃ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z ∧ ∃ m < orderOf (σ.cycleMap j) * σ.cycleLength j, (σ.partialCycleMap j m)⁻¹ = g

A translate meets the polygon in ℍ exactly when its transformation is the identity, a side-pairing map, or an inverse partial cycle product at a finite vertex before one full turn. Ideal-vertex contacts alone do not give an intersection in ℍ.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.finite_setOf_inter_smul_carrier_nonempty {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ | g ∈ Γ ∧ (P.carrier ∩ g • P.carrier).Nonempty}.Finite

Only finitely many translates of the polygon meet it in ℍ. This also holds for polygons with ideal vertices; it does not assert local finiteness at the ideal boundary.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.exists_vertex_of_mem_carrier_of_mem_two_smul_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) (hh : h ∈ Γ) (hg1 : g ≠ 1) (hh1 : h ≠ 1) (hgh : g ≠ h) {z : UpperHalfPlane} (hz : z ∈ P.carrier) (hzg : z ∈ g • P.carrier) (hzh : z ∈ h • P.carrier) : ∃ (j : Fin n), P.vertex j = Sum.inl z

A common point of the polygon and two distinct nonidentity translates is a finite vertex of the polygon. Thus triple intersections of distinct tiles are localized at vertex cycles.