Closed immersions of pre-adic spaces

Let (A, A⁺) be a Huber pair and J ⊆ A an ideal. The quotient Huber pair (A ⧸ J, (A ⧸ J)⁺) has as plus ring the integral closure of the image of A⁺, and the quotient map induces a closed embedding Spa(A ⧸ J, (A ⧸ J)⁺) → Spa(A, A⁺) onto the points whose support contains J (Wedhorn, Proposition 7.38). When the structure presheaf of the quotient pair is a sheaf, this map underlies a morphism of pre-adic spaces, the quotient morphism.

Closed immersions are defined affinoid-locally from these models: a morphism f : X ⟶ Y of pre-adic spaces is a closed immersion when every point of Y has an open neighbourhood V over which f is isomorphic to the quotient morphism of a Huber pair by a closed ideal with sheafy quotient. The ideal is required to be closed; for a complete Hausdorff Huber ring A this makes A ⧸ J complete and Hausdorff again.

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceQuotientComap: the quotient morphism Spa(A ⧸ J, (A ⧸ J)⁺) ⟶ Spa(A, A⁺) of pre-adic spaces, for a sheafy quotient pair.
• TauCeti.PreAdicSpace.IsClosedImmersion: a morphism of pre-adic spaces that is, locally on the target, isomorphic to a quotient morphism by a closed ideal.

Main results

• TauCeti.ValuationSpectrum.isClosedEmbedding_presentationLimitPreAdicSpaceQuotientComap_base and TauCeti.ValuationSpectrum.range_presentationLimitPreAdicSpaceQuotientComap_base: the quotient morphism is a closed embedding of the underlying spaces, onto the points whose support contains J.
• TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceComap_quotientLift_comp_quotientComap: the morphism induced by a morphism of Huber pairs annihilating J factors through the quotient morphism.
• TauCeti.ValuationSpectrum.isClosedImmersion_presentationLimitPreAdicSpaceQuotientComap: the quotient morphism by a closed ideal is a closed immersion.
• isClosedImmersion_presentationLimitPreAdicSpaceComap_of_isQuotientMapping: the morphism induced by a quotient mapping of Huber pairs with closed kernel is a closed immersion.
• TauCeti.PreAdicSpace.IsClosedImmersion.isClosedEmbedding: a closed immersion is a closed embedding of the underlying topological spaces.
• TauCeti.PreAdicSpace.IsClosedImmersion.respectsIso: being a closed immersion is invariant under isomorphisms of the source and of the target.

References

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

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceQuotientComap {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)) : presentationLimitPreAdicSpace (P.quotient J) (S.quotient J).plus ⋯ ⋯ ⟶ presentationLimitPreAdicSpace P S.plus ⋯ hP

The quotient morphism Spa(A ⧸ J, (A ⧸ J)⁺) ⟶ Spa(A, A⁺) of pre-adic spaces, for a Huber pair (A, A⁺) and an ideal J whose quotient pair has a sheaf as structure presheaf. It is the morphism induced by the quotient map A → A ⧸ J.

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceQuotientComap_def {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)) : presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf = presentationLimitPreAdicSpaceComap (Ideal.Quotient.mk J) ⋯ ⋯ ⋯ ⋯ hP ⋯ hsheaf

The quotient morphism is the morphism of pre-adic spaces induced by the quotient map A → A ⧸ J.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceQuotientComap_base_apply_val {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) : ↑((CategoryTheory.ConcreteCategory.hom (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf).base) x) = comap (Ideal.Quotient.mk J) ↑x

The map of underlying spaces of the quotient morphism pulls valuations back along the quotient map A → A ⧸ J.

theorem TauCeti.ValuationSpectrum.coe_presentationLimitPreAdicSpaceQuotientComap_base {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)) : ⇑(CategoryTheory.ConcreteCategory.hom (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf).base) = (S.quotientHom J).spaComap

The map of underlying spaces of the quotient morphism is the map of adic spectra induced by the quotient morphism of Huber pairs.

theorem TauCeti.ValuationSpectrum.isClosedEmbedding_presentationLimitPreAdicSpaceQuotientComap_base {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)) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf).base)

Wedhorn Proposition 7.38 for pre-adic spaces: the quotient morphism is a closed embedding of the underlying topological spaces.

theorem TauCeti.ValuationSpectrum.range_presentationLimitPreAdicSpaceQuotientComap_base {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)) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf).base) = Subtype.val ⁻¹' {v : ValuationSpectrum A | J ≤ v.supp}

