The germ kernel of a smooth finite-order action

Let a group G act on a Hausdorff manifold M without boundary, modelled on a complete normed space over ℝ or ℂ. This file proves an identity principle for elements of finite order acting by C¹ maps: the set of points near which such an element g acts as the identity, the interior of its fixed set, is closed as well as open. So if g acts as the identity on a neighbourhood (in M) of some point of a connected set, it acts as the identity on a neighbourhood of every point of that set.

In terms of the germ kernel TauCeti.MulAction.germKernel G x of the elements acting as the identity near x, this says that for a group with torsion stabilizers acting by C¹ maps the germ kernel is constant on connected sets. On a connected manifold it is the kernel of the action at every point, so it is a normal subgroup, and in general it is a locally constant function of the point, as is its order. This is the statement that the ineffective kernel of a local action chart [U/G] of an orbifold acts trivially on the whole connected chart: an element acting trivially near one point acts trivially everywhere, so the ineffective part of the isotropy is the same at every point of the chart. The order of the germ kernel is also constant along orbits, so it is a locally constant function on the orbit space. Stabilizers are finite, hence torsion, for a finite group and for a proper action of a discrete group.

For a finite group the stabilizer equals the germ kernel on a dense open set (TauCeti.MulAction.dense_setOf_stabilizer_eq_germKernel), so on a connected chart the stabilizer is the kernel of the action at a dense open set of points: generically, the isotropy of [U/G] is exactly its ineffective kernel. The same holds for a proper action of a discrete group on a connected manifold, using ProperSMul.dense_setOf_stabilizer_eq_germKernel.

The proof is Bochner linearization (OpenPartialHomeomorph.exists_equivariant_chart), which on a manifold gives a chart at a common fixed point of a finite group acting by C¹ maps in which the group acts linearly, the germ kernel at the point being the kernel of this linear action. A point y in the closure of the interior of the fixed set of g is fixed by g, so the finite cyclic group generated by g fixes y and acts linearly in a Bochner chart at y. In that chart g acts by a linear map that is the identity on a nonempty open set, hence everywhere, so g acts as the identity near y.

The Hausdorff hypothesis cannot be dropped: on the line with two origins, the map exchanging the two origins is smooth, has order two, and is the identity off the origins, but not everywhere.

Main results

• TauCeti.exists_equivariant_chart_of_contMDiffAt: Bochner linearization at a common fixed point of a finite group acting by maps that are C¹ there, with the germ kernel as the kernel of the linear action.
• TauCeti.exists_equivariant_chart_target_eq_sumOfConjugatesInnerSublevel_of_contMDiffAt: on a finite-dimensional real manifold, the Bochner chart can be taken inside any neighbourhood of the fixed point, onto an invariant ball, with preconnected domain on which exactly the elements of the germ kernel act trivially.
• TauCeti.isClosed_interior_fixedBy, TauCeti.isClopen_interior_fixedBy: the interior of the fixed set of a finite-order element acting by a C¹ map is clopen.
• TauCeti.subset_interior_fixedBy_of_isPreconnected: the identity principle on a preconnected set.
• TauCeti.germKernel_eq_of_isPreconnected: the germ kernel of a group with torsion stabilizers acting by C¹ maps is the same at all points of a preconnected set.
• TauCeti.germKernel_eq_ker, TauCeti.normal_germKernel: on a preconnected manifold, the germ kernel at every point is the kernel of the action, so it is normal.
• TauCeti.dense_setOf_stabilizer_eq_ker_of_contMDiff: for a finite group acting by C¹ maps on a preconnected manifold, the stabilizer is the kernel of the action on a dense open set of points.
• TauCeti.isOpen_setOf_stabilizer_eq_ker_of_properSMul, TauCeti.dense_setOf_stabilizer_eq_ker_of_properSMul: for a proper action of a discrete group by C¹ maps on a preconnected manifold, the stabilizer is the kernel of the action on a dense open set of points.
• TauCeti.isLocallyConstant_germKernel, TauCeti.isLocallyConstant_card_germKernel: the germ kernel of a group with torsion stabilizers acting by C¹ maps, and its order, are locally constant.
• TauCeti.isLocallyConstant_orbitCardGermKernel: the order of the germ kernel is a locally constant function on the orbit space.

References

• S. Bochner, Compact groups of differentiable transformations, Ann. of Math. (2) 46 (1945), 372–381.
• A. Adem, J. Leida and Y. Ruan, Orbifolds and Stringy Topology, Cambridge Tracts in Mathematics 171, Cambridge University Press, 2007, Ch. 1, for the ineffective kernel of the local group actions of an orbifold.

