Compact Dirichlet polygons

A bounded hyperbolic Dirichlet domain of a properly discontinuous action on ℍ is the carrier of a compact convex polygon. Each side of the polygon is a Dirichlet face dirichletFace p g: the part of the domain on the perpendicular bisector of the centre p and a translate g • p ≠ p, with the domain on the side of p. In particular, for an isometric action with compact orbit space every Dirichlet domain is a compact convex polygon. This enumerates the vertices and sides of a compact Dirichlet polygon.

Conversely, for any convex polygon, possibly with ideal vertices, whose carrier is a Dirichlet domain, the sides are exactly the Dirichlet faces with two distinct points indexed by elements moving the centre. A side lies in the boundary, which is covered by the locally finite faces, so some face contains two of its points and hence lies on its supporting line.

The statements combine the finite bisector descriptions of TauCeti.UpperHalfPlane.exists_finset_dirichletDomain_eq_iInter_closure_leftHalfPlane with TauCeti.UpperHalfPlane.exists_compactConvexPolygon_carrier_eq_iInter_closure_leftHalfPlane.

Main results

• TauCeti.UpperHalfPlane.exists_compactConvexPolygon_carrier_eq_dirichletDomain: a bounded Dirichlet domain is a compact convex polygon whose sides are Dirichlet faces.
• TauCeti.UpperHalfPlane.exists_compactConvexPolygon_carrier_eq_dirichletDomain_of_compactSpace: the same for every Dirichlet domain of an isometric action with compact orbit space.
• TauCeti.UpperHalfPlane.ConvexPolygon.exists_side_eq_dirichletFace and TauCeti.UpperHalfPlane.ConvexPolygon.exists_side_eq_dirichletFace_of_nontrivial: the sides of a Dirichlet polygon are its nondegenerate Dirichlet faces.

References

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

theorem TauCeti.UpperHalfPlane.exists_compactConvexPolygon_carrier_eq_dirichletDomain {G : Type u_1} [SMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {p : UpperHalfPlane} (hb : Bornology.IsBounded (dirichletDomain G p)) : ∃ (n : ℕ) (x : NeZero n) (P : CompactConvexPolygon n), P.carrier = dirichletDomain G p ∧ ∀ (i : Fin n), ∃ (g : G), p ≠ g • p ∧ leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))) = leftHalfPlane (perpBisector p (g • p)) ∧ P.side i = dirichletFace p g

A bounded Dirichlet domain is a compact convex polygon. For a properly discontinuous action on ℍ, a bounded Dirichlet domain centred at p is the carrier of a compact convex polygon. Each side is the Dirichlet face of an element g moving p, and the polygon lies on the side of p of the perpendicular bisector of p and g • p.

theorem TauCeti.UpperHalfPlane.exists_compactConvexPolygon_carrier_eq_dirichletDomain_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) : ∃ (n : ℕ) (x : NeZero n) (P : CompactConvexPolygon n), P.carrier = dirichletDomain G p ∧ ∀ (i : Fin n), ∃ (g : G), p ≠ g • p ∧ leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))) = leftHalfPlane (perpBisector p (g • p)) ∧ P.side i = dirichletFace p g

Dirichlet polygons of cocompact actions. For a properly discontinuous isometric action on ℍ with compact orbit space, every Dirichlet domain is the carrier of a compact convex polygon whose sides are Dirichlet faces, as in exists_compactConvexPolygon_carrier_eq_dirichletDomain.

Sides of Dirichlet polygons are Dirichlet faces

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_side_eq_dirichletFace_of_nontrivial {G : Type u_1} [SMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {n : ℕ} [NeZero n] {P : ConvexPolygon n} {p : UpperHalfPlane} (hP : P.carrier = dirichletDomain G p) {g : G} (hg : g • p ≠ p) (hne : (dirichletFace p g).Nontrivial) : ∃ (j : Fin n), P.side j = dirichletFace p g

Nondegenerate Dirichlet faces are sides. If a convex polygon, possibly with ideal vertices, is a Dirichlet domain, then every Dirichlet face with two distinct points, indexed by an element moving the centre, is one of its sides.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_side_eq_dirichletFace {G : Type u_1} [SMul G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {n : ℕ} [NeZero n] {P : ConvexPolygon n} {p : UpperHalfPlane} (hP : P.carrier = dirichletDomain G p) (i : Fin n) : ∃ (g : G), g • p ≠ p ∧ P.side i = dirichletFace p g

Sides of a Dirichlet polygon are Dirichlet faces. If a convex polygon, possibly with ideal vertices, is a Dirichlet domain, then each of its sides is the Dirichlet face of an element moving the centre.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.existsUnique_side_eq_dirichletFace {G : Type u_1} [Group G] [MulAction G UpperHalfPlane] [ProperlyDiscontinuousSMul G UpperHalfPlane] {n : ℕ} [NeZero n] {P : ConvexPolygon n} {p : UpperHalfPlane} (hP : P.carrier = dirichletDomain G p) (hp : p ∈ freeLocus G UpperHalfPlane) (i : Fin n) : ∃! g : G, g ≠ 1 ∧ P.side i = dirichletFace p g

For a centre with trivial stabilizer, each side of a Dirichlet polygon is the Dirichlet face of a unique element other than the identity.