Pre-adic spaces: locally affinoid objects of 𝒱^pre

An open subset U of an object X of 𝒱^pre is an open affinoid subspace if X restricted to U is an affinoid pre-adic space. X is locally affinoid if its open affinoid subspaces cover it. Wedhorn's pre-adic spaces are the locally affinoid objects whose structure presheaf is adapted to the open affinoid subspaces: on every open V, the presheaf is the limit of its values on the open affinoid subspaces contained in V. Their full subcategory of 𝒱^pre is Wedhorn's category (PreAd), here TauCeti.WedhornPreAdicSpace.

Adaptedness is what lets the sheaf condition on an object of 𝒱^pre be checked on its open affinoid subspaces alone, once those form a basis of the topology: an object whose open affinoid subspaces form a basis, whose presheaf is adapted to them and is a sheaf on them, for the topology restricted to them, is sheafy. That the open affinoid subspaces of a locally affinoid object form a basis is not proved here, so the basis is a hypothesis of isSheafy_of_isAdapted_of_isSheaf_affinoidOpens. Applied to a pre-adic space, whose presheaf is adapted by definition, this is the mechanism behind Wedhorn's Remark 8.27, which produces adic spaces from pre-adic spaces covered by sheafy affinoids.

Conversely, a sheaf is adapted to every basis, so a sheafy object of 𝒱^pre whose open affinoid subspaces form a basis is pre-adic. This is the remark following Wedhorn's Definition 8.22 that every adic space is a pre-adic space: adic spaces are the sheafy pre-adic spaces.

Affinoid pre-adic spaces are locally affinoid, and being locally affinoid is invariant under isomorphism in 𝒱^pre, since an isomorphism carries the restriction to an open isomorphically onto the restriction to its image (TauCeti.PreAdicSpace.restrictIso).

Main definitions

• TauCeti.PreAdicSpace.affinoidOpens: the open affinoid subspaces of an object of 𝒱^pre.
• TauCeti.PreAdicSpace.isLocallyAffinoid: the locally affinoid objects of 𝒱^pre.
• TauCeti.PreAdicSpace.isPreAdic: Wedhorn's pre-adic spaces.
• TauCeti.WedhornPreAdicSpace: Wedhorn's category (PreAd), the full subcategory of 𝒱^pre of pre-adic spaces.

Main results

• TauCeti.PreAdicSpace.isLocallyAffinoid_of_isAffinoid: affinoid pre-adic spaces are locally affinoid.
• TauCeti.PreAdicSpace.isSheafy_of_isAdapted_of_isSheaf_affinoidOpens: an object of 𝒱^pre whose open affinoid subspaces form a basis and whose presheaf is adapted to them and a sheaf on them is sheafy.
• TauCeti.PreAdicSpace.isPreAdic_of_isSheafy: a sheafy object of 𝒱^pre whose open affinoid subspaces form a basis is pre-adic.
• TauCeti.PreAdicSpace.isLocallyAffinoid.instIsClosedUnderIsomorphisms, TauCeti.PreAdicSpace.isPreAdic.instIsClosedUnderIsomorphisms: being locally affinoid, and being pre-adic, are invariant under isomorphism.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Remark and Definition 8.9, Remark and Definition 8.10, Definition 8.22, and Remark 8.27.

Open affinoid subspaces and locally affinoid objects

def TauCeti.PreAdicSpace.affinoidOpens (X : PreAdicSpace) : Set (TopologicalSpace.Opens ↑X.toTopCat)

The open affinoid subspaces of an object X of 𝒱^pre: the opens U such that X restricted to U is an affinoid pre-adic space.

Equations

• X.affinoidOpens = {U : TopologicalSpace.Opens ↑X.toTopCat | (X.restrict ⋯).isAffinoid}

@[simp]

theorem TauCeti.PreAdicSpace.top_mem_affinoidOpens_iff (X : PreAdicSpace) : ⊤ ∈ X.affinoidOpens ↔ X.isAffinoid

The whole space is an open affinoid subspace exactly when X is affinoid.

@[simp]

theorem TauCeti.PreAdicSpace.map_hom_base_mem_affinoidOpens_iff {X Y : PreAdicSpace} (e : X ≅ Y) {U : TopologicalSpace.Opens ↑Y.toTopCat} : (TopologicalSpace.Opens.map e.hom.base).obj U ∈ X.affinoidOpens ↔ U ∈ Y.affinoidOpens

An open U of Y is an open affinoid subspace of Y exactly when its preimage under an isomorphism e : X ≅ Y is an open affinoid subspace of X: e carries X restricted to e⁻¹(U) isomorphically onto Y restricted to U.

def TauCeti.PreAdicSpace.isLocallyAffinoid : CategoryTheory.ObjectProperty PreAdicSpace

An object of 𝒱^pre is locally affinoid when its open affinoid subspaces cover it.

Equations

• X.isLocallyAffinoid = ∀ (x : ↑X.toTopCat), ∃ U ∈ X.affinoidOpens, x ∈ U

theorem TauCeti.PreAdicSpace.isLocallyAffinoid_iff_sSup_eq_top (X : PreAdicSpace) : X.isLocallyAffinoid ↔ sSup X.affinoidOpens = ⊤

