Strict morphisms out of a finite module over a Tate ring

Let A be a complete Hausdorff Tate ring, let M be a finite A-module and let N be a noetherian A-module, each carrying a complete Hausdorff first-countable topology making it a topological A-module. This file proves that every linear map M →ₗ[A] N is strict: it is open onto its image, and in particular continuous, with no continuity hypothesis imposed on it. This is Wedhorn, Adic Spaces, Proposition 6.18(2).

Wedhorn states the target side as a finite module over a noetherian ring; that case is the instance isNoetherian_of_isNoetherianRing_of_finite of the noetherian target asked for here.

The strictness of a morphism is what makes a presentation of a module by finite free modules a topological presentation, so this is the result that lets finite modules over a noetherian Tate ring — where finiteness of the target already gives the noetherian hypothesis — be glued and localised topologically. The open mapping theorem it rests on is Henkel's, credited in TauCeti.RingTheory.Huber.OpenMapping.

Main result

• LinearMap.isStrictMap_of_module_finite: a linear map from a finite module to a noetherian module, over a complete Hausdorff Tate ring, is strict.

References

• T. Wedhorn, Adic Spaces, Proposition 6.18(2).

theorem LinearMap.isStrictMap_of_module_finite {A : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [CompleteSpace A] [T0Space A] [(uniformity A).IsCountablyGenerated] [IsTopologicalRing A] [TauCeti.Huber.IsTateRing A] [AddCommGroup M] [UniformSpace M] [IsUniformAddGroup M] [CompleteSpace M] [(uniformity M).IsCountablyGenerated] [T0Space M] [Module A M] [ContinuousSMul A M] [Module.Finite A M] [AddCommGroup N] [UniformSpace N] [IsUniformAddGroup N] [CompleteSpace N] [(uniformity N).IsCountablyGenerated] [T0Space N] [Module A N] [ContinuousSMul A N] [IsNoetherian A N] (f : M →ₗ[A] N) : Topology.IsStrictMap ⇑f

A linear map from a finite module to a noetherian module over a complete Tate ring is strict (Wedhorn, Adic Spaces, Proposition 6.18(2)): it is open onto its image.

No continuity hypothesis is imposed on f; continuity is part of the conclusion, obtained from it by Topology.IsStrictMap.continuous.