The image of the quotient morphism consists of the points of Spa(A, A⁺) whose support contains J.

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpaceComap_quotientLift_comp_quotientComap {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)) {B : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [Huber.IsHuberRing B] {T : Huber.Pair B} (P' : Huber.PairOfDefinition B) (hP' : P'.ringOfDefinition ≤ T.plus) (f : S.Hom T) (hf : J ≤ RingHom.ker f.toRingHom) (hsheafT : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa T.plus)) (presentationLimitPresheaf P' T.plus)) : CategoryTheory.CategoryStruct.comp (presentationLimitPreAdicSpaceComap (Huber.Pair.Hom.quotientLift J f hf).toRingHom ⋯ ⋯ ⋯ ⋯ ⋯ hP' hsheafT) (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf) = presentationLimitPreAdicSpaceComap f.toRingHom ⋯ ⋯ ⋯ ⋯ hP hP' hsheafT

The factorisation property of the quotient morphism (Wedhorn, Proposition 7.38): if a morphism f : (A, A⁺) → (B, B⁺) of Huber pairs annihilates J, the morphism Spa(B, B⁺) ⟶ Spa(A, A⁺) of pre-adic spaces induced by f factors through the quotient morphism, as the morphism induced by the factorisation (A ⧸ J, (A ⧸ J)⁺) → (B, B⁺) of f (TauCeti.Huber.Pair.Hom.quotientLift) followed by the quotient morphism.

def TauCeti.PreAdicSpace.IsClosedImmersion {X Y : PreAdicSpace} (f : X ⟶ Y) : Prop

A morphism f : X ⟶ Y of pre-adic spaces is a closed immersion when it is, locally on Y, the quotient morphism of a Huber pair by a closed ideal with sheafy quotient: every point of Y has an open neighbourhood V together with a Huber pair (A, A⁺), a closed ideal J ⊆ A for which Spa(A ⧸ J, (A ⧸ J)⁺) has a sheaf as structure presheaf, and isomorphisms identifying Y restricted to V with Spa(A, A⁺) and X restricted to f⁻¹(V) with Spa(A ⧸ J, (A ⧸ J)⁺), under which f becomes presentationLimitPreAdicSpaceQuotientComap.

theorem TauCeti.PreAdicSpace.isClosedImmersion_iff {X Y : PreAdicSpace} (f : X ⟶ Y) : IsClosedImmersion f ↔ ∀ (y : ↑Y.toTopCat), ∃ (V : TopologicalSpace.Opens ↑Y.toTopCat) (_ : y ∈ V) (A : Type u) (x : CommRing A) (x_1 : TopologicalSpace A) (x_2 : IsTopologicalRing A) (x_3 : Huber.IsHuberRing A) (S : Huber.Pair A) (P : Huber.PairOfDefinition A) (hP : P.ringOfDefinition ≤ S.plus) (J : Ideal A) (_ : IsClosed ↑J) (hsheaf : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(ValuationSpectrum.spa (S.quotient J).plus)) (ValuationSpectrum.presentationLimitPresheaf (P.quotient J) (S.quotient J).plus)) (eV : Y.restrict ⋯ ≅ ValuationSpectrum.presentationLimitPreAdicSpace P S.plus ⋯ hP) (eU : X.restrict ⋯ ≅ ValuationSpectrum.presentationLimitPreAdicSpace (P.quotient J) (S.quotient J).plus ⋯ ⋯), CategoryTheory.CategoryStruct.comp (X.ofRestrict ⋯) f = CategoryTheory.CategoryStruct.comp eU.hom (CategoryTheory.CategoryStruct.comp (ValuationSpectrum.presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf) (CategoryTheory.CategoryStruct.comp eV.inv (Y.ofRestrict ⋯)))

Unfolding lemma for TauCeti.PreAdicSpace.IsClosedImmersion.

theorem TauCeti.PreAdicSpace.IsClosedImmersion.isClosedEmbedding {X Y : PreAdicSpace} {f : X ⟶ Y} (hf : IsClosedImmersion f) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)

A closed immersion is a closed embedding of the underlying topological spaces. Being a closed embedding is local on the target, and over each neighbourhood supplied by the definition the morphism is the quotient morphism, which is a closed embedding by Wedhorn's Proposition 7.38.

instance TauCeti.PreAdicSpace.IsClosedImmersion.respectsIso : CategoryTheory.MorphismProperty.RespectsIso @IsClosedImmersion

Being a closed immersion is invariant under isomorphisms of the source and of the target.

theorem TauCeti.ValuationSpectrum.isClosedImmersion_presentationLimitPreAdicSpaceQuotientComap {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)) (hJ : IsClosed ↑J) : PreAdicSpace.IsClosedImmersion (presentationLimitPreAdicSpaceQuotientComap S P hP J hsheaf)

The quotient morphism by a closed ideal is a closed immersion, witnessed over the whole of Spa(A, A⁺).

theorem TauCeti.ValuationSpectrum.isClosedImmersion_presentationLimitPreAdicSpaceComap_of_isQuotientMapping {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) {B : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [Huber.IsHuberRing B] {T : Huber.Pair B} (P' : Huber.PairOfDefinition B) (hP' : P'.ringOfDefinition ≤ T.plus) (f : S.Hom T) (hf : f.IsQuotientMapping) (hker : IsClosed ↑(RingHom.ker f.toRingHom)) (hsheafT : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa T.plus)) (presentationLimitPresheaf P' T.plus)) : PreAdicSpace.IsClosedImmersion (presentationLimitPreAdicSpaceComap f.toRingHom ⋯ ⋯ ⋯ ⋯ hP hP' hsheafT)

A quotient mapping of Huber pairs induces a closed immersion. Let f : (A, A⁺) → (B, B⁺) be a quotient mapping (an open surjection with B⁺ the integral closure of the image of A⁺) whose kernel is closed, and suppose the structure presheaf of Spa(B, B⁺) is a sheaf. Then the induced morphism Spa(B, B⁺) ⟶ Spa(A, A⁺) is a closed immersion: through the inverse of the factorisation (A ⧸ ker f, (A ⧸ ker f)⁺) → (B, B⁺), it is the quotient morphism by ker f.