Pre-adic spaces with a sheaf of topological rings

A pre-adic space has a presheaf of complete separated topological rings. The objects whose presheaf is a sheaf form a full subcategory: their morphisms retain the local and valuative conditions of pre-adic morphisms. The underlying sheafed space forgets only those extra conditions. This is the sheaf condition in Wedhorn's category of pre-adic spaces.

References

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

def TauCeti.PreAdicSpace.isSheafy : CategoryTheory.ObjectProperty PreAdicSpace

A pre-adic space is sheafy when its presheaf of complete separated topological rings satisfies the sheaf condition. The condition concerns the topological-ring-valued presheaf, not merely its underlying presheaf of sets or rings.

Equations

• X.isSheafy = X.toPresheafedSpace.presheaf.IsSheaf

instance TauCeti.PreAdicSpace.isSheafy.instIsClosedUnderIsomorphisms : isSheafy.IsClosedUnderIsomorphisms

Being sheafy is invariant under isomorphism in 𝒱^pre: an isomorphism e : X ≅ Y is a homeomorphism of the underlying spaces along which e.hom.c identifies the structure presheaf of Y with the pushforward of that of X, and the pushforward of a sheaf is a sheaf.

@[reducible, inline]

abbrev TauCeti.SheafyPreAdicSpace : Type (u + 1)

The category of pre-adic spaces with sheaf structure presheaves. It is the full subcategory of pre-adic spaces cut out by the sheaf condition.

Equations

• TauCeti.SheafyPreAdicSpace = TauCeti.PreAdicSpace.isSheafy.FullSubcategory

noncomputable def TauCeti.SheafyPreAdicSpace.toSheafedSpace (X : SheafyPreAdicSpace) : AlgebraicGeometry.SheafedSpace CompleteSeparatedTopCommRingCat

Forget the stalk locality and valuations while retaining the sheaf of complete separated topological rings.

Equations

• X.toSheafedSpace = { toPresheafedSpace := X.obj.toPresheafedSpace, IsSheaf := ⋯ }

@[simp]

theorem TauCeti.SheafyPreAdicSpace.toSheafedSpace_toPresheafedSpace (X : SheafyPreAdicSpace) : X.toSheafedSpace.toPresheafedSpace = X.obj.toPresheafedSpace

noncomputable def TauCeti.SheafyPreAdicSpace.forgetToSheafedSpace : CategoryTheory.Functor SheafyPreAdicSpace (AlgebraicGeometry.SheafedSpace CompleteSeparatedTopCommRingCat)

Forget the valuation and local-ring conditions from sheafy pre-adic spaces, retaining their structure sheaves as sheaves of complete separated topological rings.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.SheafyPreAdicSpace.forgetToSheafedSpace_obj (X : SheafyPreAdicSpace) : forgetToSheafedSpace.obj X = X.toSheafedSpace

@[simp]

theorem TauCeti.SheafyPreAdicSpace.forgetToSheafedSpace_map_hom {X Y : SheafyPreAdicSpace} (f : X ⟶ Y) : (forgetToSheafedSpace.map f).hom ≍ f.hom.toHom

instance TauCeti.SheafyPreAdicSpace.instFaithfulSheafedSpaceCompleteSeparatedTopCommRingCatForgetToSheafedSpace : forgetToSheafedSpace.Faithful

A morphism of sheafy pre-adic spaces is determined by its morphism of underlying sheafed spaces.