Cusp orbits extracted from a fundamental polygon

Let σ pair the sides of a convex hyperbolic polygon P, and let Γ ≤ PSL(2, ℝ) contain the side-pairing maps, with locally finite translates of P whose interiors are pairwise disjoint. Then the cusp orbits of Γ are exactly the ideal vertex cycles of P: every ideal vertex is a cusp point, every cusp point is Γ-equivalent to an ideal vertex, and two ideal vertices are Γ-equivalent exactly when they lie in the same cycle.

The classification is an equivalence with the actual cusp-orbit subtype Subgroup.CuspOrbit of the boundary quotient, sending a cycle to the orbit of any of its vertices. It supplies the number of cusps in an orbifold signature, complementing the classification of elliptic orbits in ConvexPolygon.SidePairing.ellipticOrbitEquiv. Compactness and finite covolume are not additional hypotheses.

Main results

• ConvexPolygon.SidePairing.idealVertexCycleEquiv: ideal vertex cycles are in bijection with cusp orbits.
• ConvexPolygon.SidePairing.coe_idealVertexCycleEquiv_mk: a cycle goes to the orbit of its vertex.
• ConvexPolygon.SidePairing.natCard_cuspOrbit: the number of cusp orbits is the number of ideal vertex cycles.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9 (cycles of vertices at infinity).
• Svetlana Katok, Fuchsian Groups, §4.2 (cusps and vertices at infinity of a fundamental region).

The surjectivity is ConvexPolygon.SidePairing.exists_vertex_eq_inr_smul_of_isCuspPoint; the injectivity is ConvexPolygon.SidePairing.mem_orbit_iff_mem_cycle_of_vertex_eq_inr, applied with the parabolic cycle transformations given by local finiteness.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.idealVertexCycleEquiv {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)) : σ.IdealVertexCycle ≃ Γ.CuspOrbit

The cusp orbits of a locally finite fundamental polygon are its ideal vertex cycles. Let Γ contain the side-pairing maps, with locally finite translates of P whose interiors are pairwise disjoint. Sending an ideal vertex to its boundary orbit identifies the same-cycle quotient of the ideal vertices with the cusp orbits of Γ.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.coe_idealVertexCycleEquiv_mk {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)) (j : { i : Fin n // (P.vertex i).isRight = true }) : ↑((σ.idealVertexCycleEquiv hmap hlf hdisj) (Quotient.mk'' j)) = Quotient.mk'' ((P.vertex ↑j).getRight ⋯)

The cycle of an ideal vertex is sent to the boundary orbit of that vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_cuspOrbit {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)) : Nat.card Γ.CuspOrbit = Nat.card σ.IdealVertexCycle

The number of cusps of a locally finite fundamental polygon. The number of cusp orbits of Γ is the number of ideal vertex cycles of P.