Fundamental domains of properly discontinuous actions

Let a countable group G act properly discontinuously on a second countable, locally compact Hausdorff space X. Every point with trivial stabilizer has a neighbourhood disjoint from all of its nontrivial translates. Enumerating the basic open sets with this property as V₀, V₁, … and keeping, from each Vₙ, the points whose orbit misses V₀, …, Vₙ₋₁, gives a Borel set s that meets every orbit of a free point exactly once, and meets no orbit twice.

Consequently, for any measure μ on X for which the non-free points form a null set, s is a measurable fundamental domain for G in the sense of MeasureTheory.IsFundamentalDomain (MeasureTheory.Measure.exists_isFundamentalDomain_of_properlyDiscontinuousSMul). Its translates are not merely almost everywhere disjoint but genuinely disjoint. Together with MeasureTheory.IsFundamentalDomain.measure_eq this makes the covolume MeasureTheory.covolume G X μ the measure of any measurable fundamental domain.

References

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

theorem TauCeti.exists_seq_isOpen_disjoint_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [SecondCountableTopology X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] : ∃ (V : ℕ → Set X), (∀ (n : ℕ), IsOpen (V n)) ∧ (∀ (n : ℕ) (g : G), g ≠ 1 → Disjoint (g • V n) (V n)) ∧ ∀ x ∈ ↑(freeLocus G X), ∃ (n : ℕ), x ∈ V n

In a second countable space with a properly discontinuous action there is a sequence of open sets, each disjoint from its nontrivial translates, that covers the free locus.

theorem MeasureTheory.Measure.exists_isFundamentalDomain_of_properlyDiscontinuousSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [SecondCountableTopology X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] [Countable G] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) (hμ : μ (↑(TauCeti.freeLocus G X))ᶜ = 0) : ∃ (s : Set X), MeasurableSet s ∧ (Pairwise fun (g h : G) => Disjoint (g • s) (h • s)) ∧ IsFundamentalDomain G s μ

Existence of a measurable fundamental domain. A countable group acting properly discontinuously on a second countable, locally compact Hausdorff space has a measurable fundamental domain with respect to every measure for which the points with nontrivial stabilizer form a null set. The translates of the domain by distinct elements are disjoint.