Continuous actions on discrete spaces

This file develops openness properties of continuous group actions on discrete spaces. For a finite space, the kernel of the action is open, and so defines an open normal subgroup (TauCeti.openActionKernel). For an arbitrary discrete space acted on by a compact topological group, every finite set is fixed pointwise by an open normal subgroup. In particular, each orbit map factors through a finite quotient. Total disconnectedness of the acting group is not needed: point stabilizers are clopen, so Mathlib's compact-group clopen-neighborhood theorem applies directly.

A function k : G → M that is equivariant for an open subgroup U, in the sense k (u * g) = u • k g, is locally constant when U acts continuously on the discrete space M: it is constant on the open neighbourhood Stab(k g) * g of each g (TauCeti.isLocallyConstant_of_apply_mul). This is the local-constancy condition defining coinduced modules.

For actions on discrete additive groups, the fixed-point subgroups over all open normal subgroups exhaust the group; the additive group need not be commutative. These results supply the openness and exhaustion properties used by the finite-quotient system for continuous cohomology.

Mathlib supplies open point stabilizers, open normal subgroups inside clopen neighborhoods of the identity in compact groups, and the quotient action on fixed points of a normal subgroup. We use its fixed-point objects throughout.

theorem Set.Finite.exists_openNormalSubgroup_smul_eq_self {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type v} [TopologicalSpace M] [DiscreteTopology M] [MulAction G M] [ContinuousSMul G M] {s : Set M} (hs : s.Finite) : ∃ (U : OpenNormalSubgroup G), ∀ u ∈ U, ∀ m ∈ s, u • m = m

A finite set in a discrete continuous action of a compact group is fixed pointwise by a single open normal subgroup.

theorem TauCeti.exists_openNormalSubgroup_smul_eq_self {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type v} [TopologicalSpace M] [DiscreteTopology M] [MulAction G M] [ContinuousSMul G M] (m : M) : ∃ (U : OpenNormalSubgroup G), ∀ u ∈ U, u • m = m

Every element of a discrete continuous action of a compact group is fixed by an open normal subgroup.

theorem TauCeti.exists_openNormalSubgroup_smul_eq_self_range {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type v} [TopologicalSpace M] [DiscreteTopology M] [MulAction G M] [ContinuousSMul G M] {ι : Type u_1} [Finite ι] (f : ι → M) : ∃ (U : OpenNormalSubgroup G), ∀ u ∈ U, ∀ (i : ι), u • f i = f i

A finite family in a discrete continuous action of a compact group has a common open normal stabilizer. This is the form used for the finite image of a locally constant cochain.

theorem TauCeti.exists_orbitMap_quotient {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type v} [TopologicalSpace M] [DiscreteTopology M] [MulAction G M] [ContinuousSMul G M] (m : M) : ∃ (U : OpenNormalSubgroup G) (f : G ⧸ ↑U.toOpenSubgroup → M), ∀ (g : G), f ↑g = g • m

The orbit map of a discrete continuous action of a compact group factors through a finite quotient, using the quotient action on the fixed points of an open normal subgroup.

theorem TauCeti.isLocallyConstant_of_apply_mul {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {U : Subgroup G} {M : Type v} [TopologicalSpace M] [DiscreteTopology M] [MulAction (↥U) M] [ContinuousSMul (↥U) M] (hU : IsOpen ↑U) {k : G → M} (hk : ∀ (u : ↥U) (g : G), k (↑u * g) = u • k g) : IsLocallyConstant k

A function on G that is equivariant for an open subgroup U acting continuously on a discrete space is locally constant: it is constant on the open neighbourhood Stab(k g) * g of g.

theorem TauCeti.ker_toPermHom_eq_iInf_stabilizer (G : Type u) [Group G] (M : Type v) [MulAction G M] : (MulAction.toPermHom G M).ker = ⨅ (m : M), MulAction.stabilizer G m

The action kernel is the intersection of all point stabilizers.

@[simp]

theorem TauCeti.ker_toPermHom_eq_top_iff (G : Type u) [Group G] (M : Type v) [MulAction G M] : (MulAction.toPermHom G M).ker = ⊤ ↔ ∀ (g : G) (m : M), g • m = m

The action kernel is the whole group exactly when the action is trivial.

theorem TauCeti.isOpen_ker_toPermHom (G : Type u) [Group G] (M : Type v) [MulAction G M] [TopologicalSpace G] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] [Finite M] : IsOpen ↑(MulAction.toPermHom G M).ker

The kernel of a continuous action on a finite discrete space is open.

def TauCeti.openActionKernel (G : Type u) [Group G] (M : Type v) [MulAction G M] [TopologicalSpace G] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] [Finite M] : OpenNormalSubgroup G

The open normal subgroup given by the kernel of a finite discrete action.

Equations

• TauCeti.openActionKernel G M = { toOpenSubgroup := let __Subgroup := (MulAction.toPermHom G M).ker; { toSubgroup := __Subgroup, isOpen' := ⋯ }, isNormal' := ⋯ }

@[simp]

theorem TauCeti.openActionKernel_toSubgroup (G : Type u) [Group G] (M : Type v) [MulAction G M] [TopologicalSpace G] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] [Finite M] : ↑(openActionKernel G M).toOpenSubgroup = (MulAction.toPermHom G M).ker

@[simp]

theorem TauCeti.openActionKernel_smul_eq_self (G : Type u) [Group G] (M : Type v) [MulAction G M] [TopologicalSpace G] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] [Finite M] (g : ↥(openActionKernel G M)) (m : M) : ↑g • m = m

Elements of the open action kernel act trivially on the finite discrete space.

@[simp]

theorem TauCeti.fixedPoints_openActionKernel_eq_top (G : Type u) [Group G] [TopologicalSpace G] (M : Type v) [AddGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] : FixedPoints.addSubgroup (↥↑(openActionKernel G M).toOpenSubgroup) M = ⊤

The fixed points of the action kernel on a finite discrete additive group are the whole group. The additive group need not be commutative.

theorem TauCeti.iSup_fixedPoints_openNormal_eq_top {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type v} [AddGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : ⨆ (U : OpenNormalSubgroup G), FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M = ⊤

The fixed-point subgroups over the open normal subgroups of a compact group exhaust a discrete additive group with a continuous action. The additive group need not be commutative.