Slices of proper actions of discrete groups

Let a discrete group G act properly on a topological space X, in the sense of Mathlib's ProperSMul: the map (g, y) ↦ (g • y, y) is proper. This file constructs the local model of the action near a point x: arbitrarily small open neighbourhoods U of x, invariant under the stabilizer of x, such that every element of G carrying a point of U into U fixes x (ProperSMul.exists_slice). Such a U is a slice at x for the stabilizer, so near the orbit of x the quotient [X/G] is the finite quotient [U/G_x]. The stabilizer keeps every element fixing x, including those acting trivially on all of U.

Two facts make this work. First, a proper action of a discrete group is properly discontinuous (ProperSMul.properlyDiscontinuousSMul), so stabilizers are finite. Second, properness excludes all other group elements near (x, x): the image of the closed set of pairs (g, y) with g • x ≠ x under the closed map (g, y) ↦ (g • y, y) is closed and misses (x, x), so some neighbourhood U of x has no such g moving a point of U into U (ProperSMul.exists_nhds_image_smul_eq_self). Intersecting the translates of a smaller open neighbourhood by the finitely many elements of the stabilizer makes it invariant.

Mathlib proves the properly discontinuous version ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self for locally compact Hausdorff spaces, and the equivalence properlyDiscontinuousSMul_iff_properSMul for Hausdorff spaces whose square is compactly coherent. The statements here assume neither: properness is used directly.

Main results

• ProperSMul.properlyDiscontinuousSMul: a proper action of a discrete group is properly discontinuous.
• ProperSMul.exists_nhds_image_smul_eq_self: some neighbourhood of x is moved into itself only by elements fixing x.
• ProperSMul.exists_slice: every neighbourhood of x contains an open slice at x for its stabilizer.

References

• R. S. Palais, On the existence of slices for actions of non-compact Lie groups, Ann. of Math. 73 (1961), 295--323, for slices of proper actions.
• I. Moerdijk, Orbifolds as groupoids: an introduction, Section 2, for the local isotropy model of a proper étale groupoid.

theorem ProperSMul.properlyDiscontinuousSMul (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace G] [DiscreteTopology G] [TopologicalSpace X] [ProperSMul G X] : ProperlyDiscontinuousSMul G X

A proper action of a discrete group is properly discontinuous: only finitely many elements move a compact set to meet another.

theorem ProperSMul.exists_nhds_image_smul_eq_self (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [DiscreteTopology G] [TopologicalSpace X] [ProperSMul G X] (x : X) : ∃ U ∈ nhds x, ∀ (g : G), ((fun (x : X) => g • x) '' U ∩ U).Nonempty → g • x = x

For a proper action of a discrete group, some neighbourhood U of x is moved to meet itself only by elements fixing x. No local compactness or separation of X is needed.

theorem ProperSMul.exists_slice (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [DiscreteTopology G] [TopologicalSpace X] [ProperSMul G X] (x : X) {W : Set X} (hW : W ∈ nhds x) : ∃ (U : SubMulAction (↥(MulAction.stabilizer G x)) X), IsOpen ↑U ∧ x ∈ U ∧ ↑U ⊆ W ∧ ∀ (g : G), ∀ y ∈ U, g • y ∈ U → g ∈ MulAction.stabilizer G x

Slices of proper actions of discrete groups. Every neighbourhood W of x contains an open neighbourhood U of x, invariant under the stabilizer of x, such that every element of G carrying a point of U into U fixes x.