Geodesic convexity of Dirichlet domains

A Dirichlet domain in the upper half-plane is an intersection of closed geodesic half-planes: for each translate of the centre different from the centre itself, the corresponding perpendicular bisector bounds the distance dominance region. Constraints coming from the stabilizer are automatically satisfied and are omitted from this intersection.

Consequently the domain contains the geodesic segment between any two of its points. Neither this convexity nor the half-plane description requires discreteness or a trivial stabilizer. They provide the geometric description of the Dirichlet domain needed to construct its sides.

References

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

theorem TauCeti.UpperHalfPlane.dirichletDomain_eq_iInter_closure_leftHalfPlane (G : Type u_1) [SMul G UpperHalfPlane] (p : UpperHalfPlane) : dirichletDomain G p = ⋂ (g : G), ⋂ (_ : p ≠ g • p), closure (leftHalfPlane (perpBisector p (g • p)))

A Dirichlet domain in ℍ is the intersection of the closed geodesic half-planes bounded by the bisectors between its centre and the distinct points of the orbit of that centre. Translates fixing the centre impose no constraint.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_dirichletDomain (G : Type u_1) [SMul G UpperHalfPlane] {p z w : UpperHalfPlane} (hz : z ∈ dirichletDomain G p) (hw : w ∈ dirichletDomain G p) : z.geodesicSegment w ⊆ dirichletDomain G p

Dirichlet domains in the hyperbolic plane are geodesically convex. This applies to any family of translates, without discreteness, freeness, or isometry assumptions.

theorem TauCeti.UpperHalfPlane.ordConnected_preimage_geodesicLine_dirichletDomain (G : Type u_1) [SMul G UpperHalfPlane] {k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p : UpperHalfPlane} : (geodesicLine k ⁻¹' dirichletDomain G p).OrdConnected

Along any geodesic line the parameters lying in a Dirichlet domain form an interval.