The germ kernel of a group action

For a group G acting on a topological space X, the germ kernel at a point x is the subgroup TauCeti.MulAction.germKernel G x of the elements acting as the identity on some neighbourhood of x, that is, the elements whose germ at x is the germ of the identity. Equivalently, g lies in the germ kernel at x exactly when x is in the interior of the fixed set of g. The germ kernel lies between the kernel of the action, made of the elements acting trivially on all of X, and the stabilizer of x.

For the presentation [X/G] of an orbifold by a group action, the germ kernel at x is the ineffective part of the isotropy at x: the isotropy elements whose action cannot be seen near x. The effective reduction of the action discards these elements, while the orbifold keeps them. Transport along the action conjugates germ kernels, as it does stabilizers, so the order of the germ kernel is a function on the orbit space.

The stabilizer of x is the whole isotropy at x, and it equals the germ kernel exactly when all of the isotropy at x is ineffective. For a finite group acting continuously on a Hausdorff space, this happens on a dense open set of points: a point outside it lies on the frontier of the closed fixed set of some element, and a finite union of such frontiers is closed with empty interior. In the presentation [X/G], this is the dense open principal part, on which the isotropy reduces to its ineffective kernel. No smoothness or linearity is needed for this statement.

Main declarations

• TauCeti.MulAction.germKernel G x: the elements of G acting as the identity near x.
• TauCeti.MulAction.mem_germKernel_iff_mem_interior_fixedBy: g is in the germ kernel at x exactly when x is in the interior of the fixed set of g.
• TauCeti.MulAction.ker_toPermHom_le_germKernel, TauCeti.MulAction.germKernel_le_stabilizer: the germ kernel contains the kernel of the action and is contained in the stabilizer.
• TauCeti.MulAction.germKernel_smul_eq_germKernel_map_conj: the germ kernel at h • x is the conjugate by h of the germ kernel at x.
• TauCeti.MulAction.orbitCardGermKernel G: the order of the germ kernel as a function on the orbit space, well defined by TauCeti.MulAction.card_germKernel_smul.
• TauCeti.MulAction.stabilizer_eq_germKernel_iff_of_stabilizer_le: at a point whose stabilizer lies in a subgroup H, the stabilizer is the germ kernel for G exactly when it is for H.
• TauCeti.MulAction.setOf_stabilizer_eq_germKernel: the points whose stabilizer is the germ kernel are those lying in no fixed set without lying in its interior.
• TauCeti.MulAction.isOpen_setOf_stabilizer_eq_germKernel, TauCeti.MulAction.dense_setOf_stabilizer_eq_germKernel: for a finite group acting continuously on a Hausdorff space, these points form a dense open set.

References

• 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 and the ineffective kernel of their local group actions.

def TauCeti.MulAction.germKernel (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] (x : X) : Subgroup G

The germ kernel of the action of G at x: the subgroup of the elements of G that act as the identity on a neighbourhood of x.

@[simp]

theorem TauCeti.MulAction.mem_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] {x : X} {g : G} : g ∈ germKernel G x ↔ ∀ᶠ (y : X) in nhds x, g • y = y

theorem TauCeti.MulAction.mem_germKernel_iff_mem_interior_fixedBy {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] {x : X} {g : G} : g ∈ germKernel G x ↔ x ∈ interior (MulAction.fixedBy X g)

An element is in the germ kernel at x exactly when x is in the interior of its fixed set.

theorem TauCeti.MulAction.germKernel_le_stabilizer {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] (x : X) : germKernel G x ≤ MulAction.stabilizer G x

An element of the germ kernel at x fixes x.

theorem TauCeti.MulAction.ker_toPermHom_le_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] (x : X) : (MulAction.toPermHom G X).ker ≤ germKernel G x

An element acting trivially on all of X is in the germ kernel at every point.

theorem TauCeti.MulAction.germKernel_smul_eq_germKernel_map_conj {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] (h : G) (x : X) : germKernel G (h • x) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj h)) (germKernel G x)

The germ kernel at h • x is the conjugate by h of the germ kernel at x.

theorem TauCeti.MulAction.card_germKernel_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] (h : G) (x : X) : Nat.card ↥(germKernel G (h • x)) = Nat.card ↥(germKernel G x)

The germ kernels along an orbit have the same order.

theorem TauCeti.MulAction.stabilizer_le_normalizer_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] (x : X) : MulAction.stabilizer G x ≤ Subgroup.normalizer ↑(germKernel G x)

The stabilizer of x normalizes the germ kernel at x.

instance TauCeti.MulAction.normal_germKernel_subgroupOf_stabilizer {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] (x : X) : ((germKernel G x).subgroupOf (MulAction.stabilizer G x)).Normal

The germ kernel at x is a normal subgroup of the stabilizer of x, so the isotropy at x has an effective quotient by its ineffective part.

noncomputable def TauCeti.MulAction.orbitCardGermKernel (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] : MulAction.orbitRel.Quotient G X → ℕ

The order of the germ kernel as a function on the orbit space: its value at the orbit of x is the order of the germ kernel at x, which does not depend on the representative by TauCeti.MulAction.card_germKernel_smul. For the presentation [X/G] it is the order of the ineffective isotropy at a point of the coarse space.

@[simp]

theorem TauCeti.MulAction.orbitCardGermKernel_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] (x : X) : orbitCardGermKernel G ⟦x⟧ = Nat.card ↥(germKernel G x)

@[simp]

theorem TauCeti.MulAction.germKernel_subgroupOf {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] (H : Subgroup G) (x : X) : (germKernel G x).subgroupOf H = germKernel (↥H) x

The germ kernel of the restricted action of a subgroup H is the germ kernel of G pulled back to H.

theorem TauCeti.MulAction.stabilizer_eq_germKernel_iff_of_stabilizer_le {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] {H : Subgroup G} {y : X} (hy : MulAction.stabilizer G y ≤ H) : MulAction.stabilizer (↥H) y = germKernel (↥H) y ↔ MulAction.stabilizer G y = germKernel G y

If the stabilizer of y lies in a subgroup H, then the stabilizer of y is its germ kernel for G exactly when it is for H. This applies to the points of a slice for H.

theorem TauCeti.MulAction.setOf_stabilizer_eq_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] : {x : X | MulAction.stabilizer G x = germKernel G x} = (⋃ (g : G), MulAction.fixedBy X g \ interior (MulAction.fixedBy X g))ᶜ

A point has its germ kernel as its stabilizer exactly when it lies in no fixed set without lying in its interior: every element fixing the point acts as the identity near it.

@[simp]

theorem TauCeti.MulAction.stabilizer_smul_eq_germKernel_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] (g : G) (x : X) : MulAction.stabilizer G (g • x) = germKernel G (g • x) ↔ MulAction.stabilizer G x = germKernel G x

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

theorem TauCeti.MulAction.isOpen_setOf_stabilizer_eq_germKernel {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 = germKernel G x}

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

theorem TauCeti.MulAction.dense_setOf_stabilizer_eq_germKernel {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [ContinuousConstSMul G X] [Finite G] : Dense {x : X | MulAction.stabilizer G x = germKernel G x}

The principal part of a finite action. For a finite group acting continuously on a Hausdorff space, 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 TauCeti.MulAction.isOpen_setOf_stabilizer_eq_germKernel.