The principal part of a proper action of a discrete group

Let a discrete group G act properly on a topological space X, in the sense of Mathlib's ProperSMul. This file proves that the points whose stabilizer is their germ kernel form a dense open subset of X. At such a point every element fixing the point acts as the identity near it, so in the presentation [X/G] the isotropy there is exactly its ineffective part. This is the dense open principal part of [X/G]. The group may be infinite and the action need not be faithful or smooth.

The proof is local. Near a point x, a slice U for the finite stabilizer G_x (ProperSMul.exists_slice) has the property that the stabilizer in G of every point of U lies in G_x. So on U the points whose stabilizer is the germ kernel are the same for G and for G_x (TauCeti.MulAction.stabilizer_eq_germKernel_iff_of_stabilizer_le). For the finite group G_x they form a dense open set (TauCeti.MulAction.dense_setOf_stabilizer_eq_germKernel), and being dense and open is a local property.

Main results

• ProperSMul.isOpen_setOf_stabilizer_eq_germKernel, ProperSMul.dense_setOf_stabilizer_eq_germKernel: for a proper action of a discrete group, the points whose stabilizer is the germ kernel form a dense open set.

References

• I. Moerdijk, Orbifolds as groupoids: an introduction, Section 2, for the local isotropy model of a proper étale groupoid.
• A. Adem, J. Leida and Y. Ruan, Orbifolds and Stringy Topology, Cambridge Tracts in Mathematics 171, Cambridge University Press, 2007, Ch. 1, for ineffective orbifolds.

theorem ProperSMul.isOpen_setOf_stabilizer_eq_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [DiscreteTopology G] [TopologicalSpace X] [ProperSMul G X] : IsOpen {y : X | MulAction.stabilizer G y = TauCeti.MulAction.germKernel G y}

For a proper action of a discrete group, the points whose stabilizer is the germ kernel form an open set.

theorem ProperSMul.dense_setOf_stabilizer_eq_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [DiscreteTopology G] [TopologicalSpace X] [ProperSMul G X] : Dense {y : X | MulAction.stabilizer G y = TauCeti.MulAction.germKernel G y}

The principal part of a proper action. For a proper action of a discrete group, the points whose stabilizer is the germ kernel form a dense set: generically, an element fixing a point acts as the identity near it. The set is also open, by ProperSMul.isOpen_setOf_stabilizer_eq_germKernel.