X is locally affinoid exactly when the union of its open affinoid subspaces is X.

theorem TauCeti.PreAdicSpace.isLocallyAffinoid_of_isAffinoid {X : PreAdicSpace} (hX : X.isAffinoid) : X.isLocallyAffinoid

Affinoid pre-adic spaces are locally affinoid.

theorem TauCeti.PreAdicSpace.isLocallyAffinoid_of_isBasis_affinoidOpens {X : PreAdicSpace} (hB : TopologicalSpace.Opens.IsBasis X.affinoidOpens) : X.isLocallyAffinoid

An object of 𝒱^pre whose open affinoid subspaces form a basis is locally affinoid.

instance TauCeti.PreAdicSpace.isLocallyAffinoid.instIsClosedUnderIsomorphisms : isLocallyAffinoid.IsClosedUnderIsomorphisms

Being locally affinoid is invariant under isomorphism in 𝒱^pre.

Pre-adic spaces

def TauCeti.PreAdicSpace.isPreAdic : CategoryTheory.ObjectProperty PreAdicSpace

Wedhorn's pre-adic spaces: the locally affinoid objects of 𝒱^pre whose structure presheaf is adapted to the open affinoid subspaces, in the sense that on every open V it is the limit of its values on the open affinoid subspaces contained in V. Their full subcategory of 𝒱^pre is Wedhorn's category (PreAd), TauCeti.WedhornPreAdicSpace.

Equations

• X.isPreAdic = (X.isLocallyAffinoid ∧ X.toPresheafedSpace.presheaf.IsAdapted X.affinoidOpens)

theorem TauCeti.PreAdicSpace.isPreAdic.isLocallyAffinoid {X : PreAdicSpace} (h : X.isPreAdic) : X.isLocallyAffinoid

theorem TauCeti.PreAdicSpace.isPreAdic.isAdapted {X : PreAdicSpace} (h : X.isPreAdic) : X.toPresheafedSpace.presheaf.IsAdapted X.affinoidOpens

instance TauCeti.PreAdicSpace.isPreAdic.instIsClosedUnderIsomorphisms : isPreAdic.IsClosedUnderIsomorphisms

Being pre-adic is invariant under isomorphism in 𝒱^pre: an isomorphism e : X ≅ Y is a homeomorphism identifying the structure presheaves, and it matches the open affinoid subspaces of X and Y, so adaptedness is transported along it.

theorem TauCeti.PreAdicSpace.isSheafy_of_isAdapted_of_isSheaf_affinoidOpens {X : PreAdicSpace} (hB : TopologicalSpace.Opens.IsBasis X.affinoidOpens) (hA : X.toPresheafedSpace.presheaf.IsAdapted X.affinoidOpens) (hs : CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X.toTopCat)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp X.toPresheafedSpace.presheaf)) : X.isSheafy

The sheaf condition on the open affinoid subspaces suffices for an adapted presheaf. If the open affinoid subspaces of X form a basis and the structure presheaf is adapted to them and is a sheaf on them, for the topology restricted to them, then it is a sheaf. For a pre-adic space h : isPreAdic X, the adaptedness hypothesis is h.isAdapted; this is the mechanism of Wedhorn's Remark 8.27, which makes a pre-adic space covered by sheafy affinoids an adic space.

theorem TauCeti.PreAdicSpace.isPreAdic_of_isSheafy {X : PreAdicSpace} (hB : TopologicalSpace.Opens.IsBasis X.affinoidOpens) (hX : X.isSheafy) : X.isPreAdic

A sheafy object whose open affinoid subspaces form a basis is pre-adic. Its structure presheaf is a sheaf of complete separated topological rings, a category with all small limits, so it is adapted to the basis of open affinoid subspaces. This is the remark following Wedhorn's Definition 8.22: an adic space, being a sheafy object covered by affinoid adic spaces, is a pre-adic space.

theorem TauCeti.PreAdicSpace.isSheafy_iff_isPreAdic_and_isSheaf_affinoidOpens {X : PreAdicSpace} (hB : TopologicalSpace.Opens.IsBasis X.affinoidOpens) : X.isSheafy ↔ X.isPreAdic ∧ CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X.toTopCat)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp X.toPresheafedSpace.presheaf)

For an object of 𝒱^pre whose open affinoid subspaces form a basis, being sheafy is being pre-adic with a structure presheaf that is a sheaf on the open affinoid subspaces, for the topology restricted to them. Together with isSheafy_of_isAdapted_of_isSheaf_affinoidOpens, this is how the sheaf condition on an adic space is checked affinoid-locally.

@[reducible, inline]

abbrev TauCeti.WedhornPreAdicSpace : Type (u + 1)

Wedhorn's category (PreAd) of pre-adic spaces: the full subcategory of 𝒱^pre whose objects are the locally affinoid objects with structure presheaf adapted to their open affinoid subspaces (PreAdicSpace.isPreAdic).

Equations

• TauCeti.WedhornPreAdicSpace = TauCeti.PreAdicSpace.isPreAdic.FullSubcategory