Separatedness and closed submodules of finite modules over a Huber ring

Let A be a complete Hausdorff Huber ring with a pair of definition (A₀, I) such that A₀ is noetherian, and let M be a finitely generated A-module with its natural topology (IsModuleTopology A M). This file proves that M is Hausdorff and that every A-submodule of M is closed (Huber, A generalization of formal schemes and rigid analytic varieties, Lemma 2.3(ii)).

The ring of definition of a complete Hausdorff Huber ring is I-adically complete (TauCeti.Huber.PairOfDefinition.isAdicComplete_idealOfDefinition). When A₀ is noetherian, every finitely generated A₀-submodule M₀ ⊆ M is therefore I-adically complete, by IsAdicComplete.of_finite, and in particular I-adically separated. If M₀ spans M over A, the submodules Iⁿ • M₀ form a neighbourhood basis of 0 in M, so this separatedness makes M Hausdorff; applied to M ⧸ N, it makes every submodule N closed. Completeness of M itself needs no noetherian hypothesis: it holds over any complete first-countable ring, by IsOpenQuotientMap.completeSpace (see TauCeti.completeSpace_moduleTopology).

These are the facts about finite modules that Huber's sheafiness theorem for rings with a noetherian ring of definition uses, alongside the strictness of linear maps (TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing). For complete noetherian Tate rings the corresponding statements are TauCeti.Huber.IsTateRing.t2Space_moduleTopology and TauCeti.Huber.isClosed_of_isNoetherian; here A need not be Tate.

Main results

• TauCeti.Huber.PairOfDefinition.t2Space_of_isNoetherianRing: a finite module is Hausdorff.
• TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing: every submodule of a finite module is closed.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, Lemma 2.3(ii) and its proof.
• A. Grothendieck, J. Dieudonné, Éléments de géométrie algébrique I, Chapitre 0, (7.3.6).

theorem TauCeti.Huber.PairOfDefinition.t2Space_of_isNoetherianRing {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T0Space A] [IsTopologicalRing A] [Module.Finite A M] [TopologicalSpace M] [IsModuleTopology A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] : T2Space M

Finite modules over a complete Huber ring with a noetherian ring of definition are Hausdorff (Huber, Lemma 2.3(ii)). If A is complete and Hausdorff with a noetherian ring of definition, every finite A-module is Hausdorff in its natural topology.

theorem TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T0Space A] [IsTopologicalRing A] [Module.Finite A M] [TopologicalSpace M] [IsModuleTopology A M] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] (N : Submodule A M) : IsClosed ↑N

Submodules of finite modules over a complete Huber ring with a noetherian ring of definition are closed (Huber, Lemma 2.3(ii)). If A is complete and Hausdorff with a noetherian ring of definition, every A-submodule of a finite A-module is closed in its natural topology.