Geodesic faces of hyperbolic Dirichlet domains

An equality face whose index moves the centre is the intersection of the Dirichlet domain with the corresponding perpendicular bisector. It is a geodesically convex boundary piece, and its parameters on that bisector form a closed interval. In particular every nonempty bounded face is a geodesic segment, possibly a singleton. This identifies the bounded boundary pieces used as sides and vertices of Dirichlet polygons without assuming finite-sidedness.

The geometric statements apply to any family of translates in the upper half-plane. Proper discontinuity is needed only for the exact boundary and interior characterizations, where it ensures local finiteness of the distance constraints. Indices fixing the centre are explicitly excluded from the boundary description: their equality face is the whole domain.

References

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

The construction uses TauCeti.dirichletFace and the perpendicular-bisector half-plane API.

theorem TauCeti.UpperHalfPlane.dirichletFace_eq_inter_range_geodesicLine {G : Type u_1} [SMul G UpperHalfPlane] {p : UpperHalfPlane} {g : G} (hg : g • p ≠ p) : dirichletFace p g = dirichletDomain G p ∩ Set.range (geodesicLine (perpBisector p (g • p)))

A face indexed by an element moving the centre is cut out by its perpendicular bisector.

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

Equality faces of a hyperbolic Dirichlet domain are geodesically convex, including the whole-domain face of an index fixing the centre.

@[simp]

theorem TauCeti.UpperHalfPlane.preimage_geodesicLine_dirichletFace {G : Type u_1} [SMul G UpperHalfPlane] {p : UpperHalfPlane} {g : G} (hg : g • p ≠ p) : geodesicLine (perpBisector p (g • p)) ⁻¹' dirichletFace p g = geodesicLine (perpBisector p (g • p)) ⁻¹' dirichletDomain G p

On its supporting bisector the face imposes just the Dirichlet-domain inequalities.

theorem TauCeti.UpperHalfPlane.ordConnected_preimage_geodesicLine_dirichletFace {G : Type u_1} [SMul G UpperHalfPlane] {p : UpperHalfPlane} {g : G} (hg : g • p ≠ p) : (geodesicLine (perpBisector p (g • p)) ⁻¹' dirichletFace p g).OrdConnected

The parameters of a nontrivial equality face on its supporting bisector form an interval.

theorem TauCeti.UpperHalfPlane.dirichletFace_subset_frontier {G : Type u_1} [SMul G UpperHalfPlane] {p : UpperHalfPlane} {g : G} (hg : g • p ≠ p) : dirichletFace p g ⊆ frontier (dirichletDomain G p)

A face indexed by an element moving the centre lies on the boundary of the domain. This conclusion does not require discreteness or an isometric group action.

theorem TauCeti.UpperHalfPlane.exists_dirichletFace_eq_geodesicSegment {G : Type u_1} [SMul G UpperHalfPlane] {p : UpperHalfPlane} {g : G} (hg : g • p ≠ p) (hne : (dirichletFace p g).Nonempty) (hb : Bornology.IsBounded (dirichletFace p g)) : ∃ (z : UpperHalfPlane) (w : UpperHalfPlane), dirichletFace p g = z.geodesicSegment w

Every nonempty bounded face whose index moves the centre is an actual geodesic segment. A face consisting of one point is allowed; no positive side length is asserted.

theorem TauCeti.UpperHalfPlane.frontier_dirichletDomain_eq_iUnion_dirichletFace {G : Type u_1} [SMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {p : UpperHalfPlane} : frontier (dirichletDomain G p) = ⋃ (g : { g : G // g • p ≠ p }), dirichletFace p ↑g

The boundary is exactly the union of the faces indexed by elements moving the centre.

@[simp]

theorem TauCeti.UpperHalfPlane.mem_interior_dirichletDomain_iff {G : Type u_1} [SMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {p z : UpperHalfPlane} : z ∈ interior (dirichletDomain G p) ↔ ∀ (g : G), g • p ≠ p → dist z p < dist z (g • p)

A point is in the interior exactly when all constraints from indices moving the centre are strict. Local finiteness of the constraints is essential for the reverse implication.