Closed immersions are monomorphisms

Let (A, A⁺) be a Huber pair and J ⊆ A an ideal. Over a rational open R(T/s) of Spa(A, A⁺), the coordinate ring of its preimage in Spa(A ⧸ J, (A ⧸ J)⁺) is the quotient (A ⧸ J)⟨q(T)/q(s)⟩ of A⟨T/s⟩ (TauCeti.Huber.PairOfDefinition.Presentation.mapHom_quotientMk_surjective). Since the rational opens of Spa(A ⧸ J, (A ⧸ J)⁺) of this form are a basis, every germ of the structure presheaf of Spa(A ⧸ J, (A ⧸ J)⁺) comes from a germ of that of Spa(A, A⁺): the stalk maps of the quotient morphism are surjective. A closed immersion is locally on the target a quotient morphism, so its stalk maps are surjective as well.

A morphism of sheafed spaces which is injective on points and has surjective stalk maps is a monomorphism (Mathlib's AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi), as two morphisms into its source with the same composite agree on points and on stalks, and sections of a sheaf are determined by their germs. So closed immersions are monomorphisms among sheafy pre-adic spaces and among adic spaces. This is the uniqueness half of the universal property of a closed immersion: a morphism into the target factors through it in at most one way. For affinoid sources and morphisms induced by morphisms of Huber pairs killing J, the factorisation exists by TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceComap_quotientLift_comp_quotientComap.

Main results

• TauCeti.ValuationSpectrum.stalkMap_presentationLimitPreAdicSpaceQuotientComap_surjective: the stalk maps of the quotient morphism Spa(A ⧸ J, (A ⧸ J)⁺) ⟶ Spa(A, A⁺) are surjective.
• TauCeti.PreAdicSpace.IsClosedImmersion.stalkMap_surjective: the stalk maps of a closed immersion are surjective.
• TauCeti.SheafyPreAdicSpace.mono_of_isClosedImmersion and TauCeti.AdicSpace.mono_of_isClosedImmersion: closed immersions are monomorphisms in the categories of sheafy pre-adic spaces and of adic spaces.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 7.38 and §8.1.

theorem TauCeti.ValuationSpectrum.stalkMap_presentationLimitPreAdicSpaceQuotientComap_surjective {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] (S : Huber.Pair A) (P : Huber.PairOfDefinition A) (hP : P.ringOfDefinition ≤ S.plus) (J : Ideal A) (hsheaf : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa (S.quotient J).plus)) (presentationLimitPresheaf (P.quotient J) (S.quotient J).plus)) (x : ↑(presentationLimitPreAdicSpace (P.quotient J) (S.quotient J).plus ⋯ ⋯).toTopCat) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (PreAdicSpace.Hom.stalkMap (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf) x))

The stalk maps of the quotient morphism Spa(A ⧸ J, (A ⧸ J)⁺) ⟶ Spa(A, A⁺) are surjective: every germ at x is the germ of an element of (A ⧸ J)⟨q(T)/q(s)⟩ for a rational neighbourhood R(T/s) of the image of x, and such elements lift to A⟨T/s⟩.

theorem TauCeti.PreAdicSpace.IsClosedImmersion.stalkMap_surjective {X Y : PreAdicSpace} {f : X ⟶ Y} (hf : IsClosedImmersion f) (x : ↑X.toTopCat) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x))

The stalk maps of a closed immersion are surjective: around each point of the target, the closed immersion is a quotient morphism up to isomorphisms and restrictions to opens, all of which have bijective stalk maps.

theorem TauCeti.SheafyPreAdicSpace.mono_of_isClosedImmersion {X Y : SheafyPreAdicSpace} (f : X ⟶ Y) (hf : PreAdicSpace.IsClosedImmersion f.hom) : CategoryTheory.Mono f

Closed immersions of sheafy pre-adic spaces are monomorphisms: a closed immersion is injective on points and has surjective stalk maps, so it is a monomorphism of the underlying sheafed spaces of rings, to which morphisms of sheafy pre-adic spaces are faithfully sent.

theorem TauCeti.AdicSpace.mono_of_isClosedImmersion {X Y : AdicSpace} (f : X ⟶ Y) (hf : PreAdicSpace.IsClosedImmersion f.hom) : CategoryTheory.Mono f

Closed immersions of adic spaces are monomorphisms: a morphism into an adic space factors through a closed immersion in at most one way.