Continuity of the actions on a stable additive subgroup and on its quotient

Let a monoid G act continuously and distributively on a topological additive group M, and let N be a G-stable additive subgroup of M. The restricted action AddSubgroup.restrictDistribMulAction of G on N is continuous for the subspace topology, because the inclusion of N in M is an equivariant topological embedding. Mathlib records this as the instance SMulMemClass.continuousSMul when the stability is part of a SMulMemClass structure; here the stability is a hypothesis, so the continuity is a theorem about the restricted action.

When M is commutative with separately continuous addition, the quotient action AddSubgroup.quotientDistribMulAction of G on M ⧸ N is continuous for the quotient topology as well, because the quotient map M → M ⧸ N is an open quotient map and the action on M ⧸ N is the descent of the continuous map (g, x) ↦ ↑(g • x) along G × M → G × (M ⧸ N).

Main results

• AddSubgroup.restrictDistribMulAction_continuousSMul: the restricted action of G on a G-stable additive subgroup is continuous.
• AddSubgroup.quotientDistribMulAction_continuousSMul: the quotient action of G on the quotient by a G-stable additive subgroup is continuous.

theorem AddSubgroup.restrictDistribMulAction_continuousSMul {G : Type u_1} [Monoid G] [TopologicalSpace G] {M : Type u_2} [AddGroup M] [TopologicalSpace M] [DistribMulAction G M] [ContinuousSMul G M] (N : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : ContinuousSMul G ↥N

The restricted action AddSubgroup.restrictDistribMulAction of G on a G-stable additive subgroup N of M is continuous for the subspace topology on N.

theorem AddSubgroup.quotientDistribMulAction_continuousSMul {G : Type u_1} [Monoid G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [SeparatelyContinuousAdd M] [DistribMulAction G M] [ContinuousSMul G M] (N : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : ContinuousSMul G (M ⧸ N)

The quotient action AddSubgroup.quotientDistribMulAction of G on the quotient M ⧸ N by a G-stable additive subgroup N is continuous for the quotient topology on M ⧸ N.