Pre-adic spaces

A pre-adic space has a presheaf of complete separated topological rings, local ring stalks, and a valuation on the residue field at every point. The valuation is a point of the valuation spectrum, so it is specified only up to equivalence. Stalks and residue fields are taken after forgetting the topology on the rings; no topology is imposed on a stalk.

This is the object-level input for morphisms of pre-adic spaces and for the sheafy full subcategory.

References

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

structure TauCeti.PreAdicSpace : Type (u + 1)

A topological space with a presheaf of complete separated topological commutative rings, local stalks, and a valuation on each stalk's residue field. Stalks are formed after forgetting the topology on sections.

• toPresheafedSpace : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat

  The underlying presheafed space of complete separated topological rings.

• isLocalRing (x : ↑↑self.toPresheafedSpace) : IsLocalRing ↑(((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).mapPresheaf.obj self.toPresheafedSpace).presheaf.stalk x)

  Every stalk of the underlying ring presheaf is local.

• valuation (x : ↑↑self.toPresheafedSpace) : ValuationSpectrum (IsLocalRing.ResidueField ↑(((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).mapPresheaf.obj self.toPresheafedSpace).presheaf.stalk x))

  The valuation of the residue field at each point.

@[reducible, inline]

abbrev TauCeti.PreAdicSpace.toTopCat (X : PreAdicSpace) : TopCat

The underlying topological space of a pre-adic space.

Equations

• X.toTopCat = ↑X.toPresheafedSpace

@[instance_reducible]

instance TauCeti.PreAdicSpace.instCoeSortType : CoeSort PreAdicSpace (Type u)

Points of a pre-adic space are points of its underlying topological space.

Equations

• TauCeti.PreAdicSpace.instCoeSortType = { coe := fun (X : TauCeti.PreAdicSpace) => ↑X.toTopCat }

@[reducible, inline]

noncomputable abbrev TauCeti.PreAdicSpace.toRingPresheafedSpace (X : PreAdicSpace) : AlgebraicGeometry.PresheafedSpace CommRingCat

The presheafed space obtained by forgetting the topology on the sections.

Equations

• X.toRingPresheafedSpace = (TauCeti.TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).mapPresheaf.obj X.toPresheafedSpace

instance TauCeti.PreAdicSpace.instIsLocalRingCarrierStalkCommRingCatPresheafToRingPresheafedSpace (X : PreAdicSpace) (x : ↑X.toTopCat) : IsLocalRing ↑(X.toRingPresheafedSpace.presheaf.stalk x)

The underlying ring presheaf has local stalks.

noncomputable def TauCeti.PreAdicSpace.stalkValuation (X : PreAdicSpace) (x : ↑X.toTopCat) : ValuationSpectrum ↑(X.toRingPresheafedSpace.presheaf.stalk x)

The valuation on the stalk at x: the residue-field valuation pulled back along the residue map. Its support is the maximal ideal of the stalk, so it is a valuation on the stalk in Wedhorn's sense, and it determines X.valuation x.

Equations

• X.stalkValuation x = TauCeti.ValuationSpectrum.comap (IsLocalRing.residue ↑(X.toRingPresheafedSpace.presheaf.stalk x)) (X.valuation x)

theorem TauCeti.PreAdicSpace.stalkValuation_def (X : PreAdicSpace) (x : ↑X.toTopCat) : X.stalkValuation x = ValuationSpectrum.comap (IsLocalRing.residue ↑(((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).mapPresheaf.obj X.toPresheafedSpace).presheaf.stalk x)) (X.valuation x)

The stalk valuation is the residue-field valuation pulled back along the residue map.

@[simp]

theorem TauCeti.PreAdicSpace.supp_stalkValuation (X : PreAdicSpace) (x : ↑X.toTopCat) : (X.stalkValuation x).supp = IsLocalRing.maximalIdeal ↑(X.toRingPresheafedSpace.presheaf.stalk x)

The support of the stalk valuation is the maximal ideal of the stalk.

theorem TauCeti.PreAdicSpace.valuation_eq_of_comap_residue_eq (X : PreAdicSpace) (x : ↑X.toTopCat) {w : ValuationSpectrum (IsLocalRing.ResidueField ↑(X.toRingPresheafedSpace.presheaf.stalk x))} (hw : ValuationSpectrum.comap (IsLocalRing.residue ↑(X.toRingPresheafedSpace.presheaf.stalk x)) w = X.stalkValuation x) : w = X.valuation x

Two points of the valuation spectrum of the residue field at x agreeing after pullback to the stalk are equal.