The topological Nakayama lemma

Let R be a commutative topological semiring and I a finitely generated ideal of R all of whose elements are topologically nilpotent. For a topological R-module M, compactness takes over the role that finite generation plays in the algebraic Nakayama lemma (Submodule.le_of_le_smul_of_le_jacobson): if P is a compact submodule and N a closed submodule with P ≤ N ⊔ I • P, then P ≤ N. No finiteness of P and no Jacobson radical hypothesis is needed.

The proof treats one generator a of I at a time. If P ≤ N ⊔ a • P, then P ≤ N ⊔ aⁿ • P for every n; continuity of the action and compactness of P make aⁿ • P lie in any prescribed neighbourhood of zero for large n, so every element of P lies in the closure of N. Adding the remaining generators one at a time keeps the submodule closed, because the sum of a closed set and a compact set in a topological group is closed.

The typical application is to a noetherian local ring with its adic topology and I its maximal ideal 𝔪, whose elements are then topologically nilpotent (WithIdeal.isTopologicallyNilpotent_of_mem). The main example is the Iwasawa algebra Λ = O⟦T⟧ of a complete discrete valuation ring O with finite residue field: Λ is compact, its (ϖ, T)-adic topology agrees with the coefficientwise topology, and each element of its maximal ideal is topologically nilpotent there (MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeff). For a compact Hausdorff Λ-module M with continuous action this gives: M = 0 once M = 𝔪M; M is generated by lifts of any finite spanning set of M ⧸ 𝔪M, so M is finitely generated once M ⧸ 𝔪M is finite; and a continuous linear map of compact modules is surjective once it is surjective modulo 𝔪. Compactness cannot be dropped: ℚ_p ⧸ ℤ_p with the discrete topology is a nonzero ℤ_p-module equal to p times itself.

Main results

• Submodule.le_of_le_smul_of_isCompact: the topological Nakayama lemma, P ≤ N ⊔ I • P implies P ≤ N for P compact and N closed.
• Submodule.eq_bot_of_le_smul_of_isCompact: a compact submodule N of a T1 module with N ≤ I • N is zero.
• Submodule.span_eq_top_of_span_image_mkQ_eq_top: over a compact ring, a finite subset of a compact Hausdorff module whose image spans M ⧸ I • ⊤ spans M.
• Module.Finite.of_quotient_smul_top: over a compact ring, a compact Hausdorff module is finitely generated once M ⧸ I • ⊤ is.
• LinearMap.surjective_of_surjective_comp_mkQ_of_compactSpace: a continuous linear map between compact modules, with Hausdorff target, is surjective once it is surjective modulo I.

References

• P. N. Balister and S. Howson, Note on Nakayama's lemma for compact Λ-modules, Asian J. Math. 1 (1997), 224–229.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Chapter V, §2.

theorem Submodule.le_of_le_smul_of_isCompact {R : Type u_1} {M : Type u_2} [CommSemiring R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul R M] {I : Ideal R} {N P : Submodule R M} (hI : I.FG) (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) (hN : IsClosed ↑N) (hP : IsCompact ↑P) (hNP : P ≤ N ⊔ I • P) : P ≤ N

The topological Nakayama lemma. Let I be a finitely generated ideal of topologically nilpotent elements. If P is a compact submodule and N a closed submodule of a topological module with P ≤ N ⊔ I • P, then P ≤ N. Compactness of P replaces the finite generation hypothesis of Submodule.le_of_le_smul_of_le_jacobson.

theorem Submodule.eq_bot_of_le_smul_of_isCompact {R : Type u_1} {M : Type u_2} [CommSemiring R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul R M] [T1Space M] {I : Ideal R} {N : Submodule R M} (hI : I.FG) (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) (hN : IsCompact ↑N) (hIN : N ≤ I • N) : N = ⊥

The topological Nakayama lemma, vanishing form: if I is a finitely generated ideal of topologically nilpotent elements, a compact submodule N of a T1 topological module with N ≤ I • N is zero.

theorem Submodule.span_eq_top_of_span_image_mkQ_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul R M] [CompactSpace R] [CompactSpace M] [T2Space M] {I : Ideal R} (hI : I.FG) (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) {s : Set M} (hs : s.Finite) (hspan : span R (⇑(I • ⊤).mkQ '' s) = ⊤) : span R s = ⊤

Lifting generators along M → M ⧸ I • M. Over a compact ring, let I be a finitely generated ideal of topologically nilpotent elements and M a compact Hausdorff module. A finite set whose image spans M ⧸ I • ⊤ spans M.

theorem Module.Finite.of_quotient_smul_top {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul R M] [CompactSpace R] [CompactSpace M] [T2Space M] {I : Ideal R} (hI : I.FG) (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) [Module.Finite R (M ⧸ I • ⊤)] : Module.Finite R M

Finite generation from the reduction modulo I. Over a compact ring, let I be a finitely generated ideal of topologically nilpotent elements. A compact Hausdorff topological module M is finitely generated once M ⧸ I • ⊤ is; in particular once M ⧸ I • ⊤ is finite (Module.Finite.of_finite).

theorem LinearMap.surjective_of_surjective_comp_mkQ_of_compactSpace {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] [TopologicalSpace M'] [CompactSpace M'] [CompactSpace M] [T2Space M] {I : Ideal R} (hI : I.FG) (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) (f : M' →ₗ[R] M) (hf : Continuous ⇑f) (surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)) : Function.Surjective ⇑f

Surjectivity modulo I. Let I be a finitely generated ideal of topologically nilpotent elements and f : M' →ₗ[R] M a continuous linear map between compact topological modules, with M Hausdorff. If f is surjective modulo I, that is M' → M ⧸ I • M is surjective, then f is surjective. Compare LinearMap.surjective_of_surjective_comp_mkQ for finite modules.