Discrete topological G-modules: conventions and basic facts

Convention — no new structures. Throughout the project, a topological G-module is a type M with the Mathlib classes

[AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M],

a discrete G-module additionally has [DiscreteTopology M] (which already implies IsTopologicalAddGroup M by instance), and a finite one [Finite M]. No bundling class is introduced: instance search composes these freely (products, subgroups, ZMod n, μ_n, …), and each B-axiom quantifies over exactly the classes it needs.

This file stress-tests the convention by proving the facts that make discrete modules over profinite groups smooth in the classical sense:

• GQ2.isOpen_stabilizer — point stabilizers are open;
• GQ2.isOpen_iInf_stabilizer — for finite M, the kernel of the action is open;
• GQ2.exists_openNormalSubgroup_smul_eq_self — over a profinite G, a finite discrete module is acted on trivially by some open normal subgroup, i.e. the action factors through a finite quotient — the bridge between continuous cohomology and finite group cohomology.

theorem GQ2.isOpen_stabilizer {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : M) : IsOpen ↑(MulAction.stabilizer G m)

In a discrete module, point stabilizers are open subgroups.

theorem GQ2.isOpen_iInf_stabilizer {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] : IsOpen ↑(⨅ (m : M), MulAction.stabilizer G m)

In a finite discrete module, the kernel of the action (the intersection of all point stabilizers) is an open subgroup.

theorem GQ2.exists_openNormalSubgroup_smul_eq_self {G : Type u_1} [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ∃ (U : OpenNormalSubgroup G), ∀ u ∈ U, ∀ (m : M), u • m = m

Smoothness: a finite discrete module over a profinite group is acted on trivially by an open normal subgroup — the action factors through a finite quotient of G. This is the structural fact connecting continuous cohomology of G to ordinary cohomology of its finite quotients.