Continuous actions on a topological module

Let a monoid Γ act continuously and R-linearly on a topological R-module M. Two compactness arguments, both instances of the tube lemma, control the interaction of the action with the open submodules of M.

• When Γ is compact, the invariant core V.invariantCore Γ of an open submodule V is open: the set of pairs (γ, x) with γ • x ∈ V is an open neighbourhood of Γ × {0}, so it contains a tube Γ × W, and W lies in the core. Hence the Γ-invariant open submodules are cofinal among the open submodules; in a linearly topologized module they form a basis of neighbourhoods of zero, so continuity into M and equality in a Hausdorff M can both be tested modulo the invariant open submodules.
• When Γ is a group and M is compact, the action on the quotient M ⧸ V by an invariant open submodule V has open kernel: the set of pairs (γ, x) with γ • x - x ∈ V is an open neighbourhood of {1} × M, so it contains a tube U × M, and U lies in the kernel. The kernel is recorded as the open normal subgroup Submodule.quotientActionKernel hV hVo.

These are the two facts that turn a compact module with a continuous action of a profinite group Γ into a module over the completed group algebra of Γ: the action on each finite quotient M ⧸ V factors through a finite quotient of Γ, and the quotients M ⧸ V by the invariant open V determine M.

Main definitions

• Submodule.quotientActionKernel: the kernel of the action of Γ on the quotient by an invariant open submodule of a compact module, as an open normal subgroup of Γ.

Main results

• Submodule.isOpen_invariantCore: for compact Γ, the invariant core of an open submodule is open.
• Submodule.isOpen_ker_quotientToModuleEnd: for compact M, the action on the quotient by an invariant open submodule has open kernel.
• TauCeti.IsLinearTopology.continuous_iff_forall_invariant_continuous_mkQ, TauCeti.IsLinearTopology.eq_of_forall_invariant_mkQ_eq: for compact Γ, continuity into a linearly topologized M, and equality in a T1 one, can be tested modulo the Γ-invariant open submodules.

theorem Submodule.isOpen_invariantCore (Γ : Type u_1) {R : Type u_2} {M : Type u_3} [Monoid Γ] [TopologicalSpace Γ] [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [ContinuousSMul Γ M] [CompactSpace Γ] [SeparatelyContinuousAdd M] (V : Submodule R M) (hV : IsOpen ↑V) : IsOpen ↑(invariantCore Γ V)

Invariant cores of open submodules are open when the acting monoid is compact: by the tube lemma, a neighbourhood of 0 is carried into V by the whole of Γ.

theorem Submodule.isOpen_ker_quotientToModuleEnd {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Group Γ] [TopologicalSpace Γ] [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [ContinuousSMul Γ M] [SeparatelyContinuousMul Γ] [CompactSpace M] [IsTopologicalAddGroup M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hVo : IsOpen ↑V) : IsOpen ↑(quotientToModuleEnd hV).ker

The action on an open quotient has open kernel when the module is compact: by the tube lemma, a neighbourhood of 1 moves every element of M by an element of V.

def Submodule.quotientActionKernel {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Group Γ] [TopologicalSpace Γ] [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [ContinuousSMul Γ M] [SeparatelyContinuousMul Γ] [CompactSpace M] [IsTopologicalAddGroup M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hVo : IsOpen ↑V) : OpenNormalSubgroup Γ

The kernel of the action of Γ on the quotient of a compact module by an invariant open submodule, as an open normal subgroup of Γ.

Equations

• Submodule.quotientActionKernel hV hVo = { toSubgroup := (Submodule.quotientToModuleEnd hV).ker, isOpen' := ⋯, isNormal' := ⋯ }

@[simp]

theorem Submodule.quotientActionKernel_toSubgroup {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Group Γ] [TopologicalSpace Γ] [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [ContinuousSMul Γ M] [SeparatelyContinuousMul Γ] [CompactSpace M] [IsTopologicalAddGroup M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hVo : IsOpen ↑V) : ↑(quotientActionKernel hV hVo).toOpenSubgroup = (quotientToModuleEnd hV).ker

theorem TauCeti.IsLinearTopology.continuous_iff_forall_invariant_continuous_mkQ (Γ : Type u_1) (R : Type u_2) {M : Type u_3} [Monoid Γ] [TopologicalSpace Γ] [CompactSpace Γ] [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [ContinuousSMul Γ M] [IsLinearTopology R M] [IsTopologicalAddGroup M] {X : Type u_4} [TopologicalSpace X] {f : X → M} : Continuous f ↔ ∀ (V : Submodule R M), IsOpen ↑V → (∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) → Continuous (⇑V.mkQ ∘ f)

Continuity modulo the invariant open submodules. For a compact monoid acting continuously on a linearly topologized topological module M, a map into M is continuous exactly when it is continuous modulo every Γ-invariant open submodule.

theorem TauCeti.IsLinearTopology.eq_of_forall_invariant_mkQ_eq (Γ : Type u_1) {R : Type u_2} {M : Type u_3} [Monoid Γ] [TopologicalSpace Γ] [CompactSpace Γ] [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [ContinuousSMul Γ M] [IsLinearTopology R M] [ContinuousAdd M] [T1Space M] {m m' : M} (h : ∀ (V : Submodule R M), IsOpen ↑V → (∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) → V.mkQ m = V.mkQ m') : m = m'

Separation by the invariant open submodules. For a compact monoid acting continuously on a T1 linearly topologized topological module, two elements that agree modulo every Γ-invariant open submodule are equal.