Submodules with a module-finite closure are closed

A submodule of a complete, metrisable module over a complete Tate ring whose topological closure is module-finite is itself closed. This is Bosch–Güntzer–Remmert §3.7.2/1 in its closure form, and it is the closedness prerequisite on the route to Wedhorn 6.17/6.18. Its consequence for a noetherian ring — every submodule of a finitely generated module is closed — is what makes a finite presentation of a finite module strict, which is the form in which Wedhorn's Remark 8.29 consumes Proposition 6.18(2).

The proof is one application of TauCeti.Huber.eq_top_of_dense_of_module_finite, made inside the closure N.topologicalClosure rather than inside the ambient module. That closure is closed in a complete space, so it is complete — the one instance that has to be supplied by hand; it is a uniform additive group with a countably generated uniformity by Submodule.isUniformAddGroup and Submodule.isCountablyGenerated_uniformity; and it is module-finite by hypothesis. Inside that closure the submodule N is dense, by the very definition of the closure. So N is everything in the closure, that is N.topologicalClosure = N, and N is closed because its closure is.

Main results

• TauCeti.Huber.isClosed_of_module_finite_topologicalClosure: a submodule whose topological closure is module-finite is closed.
• TauCeti.Huber.isClosed_of_isNoetherian: in a noetherian module, every submodule is closed.
• TauCeti.Huber.IsTateRing.exists_presentation_isStrictMap_isOpenMap: over a complete noetherian Tate ring, a finite module with its module topology has a presentation Aⁿ →[u] Aᵐ →[p] M → 0 with u strict and p open — Wedhorn's Remark 8.29's use of Proposition 6.18(2).

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §3.7.2/1.
• Wedhorn, Adic Spaces, Propositions 6.17–6.18 and Remark 8.29.

Provenance

Adapted from the AINTLIB development (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9, file projects/AdicSpaces/Adic spaces/WedhornBanachTheorem.lean, where the same statement is fg_topologicalClosure_isClosed. The argument is AINTLIB's, and the density step follows its proof closely. Three things differ. AINTLIB establishes the uniform-group, countable-generation, separation and ContinuousSMul instances on the closure by hand; here all four are found by instance search — the first two from Submodule.isUniformAddGroup and Submodule.isCountablyGenerated_uniformity, the last from this repository's ContinuousSMul instance on a submodule — so only completeness is supplied. The engine is this repository's TauCeti.Huber.eq_top_of_dense_of_module_finite, stated with T0Space, rather than AINTLIB's T2Space-based eq_top_of_dense_of_finite. And the passage from N' = ⊤ back to N.topologicalClosure ≤ N is Submodule.comap_subtype_eq_top rather than AINTLIB's element-level unfolding.

TauCeti.Huber.isClosed_of_isNoetherian follows the same development's _sub_lemma_L3_1b_fg_submodule_closed (same file, line 778 at the commit above), which is where the plan of discharging closedness from noetherianity is taken from. Only the plan is shared: that proof concludes closedness from completeness of the finitely generated submodule, via its _sub_lemma_L3_1a_completion_fg_complete and completeSpace_coe_iff_isComplete, whereas the proof here routes through this file's own isClosed_of_module_finite_topologicalClosure and so never mentions completeness of N. The hypotheses differ too: that statement asks for [IsNoetherianRing A] together with an explicit (hN_fg : N.FG), while [IsNoetherian A V] here covers every submodule at once and needs no finite-generation argument at the call site. Sharing only the plan is not a stylistic choice: that proof reaches completeness through _sub_lemma_L3_1a_completion_fg_complete, whose body in that development is sorry (same file, line 611), so its route is not available to import even in principle.

theorem TauCeti.Huber.isClosed_of_module_finite_topologicalClosure {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsTateRing A] {V : Type u_2} [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V] [CompleteSpace V] [(uniformity V).IsCountablyGenerated] [T0Space V] [Module A V] [ContinuousSMul A V] (N : Submodule A V) (hfin : Module.Finite A ↥N.topologicalClosure) : IsClosed ↑N

A submodule whose topological closure is module-finite is closed (Bosch–Güntzer–Remmert §3.7.2/1).

Working inside N.topologicalClosure, which is complete because it is closed in a complete space, the submodule N is dense and that closure is module-finite, so eq_top_of_dense_of_module_finite gives N = N.topologicalClosure.

theorem TauCeti.Huber.isClosed_of_isNoetherian {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T2Space A] [IsTopologicalRing A] [IsTateRing A] {V : Type u_2} [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V] [CompleteSpace V] [(uniformity V).IsCountablyGenerated] [T0Space V] [Module A V] [ContinuousSMul A V] [IsNoetherian A V] (N : Submodule A V) : IsClosed ↑N

In a noetherian module, every submodule is closed.

Every submodule of a noetherian module is finitely generated — the topological closure of N included. That closure is therefore module-finite, which is exactly what TauCeti.Huber.isClosed_of_module_finite_topologicalClosure asks of it.

The hypothesis is on the module and not on the ring, because that is all the argument uses: the noetherian-base, module-finite case is recovered from Mathlib's instance isNoetherian_of_isNoetherianRing_of_finite, so no separate statement of it is needed.

This is the closedness statement of Wedhorn, Adic Spaces, Proposition 6.17, for a module whose complete metrisable topology is given. It is not that proposition: 6.17 is about the canonical topology of 6.18(1), and the construction of that topology, together with its uniqueness, is not available here.

theorem TauCeti.Huber.IsTateRing.exists_presentation_isStrictMap_isOpenMap {A : Type u_3} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [(uniformity A).IsCountablyGenerated] [T0Space A] [NonarchimedeanRing A] [IsTateRing A] [IsNoetherianRing A] {M : Type u_4} [AddCommGroup M] [Module A M] [Module.Finite A M] [TopologicalSpace M] [IsModuleTopology A M] : ∃ (n : ℕ) (m : ℕ) (u : (Fin n → A) →ₗ[A] Fin m → A) (p : (Fin m → A) →ₗ[A] M), Continuous ⇑u ∧ Continuous ⇑p ∧ Function.Surjective ⇑p ∧ Function.Exact ⇑u ⇑p ∧ Topology.IsStrictMap ⇑u ∧ IsOpenMap ⇑p

A finite module over a complete noetherian Tate ring has a strict finite presentation. This is the sentence Wedhorn's Remark 8.29 opens with: "we find a presentation Aⁿ →[u] Aᵐ →[p] M → 0 (because A is noetherian). Proposition 6.18(2) shows that u and p are continuous and open onto its image."

M carries its canonical topology, which is Mathlib's module topology: every complete first-countable module topology on a finite module is the module topology (TauCeti.Huber.IsTateRing.isModuleTopology), so IsModuleTopology A M is the topology Proposition 6.18(1) speaks of, and nothing else is asked of M. The presentation is Mathlib's Module.FinitePresentation.exists_fin', available because a finite module over a noetherian ring is finitely presented. Both maps are continuous by IsModuleTopology.continuous_of_linearMap, p is open by IsModuleTopology.isOpenMap_of_surjective — the module topology on M is the quotient topology along any linear surjection from Aᵐ — and u is strict by TauCeti.Huber.IsTateRing.isStrictMap_of_isClosed_range, its range being closed in Aᵐ by TauCeti.Huber.isClosed_of_isNoetherian. That closedness is the one place, beyond the existence of the presentation, where A being noetherian enters, and the open mapping theorem is spent on the free module Aᵐ, not on M.