The side pairing of a Dirichlet polygon

Let Γ ≤ PSL(2, ℝ) be discrete, let p ∈ ℍ have trivial stabilizer in Γ, and let P be a convex polygon, possibly with ideal vertices, whose carrier is the Dirichlet domain of Γ centred at p. Every side of P is the Dirichlet face dirichletFace p g of a unique g ≠ 1, the part of the domain equidistant from p and g • p, and g⁻¹ carries it onto the face of g⁻¹, again a side. This file shows that these identifications form a side pairing of P in the sense of ConvexPolygon.SidePairing: g⁻¹ reverses the orientation of the sides, since it moves the centre p across the bisector of p and g⁻¹ • p. It is the only side pairing of P by elements of Γ.

The translates of a Dirichlet polygon by Γ are locally finite, and, since the centre has trivial stabilizer, every nonidentity element of Γ moves its interior off itself. These are the tessellation hypotheses of Poincaré's polygon theorem, under which the side-pairing maps generate Γ and present it, subject to the side relations and the vertex-cycle relations. For a cocompact group every Dirichlet domain is a compact convex polygon, so every cocompact group has such a Dirichlet presentation.

Main results

• ConvexPolygon.existsUnique_sidePairing_of_carrier_eq_dirichletDomain: a Dirichlet polygon has exactly one side pairing whose maps lie in Γ.
• ConvexPolygon.SidePairing.side_eq_dirichletFace: for that side pairing, side i is the Dirichlet face of the inverse of the side-pairing map of i.
• ConvexPolygon.disjoint_smul_interior_carrier_of_carrier_eq_dirichletDomain: the translates of a Dirichlet polygon have disjoint interiors.
• Subgroup.exists_sidePairing_of_compactSpace: a Dirichlet polygon of a cocompact group is a compact convex polygon whose sides are paired by elements of the group.
• Subgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace: a cocompact Fuchsian group is presented by the side pairing of a compact Dirichlet polygon.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.4 (Dirichlet polygons and their side pairings).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§3.2 and 4.1 (generators of a Fuchsian group from its Dirichlet region).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.side_eq_dirichletFace {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {p : UpperHalfPlane} {n : ℕ} [NeZero n] {P : ConvexPolygon n} [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] (σ : P.SidePairing) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hP : P.carrier = dirichletDomain (↥Γ) p) (hp : p ∈ freeLocus (↥Γ) UpperHalfPlane) (i : Fin n) : P.side i = dirichletFace p ⟨σ.map i, ⋯⟩⁻¹

Sides of a Dirichlet polygon are paired along Dirichlet faces. If the carrier of P is the Dirichlet domain of a properly discontinuous Γ, centred at a point with trivial stabilizer, and σ is a side pairing of P by elements of Γ, then side i is the Dirichlet face of the inverse of the side-pairing map of i: the points of the domain equidistant from the centre and its translate by that inverse.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.existsUnique_sidePairing_of_carrier_eq_dirichletDomain {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {p : UpperHalfPlane} {n : ℕ} [NeZero n] {P : ConvexPolygon n} [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] (hP : P.carrier = dirichletDomain (↥Γ) p) (hp : p ∈ freeLocus (↥Γ) UpperHalfPlane) : ∃! σ : P.SidePairing, ∀ (i : Fin n), σ.map i ∈ Γ

The side pairing of a Dirichlet polygon. Let Γ ≤ PSL(2, ℝ) act properly discontinuously and let the carrier of a convex polygon P, possibly with ideal vertices, be the Dirichlet domain of Γ centred at a point with trivial stabilizer. Then P has exactly one side pairing whose maps lie in Γ: the element g⁻¹ pairs the Dirichlet face of g with that of g⁻¹.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.disjoint_smul_interior_carrier_of_carrier_eq_dirichletDomain {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {p : UpperHalfPlane} {n : ℕ} [NeZero n] {P : ConvexPolygon n} (hP : P.carrier = dirichletDomain (↥Γ) p) (hp : p ∈ freeLocus (↥Γ) UpperHalfPlane) (γ : ↥Γ) (hγ : γ ≠ 1) : Disjoint (↑γ • interior P.carrier) (interior P.carrier)

Distinct translates of the interior of a Dirichlet polygon are disjoint. If the carrier of P is the Dirichlet domain of Γ, centred at a point with trivial stabilizer, then every nonidentity element of Γ moves the interior of P off itself.

theorem Subgroup.exists_sidePairing_of_compactSpace (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ] [CompactSpace (MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane)] {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) : ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.CompactConvexPolygon n) (σ : P.toConvexPolygon.SidePairing), (∀ (i : Fin n), σ.map i ∈ Γ) ∧ P.toConvexPolygon.carrier = TauCeti.dirichletDomain (↥Γ) p

Side pairings of Dirichlet polygons of cocompact groups. Let Γ ≤ PSL(2, ℝ) be discrete with compact orbit space, and let p ∈ ℍ have trivial stabilizer. The Dirichlet domain of Γ centred at p is the carrier of a compact convex polygon whose sides are paired by elements of Γ. This side pairing is unique, by TauCeti.UpperHalfPlane.ConvexPolygon.existsUnique_sidePairing_of_carrier_eq_dirichletDomain.

theorem Subgroup.exists_sidePairing_relatorQuotientTo_bijective_of_compactSpace (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ] [CompactSpace (MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane)] {p : UpperHalfPlane} (hp : p ∈ TauCeti.freeLocus (↥Γ) UpperHalfPlane) : ∃ (n : ℕ) (x : NeZero n) (P : TauCeti.UpperHalfPlane.CompactConvexPolygon n) (σ : P.toConvexPolygon.SidePairing) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ), P.carrier = TauCeti.dirichletDomain (↥Γ) p ∧ Function.Bijective ⇑(σ.relatorQuotientTo hmap)

Dirichlet presentations of cocompact Fuchsian groups. Let Γ ≤ PSL(2, ℝ) be discrete with compact orbit space, and let p ∈ ℍ have trivial stabilizer. The Dirichlet domain of Γ centred at p is a compact convex polygon P with a side pairing by elements of Γ, and Γ is presented by the side-pairing maps, subject to the side relations and the vertex-cycle relations.