theorem TauCeti.exists_chart_isotropyRepresentation {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [ContinuousConstSMul G M] {y : M} (hsmooth : ∀ (g : G), ContMDiffAt I I 1 (fun (x : M) => g • x) y) (hy : ∀ (g : G), g • y = y) : ∃ (χ : OpenPartialHomeomorph M E) (σ : ContRepresentation 𝕜 G E), y ∈ χ.source ∧ ↑χ = ↑(extChartAt I y) ∧ ↑χ.symm = ↑(extChartAt I y).symm ∧ χ.source = (extChartAt I y).source ∧ χ.target = (extChartAt I y).target ∧ ∀ (g : G), HasStrictFDerivAt (↑χ ∘ (fun (x : M) => g • x) ∘ ↑χ.symm) (σ g) (↑χ y)

At a common fixed point of a C¹ action, choose an open partial homeomorphism realizing extChartAt and its isotropy representation, with strict derivatives of all conjugated maps. This is the common coordinate setup for topological and smooth Bochner linearization.

theorem TauCeti.exists_equivariant_chart_of_contMDiffAt {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [Finite G] [ContinuousConstSMul G M] {y : M} (hsmooth : ∀ (g : G), ContMDiffAt I I 1 (fun (x : M) => g • x) y) (hy : ∀ (g : G), g • y = y) : ∃ (σ : ContRepresentation 𝕜 G E) (e : OpenPartialHomeomorph M E), y ∈ e.source ∧ ↑e y = 0 ∧ (∀ (g : G), ∀ z ∈ e.source, g • z ∈ e.source ∧ ↑e (g • z) = (σ g) (↑e z)) ∧ ∀ (g : G), σ g = 1 ↔ g ∈ MulAction.germKernel G y

Bochner linearization on a manifold. Let a finite group act continuously on a manifold without boundary, fixing y, by maps that are C¹ at y. Then in some chart e at y with invariant domain, sending y to 0, the group acts linearly, through a continuous representation σ, and an element lies in the germ kernel at y exactly when it acts trivially through σ.

theorem TauCeti.isClosed_interior_fixedBy {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] (g : G) (hg : IsOfFinOrder g) (hsmooth : ContMDiff I I 1 fun (x : M) => g • x) : IsClosed (interior (MulAction.fixedBy M g))

Identity principle for finite-order actions. For an element of finite order acting by a C¹ map on a Hausdorff manifold without boundary, the set of points near which it acts as the identity is closed.

theorem TauCeti.isClopen_interior_fixedBy {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] (g : G) (hg : IsOfFinOrder g) (hsmooth : ContMDiff I I 1 fun (x : M) => g • x) : IsClopen (interior (MulAction.fixedBy M g))

For an element of finite order acting by a C¹ map on a Hausdorff manifold without boundary, the set of points near which it acts as the identity is clopen.

theorem TauCeti.subset_interior_fixedBy_of_isPreconnected {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] (g : G) (hg : IsOfFinOrder g) (hsmooth : ContMDiff I I 1 fun (x : M) => g • x) {s : Set M} (hs : IsPreconnected s) (hne : (s ∩ interior (MulAction.fixedBy M g)).Nonempty) : s ⊆ interior (MulAction.fixedBy M g)

Identity principle for finite-order actions on a preconnected set. If an element of finite order acting by a C¹ map on a Hausdorff manifold without boundary acts as the identity near some point of a preconnected set, then it acts as the identity near every point of that set.

theorem TauCeti.germKernel_eq_of_isPreconnected {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) {s : Set M} (hs : IsPreconnected s) {x y : M} (hx : x ∈ s) (hy : y ∈ s) : MulAction.germKernel G x = MulAction.germKernel G y

For a group with torsion stabilizers acting by C¹ maps on a Hausdorff manifold without boundary, the germ kernel is the same at any two points of a preconnected set.

theorem TauCeti.germKernel_eq_ker {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] [PreconnectedSpace M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) (x : M) : MulAction.germKernel G x = (MulAction.toPermHom G M).ker

For a group with torsion stabilizers acting by C¹ maps on a preconnected Hausdorff manifold without boundary, the germ kernel at every point is the kernel of the action: an element acting as the identity near one point acts as the identity everywhere.

theorem TauCeti.normal_germKernel {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] [PreconnectedSpace M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) (x : M) : (MulAction.germKernel G x).Normal

For a group with torsion stabilizers acting by C¹ maps on a preconnected Hausdorff manifold without boundary, the germ kernel at every point is a normal subgroup.

theorem TauCeti.dense_setOf_stabilizer_eq_ker_of_contMDiff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [Finite G] [T2Space M] [PreconnectedSpace M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) : Dense {x : M | MulAction.stabilizer G x = (MulAction.toPermHom G M).ker}

The principal part of a finite smooth action. For a finite group acting by C¹ maps on a preconnected Hausdorff manifold without boundary, the points whose stabilizer is the kernel of the action form a dense set. The action need not be faithful: elements acting trivially are retained in every stabilizer, and generically they are the only ones. The set is also open, by TauCeti.isOpen_setOf_stabilizer_eq_ker.

theorem TauCeti.isLocallyConstant_germKernel {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) : IsLocallyConstant (MulAction.germKernel G)

For a group with torsion stabilizers acting by C¹ maps on a Hausdorff manifold without boundary, the germ kernel is a locally constant function of the point: it is constant on connected components, which are open.

theorem TauCeti.isLocallyConstant_card_germKernel {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) : IsLocallyConstant fun (x : M) => Nat.card ↥(MulAction.germKernel G x)

For a group with torsion stabilizers acting by C¹ maps on a Hausdorff manifold without boundary, the order of the germ kernel is a locally constant function of the point.

theorem TauCeti.isLocallyConstant_orbitCardGermKernel {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [T2Space M] [ContinuousConstSMul G M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) (hG : ∀ (x : M), IsMulTorsion ↥(MulAction.stabilizer G x)) : IsLocallyConstant (MulAction.orbitCardGermKernel G)

The kernel order on the coarse space. For a group with torsion stabilizers acting by C¹ maps on a Hausdorff manifold without boundary, the order of the germ kernel, as a function on the orbit space, is locally constant. So it is constant on each connected component of the orbit space.

theorem TauCeti.isOpen_setOf_stabilizer_eq_ker_of_properSMul {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [TopologicalSpace G] [DiscreteTopology G] [ProperSMul G M] [PreconnectedSpace M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) : IsOpen {x : M | MulAction.stabilizer G x = (MulAction.toPermHom G M).ker}

For a proper action of a discrete group by C¹ maps on a preconnected manifold without boundary, the points whose stabilizer is the kernel of the action form an open set.

theorem TauCeti.dense_setOf_stabilizer_eq_ker_of_properSMul {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} {G : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [MulAction G M] [CompleteSpace E] [TopologicalSpace G] [DiscreteTopology G] [ProperSMul G M] [PreconnectedSpace M] (hsmooth : ∀ (g : G), ContMDiff I I 1 fun (x : M) => g • x) : Dense {x : M | MulAction.stabilizer G x = (MulAction.toPermHom G M).ker}

The principal part of a proper smooth action. For a proper action of a discrete group by C¹ maps on a preconnected manifold without boundary, the points whose stabilizer is the kernel of the action form a dense set. The group may be infinite and the action need not be faithful: the elements acting trivially lie in every stabilizer, and generically they are the only ones. The set is also open, by TauCeti.isOpen_setOf_stabilizer_eq_ker_of_properSMul.

theorem TauCeti.exists_equivariant_chart_target_eq_sumOfConjugatesInnerSublevel_of_contMDiffAt {E : Type u_1} {H : Type u_2} {M : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [Group G] [Fintype G] [MulAction G M] [ContinuousConstSMul G M] {y : M} (hsmooth : ∀ (g : G), ContMDiffAt I I 1 (fun (x : M) => g • x) y) (hy : ∀ (g : G), g • y = y) {s : Set M} (hs : s ∈ nhds y) : ∃ (σ : ContRepresentation ℝ G E) (e : OpenPartialHomeomorph M E) (c : ℝ), 0 < c ∧ y ∈ e.source ∧ ↑e y = 0 ∧ e.source ⊆ s ∧ e.target = (ContRepresentation.toRepresentation ℝ G E σ).sumOfConjugatesInnerSublevel c ∧ IsPreconnected e.source ∧ (∀ (g : G), ∀ z ∈ e.source, g • z ∈ e.source ∧ ↑e (g • z) = (σ g) (↑e z)) ∧ ∀ (g : G), (σ g = 1 ↔ g ∈ MulAction.germKernel G y) ∧ (σ g = 1 ↔ ∀ z ∈ e.source, g • z = z)

The linear local model at a fixed point. Let a finite group G act continuously on a finite-dimensional real manifold without boundary, fixing y, by maps that are C¹ at y. Inside any neighbourhood s of y there is a chart e sending y to 0 whose domain is G-invariant and preconnected and whose target is a positive strict sublevel set of a σ-invariant inner product, in which G acts linearly through a continuous representation σ. Every element of G is retained, including those acting trivially: g acts as the identity near y, that is, lies in the germ kernel at y, exactly when σ g = 1, and exactly when g fixes every point of the domain of e.