Compact modules over a compact ring

A compact module over a topological ring R is a topological R-module M that is a compact, totally disconnected topological additive group with continuous scalar action. For R compact these are the modules that are inverse limits of finite modules with surjective transition maps: the profinite modules. The case of interest is R = ℤ_p⟦Γ⟧, the completed group algebra of a profinite group Γ, whose compact modules are the objects Iwasawa theory and the classification of Demushkin groups compute with.

Two facts make a compact module accessible level by level. First, when R is compact, the open submodules of a nonarchimedean topological R-module form a basis of neighbourhoods of zero: an open additive subgroup V contains an open submodule, because by compactness of R and continuity of the action there is a neighbourhood W of zero with R • W ⊆ V, and the submodule spanned by W is open and lies in V. This is Mathlib's IsLinearTopology R M, and in a T1 module it gives separatedness: an element lying in every open submodule is zero. Second, when M is compact, a compatible family of elements of the quotients M ⧸ N, N ranging over the open submodules, comes from an element of M, by Cantor's intersection theorem applied to the closed cosets it describes. Together these are the inverse-limit description M ≅ lim_N M ⧸ N of a compact module over a compact ring.

The predicate IsCompactModule R M packages the four topological hypotheses so that they can be carried as a single hypothesis on a module whose topology is given by hand; its API restates the two facts above for it, shows that it passes to quotients by closed submodules, and records the witness that a compact totally disconnected topological ring is a compact module over itself.

Main definitions

• TauCeti.IsCompactModule R M: M is a compact totally disconnected topological R-module.

Main results

• Submodule.FG.isCompact: over a compact semiring, a finitely generated submodule of a topological module is compact.
• Submodule.span_eq_top_of_dense_closure: over a compact ring, a finite set spans a Hausdorff module as soon as a subset of its span generates a dense additive subgroup.
• OpenAddSubgroup.exists_submodule_isOpen_subset: over a compact ring, an open additive subgroup of a topological module contains an open submodule.
• TauCeti.NonarchimedeanAddGroup.isLinearTopology: over a compact ring, a nonarchimedean topological module is linearly topologized.
• TauCeti.IsLinearTopology.eq_zero_of_forall_mem_of_isOpen, TauCeti.IsLinearTopology.sInf_isOpen_eq_bot: in a T1 linearly topologized module the open submodules intersect in zero.
• TauCeti.IsLinearTopology.continuous_iff_forall_continuous_mkQ: a map into a linearly topologized module is continuous exactly when it is continuous modulo every open submodule.
• TauCeti.exists_forall_mkQ_eq: for a compact topological module, the map to compatible families in its quotients by open submodules is surjective.
• TauCeti.existsUnique_forall_mkQ_eq: a compact T1 linearly topologized module is the inverse limit of its quotients by open submodules.
• TauCeti.IsCompactModule.isLinearTopology, TauCeti.IsCompactModule.eq_zero_of_forall_mem_of_isOpen, TauCeti.IsCompactModule.existsUnique_forall_mkQ_eq, TauCeti.IsCompactModule.quotient, TauCeti.IsCompactModule.self: the same statements for the predicate, its stability under quotients by closed submodules, and the self-module witness.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 5.1.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), Section 1.5.

theorem Submodule.FG.isCompact {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace R] [CompactSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] {N : Submodule R M} (hN : N.FG) : IsCompact ↑N

A finitely generated submodule of a topological module over a compact semiring is compact. Unlike Mathlib's Submodule.isCompact_of_fg, the semiring need not be commutative; the completed group algebra of a nonabelian profinite group is the case that needs this.

theorem Submodule.span_eq_top_of_dense_closure {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace R] [CompactSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] [ContinuousSMul R M] {T S : Set M} (hT : T.Finite) (hS : S ⊆ ↑(span R T)) (hd : Dense ↑(AddSubgroup.closure S)) : span R T = ⊤

A finite set spans a Hausdorff module over a compact ring as soon as a subset of its span generates a dense additive subgroup: the span is compact, hence closed, and contains a dense set.

theorem OpenAddSubgroup.exists_submodule_isOpen_subset {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] [CompactSpace R] [ContinuousSMul R M] [SeparatelyContinuousAdd M] (V : OpenAddSubgroup M) : ∃ (N : Submodule R M), IsOpen ↑N ∧ ↑N ⊆ ↑V

Over a compact ring R, every open additive subgroup V of a topological R-module contains an open submodule: by compactness of R there is a neighbourhood W of zero with R • W ⊆ V, and the submodule spanned by W is open and contained in V.

@[instance 100]

instance TauCeti.NonarchimedeanAddGroup.isLinearTopology (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] [CompactSpace R] [ContinuousSMul R M] [NonarchimedeanAddGroup M] : IsLinearTopology R M

Over a compact ring, a nonarchimedean topological module is linearly topologized: its open submodules form a basis of neighbourhoods of zero.

