Compact Dirichlet domains #
For an isometric group action on a proper metric space with compact orbit space, every Dirichlet domain is compact. A compact set of orbit representatives bounds the distance from a point of the domain to its centre. No proper discontinuity or freeness is needed.
In the hyperbolic plane, this supplies the boundedness used to reduce the defining bisectors to a finite family when the orbit quotient is compact.
References #
- Alan Beardon, The Geometry of Discrete Groups, §9.4.
- Svetlana Katok, Fuchsian Groups, §3.2.
Compact representatives are supplied by IsOpenMap.exists_isCompact_subset_image.
theorem
TauCeti.isCompact_dirichletDomain_of_compactSpace
{G : Type u_1}
{X : Type u_2}
[Group G]
[PseudoMetricSpace X]
[ProperSpace X]
[MulAction G X]
[IsIsometricSMul G X]
[CompactSpace (MulAction.orbitRel.Quotient G X)]
(p : X)
:
IsCompact (dirichletDomain G p)
If the orbit space of an isometric action on a proper metric space is compact, every Dirichlet domain is compact. The action need not be properly discontinuous.