Documentation

TauCeti.Analysis.Complex.Fuchsian.DirichletDomain.Polygon

Dirichlet polygons of Fuchsian groups with cusps #

Let Γ ≤ PSL(2, ℝ) be discrete. If the Dirichlet domain of Γ centred at p becomes bounded after removing finitely many cusp horodiscs, then it is the carrier of a convex polygon, possibly with ideal vertices, and every ideal vertex is the point of one of the cusp data (Subgroup.exists_convexPolygon_carrier_eq_dirichletDomain_of_isBounded_truncation). The sides of such a polygon are Dirichlet faces, by ConvexPolygon.exists_side_eq_dirichletFace, and for a centre with trivial stabilizer it has a unique side pairing by elements of Γ, by ConvexPolygon.existsUnique_sidePairing_of_carrier_eq_dirichletDomain.

Since a Dirichlet domain meets every orbit, the cusp compactification of Γ is then compact as soon as Γ has finitely many cusp orbits (Subgroup.compactSpace_compactifiedQuotient_of_isBounded_truncation).

References #

theorem Subgroup.exists_convexPolygon_carrier_eq_dirichletDomain_of_isBounded_truncation (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ] {ι : Type u_1} [Finite ι] (p : UpperHalfPlane) (D : ι → Γ.CuspDatum) {A : ι → ℝ} (hA : ∀ (i : ι), 0 < A i) (hb : Bornology.IsBounded (TauCeti.dirichletDomain (↥Γ) p \ ⋃ (i : ι), TauCeti.Subgroup.CuspDatum.horodisc (D i) (A i))) :
∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.ConvexPolygon n), P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧ ∀ (i : Fin n) (c : OnePoint ℝ), P.vertex i = Sum.inr c → ∃ (j : ι), (D j).cusp = c

Dirichlet polygons with cusps. If the Dirichlet domain of a discrete subgroup Γ centred at p is bounded after removing finitely many cusp horodiscs of positive heights, it is the carrier of a convex polygon, possibly with ideal vertices. Each ideal vertex is the cusp point of one of the cusp data.

Compactness from a Dirichlet domain with a bounded cusp truncation. If a discrete subgroup Γ has finitely many cusp orbits, and some Dirichlet domain of Γ is bounded after removing finitely many cusp horodiscs of positive heights, then the quotient Γ \ ℍ with its cusp orbits adjoined is compact.