Finite bisector descriptions of bounded Dirichlet domains

A bounded Dirichlet domain for a properly discontinuous action on the upper half-plane is a finite intersection of closed geodesic half-planes. The equality holds on the entire upper half-plane, not merely inside a prescribed bounded set. Constraints indexed by elements fixing the centre are omitted. In particular, an isometric action with compact orbit quotient has such a finite description.

This is the finite-constraint step in constructing compact Dirichlet polygons. It does not assert finite-sidedness for an unbounded finite-area domain, or enumerate the sides and vertices of the finite intersection.

References

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

We use TauCeti.exists_finset_dirichletDomain_inter_eq for local finiteness and the geodesic convexity of distance-dominance regions to obtain global equality.

theorem TauCeti.UpperHalfPlane.exists_finset_dirichletDomain_eq_iInter_closure_leftHalfPlane {G : Type u_1} [SMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {p : UpperHalfPlane} (hb : Bornology.IsBounded (dirichletDomain G p)) : ∃ (s : Finset G), (∀ g ∈ s, p ≠ g • p) ∧ dirichletDomain G p = ⋂ g ∈ s, closure (leftHalfPlane (perpBisector p (g • p)))

A bounded hyperbolic Dirichlet domain is globally cut out by finitely many perpendicular bisectors. The finite family contains only indices moving the centre.

theorem TauCeti.UpperHalfPlane.exists_finset_dirichletDomain_eq_iInter_closure_leftHalfPlane_of_compactSpace (G : Type u_1) [Group G] [MulAction G UpperHalfPlane] [IsIsometricSMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] [CompactSpace (MulAction.orbitRel.Quotient G UpperHalfPlane)] (p : UpperHalfPlane) : ∃ (s : Finset G), (∀ g ∈ s, p ≠ g • p) ∧ dirichletDomain G p = ⋂ g ∈ s, closure (leftHalfPlane (perpBisector p (g • p)))

For a properly discontinuous isometric action with compact orbit space, every hyperbolic Dirichlet domain has a finite closed-half-plane description.