Finite descriptions of cusp-truncated Dirichlet domains

If a Dirichlet domain of a discrete Fuchsian group is bounded outside finitely many cusp horodiscs of positive heights, it is globally defined by finitely many distance inequalities. These inequalities are the closed geodesic half-planes bounded by perpendicular bisectors of the centre and its translates. This supplies the finite intersection needed to construct the Dirichlet polygon, including domains with unbounded cusp ends.

Boundedness of the truncation is independent of its positive heights: the constraints from a cusp generator bound the horizontal coordinate, so changing a height only adds bounded bands. The finite constraints on the bounded core and the cusp ends agree with the domain on an open neighbourhood. Geodesic convexity then gives equality globally, via UpperHalfPlane.dirichletDomain_eq_iInter_of_inter_eq.

No finite-area hypothesis is used, and no assertion that finite area alone provides a bounded truncation is made. The cusp data need not have distinct cusp orbits, and the index type may be empty, in which case the hypothesis is boundedness of the whole domain.

References

• Alan Beardon, The Geometry of Discrete Groups, §9.4.
• Svetlana Katok, Fuchsian Groups, §§3.2 and 4.2.

We combine TauCeti.exists_finset_dirichletDomain_inter_eq with TauCeti.Subgroup.CuspDatum.exists_finset_dirichletDomain_inter_horodisc_eq.

theorem Subgroup.isBounded_dirichletDomain_diff_iUnion_horodisc (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) {ι : 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))) (B : ι → ℝ) : Bornology.IsBounded (TauCeti.dirichletDomain (↥Γ) p \ ⋃ (i : ι), TauCeti.Subgroup.CuspDatum.horodisc (D i) (B i))

A bounded truncation of a Dirichlet domain at positive cusp heights remains bounded after changing any of the heights. The new heights need not be positive.

theorem Subgroup.exists_finset_dirichletDomain_eq_iInter_closure_leftHalfPlane_of_isBounded_truncation (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) {ι : Type u_1} [Finite ι] [DiscreteTopology ↥Γ] (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))) : ∃ (s : Finset ↥Γ), (∀ g ∈ s, p ≠ g • p) ∧ TauCeti.dirichletDomain (↥Γ) p = ⋂ g ∈ s, _root_.closure (TauCeti.UpperHalfPlane.leftHalfPlane (TauCeti.UpperHalfPlane.perpBisector p (g • p)))

If a Dirichlet domain has a bounded truncation outside finitely many cusp horodiscs of positive heights, finitely many of its distance inequalities define it on all of ℍ. The result omits elements fixing the centre and expresses the remaining constraints as closed geodesic half-planes. Neither a trivial centre stabilizer nor distinct cusp data is required.