Faces and identifications of a Dirichlet domain

The equality face indexed by g consists of points in the Dirichlet domain of p at equal distance from p and g • p. For an isometric group action this is exactly the intersection with the g-translate of the domain. The transformation g⁻¹ carries this face onto the face indexed by g⁻¹, describing all orbit identifications between points of the domain.

For a properly discontinuous action on a proper space the equality faces form a locally finite family. Every boundary point belongs to a face indexed by an element not fixing the centre. These results supply the identifications used to pair sides of a hyperbolic Dirichlet polygon. An equality face may be empty or have lower dimension than a side; no assertion of polygonal structure or global finite-sidedness is made here. Elements fixing the centre have the whole domain as their equality face, and are excluded from the boundary-covering statement.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.4.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §3.2.

def TauCeti.dirichletFace {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) (g : G) : Set X

The equality face of the Dirichlet domain of p indexed by g. It can be empty or of lower dimension than a side. If g fixes p, it is the whole Dirichlet domain.

Equations

• TauCeti.dirichletFace p g = TauCeti.dirichletDomain G p ∩ {x : X | dist x p = dist x (g • p)}

theorem TauCeti.dirichletFace_def {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) (g : G) : dirichletFace p g = dirichletDomain G p ∩ {x : X | dist x p = dist x (g • p)}

The defining equality-face intersection, available without unfolding the definition.

@[simp]

theorem TauCeti.mem_dirichletFace {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] {p x : X} {g : G} : x ∈ dirichletFace p g ↔ x ∈ dirichletDomain G p ∧ dist x p = dist x (g • p)

Membership in an equality face.

theorem TauCeti.dirichletFace_subset {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) (g : G) : dirichletFace p g ⊆ dirichletDomain G p

An equality face is contained in the Dirichlet domain.

theorem TauCeti.isClosed_dirichletFace {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) (g : G) : IsClosed (dirichletFace p g)

Equality faces are closed.

@[simp]

theorem TauCeti.dirichletFace_eq_dirichletDomain_of_smul_eq {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] {p : X} {g : G} (hg : g • p = p) : dirichletFace p g = dirichletDomain G p

An element fixing the centre gives the whole Dirichlet domain as its equality face.

theorem TauCeti.finite_setOf_dirichletFace_inter_nonempty {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p : X) {K : Set X} (hK : Bornology.IsBounded K) : {g : G | (dirichletFace p g ∩ K).Nonempty}.Finite

Only finitely many equality faces meet a bounded set. This counts acting elements, including the finitely many elements fixing the centre.

theorem TauCeti.locallyFinite_dirichletFace {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p : X) : LocallyFinite (dirichletFace p)

The equality faces of a Dirichlet domain are locally finite.

theorem TauCeti.frontier_dirichletDomain_subset_iUnion_dirichletFace {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p : X) : frontier (dirichletDomain G p) ⊆ ⋃ (g : { g : G // g • p ≠ p }), dirichletFace p ↑g

Every boundary point of the Dirichlet domain belongs to an equality face indexed by an element moving the centre. This does not assert that every equality face is a boundary face in an arbitrary metric space.

theorem TauCeti.dirichletFace_eq_inter_smul {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (p : X) (g : G) : dirichletFace p g = dirichletDomain G p ∩ g • dirichletDomain G p

An equality face is exactly the overlap with the corresponding translate of the Dirichlet domain. Thus every overlap, including lower-dimensional ones, has its prescribed pairing.

@[simp]

theorem TauCeti.inv_smul_dirichletFace {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (p : X) (g : G) : g⁻¹ • dirichletFace p g = dirichletFace p g⁻¹

The side-identification transformation g⁻¹ pairs the equality face indexed by g with that indexed by g⁻¹. In particular inversion preserves the indices of nonempty faces.

theorem TauCeti.inv_smul_mem_dirichletDomain_iff {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] {p x : X} (hx : x ∈ dirichletDomain G p) (g : G) : g⁻¹ • x ∈ dirichletDomain G p ↔ x ∈ dirichletFace p g

Two points of the Dirichlet domain related by g⁻¹ are related along the face indexed by g; conversely every point of that face has its g⁻¹-translate in the domain.