theorem TauCeti.IsLinearTopology.eq_zero_of_forall_mem_of_isOpen {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [IsLinearTopology R M] [T1Space M] {x : M} (h : ∀ (N : Submodule R M), IsOpen ↑N → x ∈ N) : x = 0

In a T1 linearly topologized module, an element lying in every open submodule is zero.

@[simp]

theorem TauCeti.IsLinearTopology.sInf_isOpen_eq_bot (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [IsLinearTopology R M] [T1Space M] : sInf {N : Submodule R M | IsOpen ↑N} = ⊥

In a T1 linearly topologized module, the open submodules intersect in zero.

theorem TauCeti.IsLinearTopology.continuous_iff_forall_continuous_mkQ (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [IsLinearTopology R M] {X : Type u_3} [TopologicalSpace X] {f : X → M} : Continuous f ↔ ∀ (N : Submodule R M), IsOpen ↑N → Continuous (⇑N.mkQ ∘ f)

Continuity level by level. A map into a linearly topologized topological module is continuous exactly when its compositions with the quotient maps onto the quotients by the open submodules are continuous.

theorem TauCeti.exists_forall_mkQ_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [CompactSpace M] [SeparatelyContinuousAdd M] (x : (N : { N : Submodule R M // IsOpen ↑N }) → M ⧸ ↑N) (hx : ∀ ⦃N N' : { N : Submodule R M // IsOpen ↑N }⦄ (h : ↑N ≤ ↑N'), (Submodule.factor h) (x N) = x N') : ∃ (m : M), ∀ (N : { N : Submodule R M // IsOpen ↑N }), (↑N).mkQ m = x N

Surjectivity onto compatible families of open quotients. Every family of elements of M ⧸ N, with N ranging over the open submodules, that is compatible along the factor maps M ⧸ N → M ⧸ N' for N ≤ N' comes from an element of M, for M compact with separately continuous addition. The element is unique when M moreover has continuous addition and is T1 and linearly topologized (TauCeti.existsUnique_forall_mkQ_eq).

theorem TauCeti.existsUnique_forall_mkQ_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [CompactSpace M] [ContinuousAdd M] [IsLinearTopology R M] [T1Space M] (x : (N : { N : Submodule R M // IsOpen ↑N }) → M ⧸ ↑N) (hx : ∀ ⦃N N' : { N : Submodule R M // IsOpen ↑N }⦄ (h : ↑N ≤ ↑N'), (Submodule.factor h) (x N) = x N') : ∃! m : M, ∀ (N : { N : Submodule R M // IsOpen ↑N }), (↑N).mkQ m = x N

The inverse-limit description of a compact linearly topologized module: a compatible family of elements of the quotients M ⧸ N by the open submodules comes from exactly one element of M.

structure TauCeti.IsCompactModule (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] : Prop

A compact module over a topological ring R: a topological R-module that is a compact, totally disconnected topological additive group with continuous scalar action. Over a compact ring these are the modules that are inverse limits of finite modules with surjective transition maps. The four conditions are bundled as one predicate so that a module whose topology is given by hand can carry them as a single hypothesis.

• isTopologicalAddGroup : IsTopologicalAddGroup M

  the module is a topological additive group

• continuousSMul : ContinuousSMul R M

  the scalar action is continuous

• compactSpace : CompactSpace M

  the module is compact

• totallyDisconnectedSpace : TotallyDisconnectedSpace M

  the module is totally disconnected

theorem TauCeti.IsCompactModule.self {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [TotallyDisconnectedSpace R] : IsCompactModule R R

A compact totally disconnected topological ring is a compact module over itself.

theorem TauCeti.IsCompactModule.nonarchimedeanAddGroup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] (hM : IsCompactModule R M) : NonarchimedeanAddGroup M

A compact module is nonarchimedean: every neighbourhood of zero contains an open additive subgroup.

theorem TauCeti.IsCompactModule.t2Space {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] (hM : IsCompactModule R M) : T2Space M

A compact module is Hausdorff.

theorem TauCeti.IsCompactModule.isLinearTopology {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] (hM : IsCompactModule R M) [CompactSpace R] : IsLinearTopology R M

A compact module over a compact ring is linearly topologized: its open submodules form a basis of neighbourhoods of zero.

theorem TauCeti.IsCompactModule.eq_zero_of_forall_mem_of_isOpen {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] (hM : IsCompactModule R M) [CompactSpace R] {x : M} (h : ∀ (N : Submodule R M), IsOpen ↑N → x ∈ N) : x = 0

Separatedness. In a compact module over a compact ring, an element lying in every open submodule is zero.

theorem TauCeti.IsCompactModule.existsUnique_forall_mkQ_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] (hM : IsCompactModule R M) [CompactSpace R] (x : (N : { N : Submodule R M // IsOpen ↑N }) → M ⧸ ↑N) (hx : ∀ ⦃N N' : { N : Submodule R M // IsOpen ↑N }⦄ (h : ↑N ≤ ↑N'), (Submodule.factor h) (x N) = x N') : ∃! m : M, ∀ (N : { N : Submodule R M // IsOpen ↑N }), (↑N).mkQ m = x N

The inverse-limit description. A compact module over a compact ring is the inverse limit of its quotients by the open submodules: a compatible family of elements of those quotients comes from exactly one element of the module.

theorem TauCeti.IsCompactModule.quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [TopologicalSpace R] (hM : IsCompactModule R M) (N : Submodule R M) (hN : IsClosed ↑N) : IsCompactModule R (M ⧸ N)

Quotients stay compact. The quotient of a compact module by a closed submodule is a compact module. Closedness is what makes the quotient Hausdorff, and with the nonarchimedean property it gives total disconnectedness.