The generic stabilizer of a finite linear action

Every point stabilizer of a group action contains the kernel of the action, the subgroup (MulAction.toPermHom G X).ker of elements acting trivially. This file shows that for a finite group acting linearly on a topological vector space, the stabilizer is exactly that kernel on a dense open set of points. No faithfulness is assumed: elements of the kernel are kept as genuine isotropy, and the statement is that on a dense open set they are the only isotropy. For a faithful action the kernel is trivial, so the free locus is dense.

The proof is the fixed-subspace calculation. A point fails to have the kernel as its stabilizer exactly when it is fixed by some element outside the kernel, so the set in question is the complement of the union of the fixed sets MulAction.fixedBy X g over g outside the kernel. For a finite group acting by continuous maps on a Hausdorff space, this is a finite union of closed sets, which gives openness. For a linear action, the fixed set of g is a submodule, and it is a proper submodule when g is outside the kernel; over a ring such as a nontrivially normed field a proper submodule has empty interior, so the finite union is nowhere dense.

The density statement is also recorded for an arbitrary finite action whose nontrivially acting elements have fixed sets with empty interior; the linear case is the instance of it obtained from the fixed-subspace calculation.

Main results

• TauCeti.setOf_stabilizer_eq_ker: the points whose stabilizer is the action kernel are the complement of the fixed sets of the elements outside the kernel.
• TauCeti.stabilizer_smul_eq_ker_iff: this set of points is invariant under the action.
• TauCeti.isOpen_setOf_stabilizer_eq_ker: for a finite group acting continuously on a Hausdorff space, this set is open.
• TauCeti.dense_setOf_stabilizer_eq_ker_of_interior_fixedBy: it is dense when the fixed set of every element outside the kernel has empty interior.
• TauCeti.interior_fixedBy_eq_empty_of_notMem_ker: for a linear action, the fixed set of an element outside the kernel has empty interior.
• TauCeti.dense_setOf_stabilizer_eq_ker: for a finite linear action, the stabilizer is the action kernel on a dense set of points.
• TauCeti.dense_freeLocus: for a faithful finite linear action, the free locus is dense.

References

• G. E. Bredon, Introduction to Compact Transformation Groups, Chapter IV, §3.
• A. Adem, J. Leida and Y. Ruan, Orbifolds and Stringy Topology, Chapter 1.

theorem TauCeti.setOf_stabilizer_eq_ker {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] : {x : X | MulAction.stabilizer G x = (MulAction.toPermHom G X).ker} = (⋃ (g : G), ⋃ (_ : g ∉ (MulAction.toPermHom G X).ker), MulAction.fixedBy X g)ᶜ

A point has the action kernel as its stabilizer exactly when it is fixed by no element outside the kernel.

@[simp]

theorem TauCeti.stabilizer_smul_eq_ker_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (g : G) (x : X) : MulAction.stabilizer G (g • x) = (MulAction.toPermHom G X).ker ↔ MulAction.stabilizer G x = (MulAction.toPermHom G X).ker

The set of points whose stabilizer is the action kernel is invariant under the action.

theorem TauCeti.isOpen_setOf_stabilizer_eq_ker {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [ContinuousConstSMul G X] [Finite G] : IsOpen {x : X | MulAction.stabilizer G x = (MulAction.toPermHom G X).ker}

For a finite group acting continuously on a Hausdorff space, the points whose stabilizer is the action kernel form an open set.

theorem TauCeti.dense_setOf_stabilizer_eq_ker_of_interior_fixedBy {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [ContinuousConstSMul G X] [Finite G] (h : ∀ g ∉ (MulAction.toPermHom G X).ker, interior (MulAction.fixedBy X g) = ∅) : Dense {x : X | MulAction.stabilizer G x = (MulAction.toPermHom G X).ker}

For a finite group acting continuously on a Hausdorff space, the points whose stabilizer is the action kernel form a dense set, provided the fixed set of every element outside the kernel has empty interior.

theorem TauCeti.interior_fixedBy_eq_empty_of_notMem_ker {G : Type u_1} [Group G] (R : Type u_3) {V : Type u_4} [Ring R] [TopologicalSpace R] [(nhdsWithin 0 {r : R | IsUnit r}).NeBot] [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V] [DistribMulAction G V] [SMulCommClass G R V] {g : G} (hg : g ∉ (MulAction.toPermHom G V).ker) : interior (MulAction.fixedBy V g) = ∅

For a linear action on a topological module over a ring in which 0 is a limit of units, for instance a nontrivially normed field, the fixed set of an element outside the action kernel has empty interior: it is a proper submodule.

theorem TauCeti.dense_setOf_stabilizer_eq_ker {G : Type u_1} [Group G] (R : Type u_3) {V : Type u_4} [Ring R] [TopologicalSpace R] [(nhdsWithin 0 {r : R | IsUnit r}).NeBot] [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V] [DistribMulAction G V] [SMulCommClass G R V] [T2Space V] [ContinuousConstSMul G V] [Finite G] : Dense {v : V | MulAction.stabilizer G v = (MulAction.toPermHom G V).ker}

Generic stabilizer of a finite linear action. For a finite group acting linearly and continuously on a Hausdorff topological module over a ring in which 0 is a limit of units, for instance a finite-dimensional real vector space, the points whose stabilizer is the kernel of the action form a dense set. The action need not be faithful. The set is also open, by TauCeti.isOpen_setOf_stabilizer_eq_ker.

theorem TauCeti.dense_freeLocus {G : Type u_1} [Group G] (R : Type u_3) {V : Type u_4} [Ring R] [TopologicalSpace R] [(nhdsWithin 0 {r : R | IsUnit r}).NeBot] [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V] [DistribMulAction G V] [SMulCommClass G R V] [T2Space V] [ContinuousConstSMul G V] [Finite G] [FaithfulSMul G V] : Dense ↑(freeLocus G V)

For a faithful finite group action, linear and continuous on a Hausdorff topological module over a ring in which 0 is a limit of units, the points with trivial stabilizer form a dense set.