Strict linear maps of finite modules over a Huber ring with a noetherian ring of definition

Let A be a Huber ring with a pair of definition (A₀, I) such that A₀ is noetherian. Every A-linear map u : M → N between finitely generated A-modules with their natural topologies is strict: it is continuous, and open onto its image with the subspace topology (Huber, A generalization of formal schemes and rigid analytic varieties, Lemma 2.3(i)). Neither completeness nor the Tate property is assumed; the complete Tate case, with a noetherian target module in place of a noetherian ring of definition, is LinearMap.isStrictMap_of_module_finite.

Strictness is what lets a complex of finite modules be completed term by term without losing exactness (AddMonoidHom.exact_completion), which is how algebraic Čech complexes become complexes of completed modules in Huber's sheafiness theorem.

Main results

• TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing: every linear map between finite modules with their natural topologies is strict.

References

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

theorem TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] [TopologicalSpace M] [IsModuleTopology A M] {N : Type u_3} [AddCommGroup N] [Module A N] [Module.Finite A N] [TopologicalSpace N] [IsModuleTopology A N] (P : PairOfDefinition A) [IsNoetherianRing ↥P.ringOfDefinition] (u : M →ₗ[A] N) : Topology.IsStrictMap ⇑u

Linear maps of finite modules over a Huber ring with a noetherian ring of definition are strict (Huber, Lemma 2.3(i)). If A₀ is noetherian, every A-linear map between finitely generated A-modules with their natural topologies is continuous and open onto its image.