Adic spaces and open adic subspaces

An adic space is an object of 𝒱, a pre-adic space whose structure presheaf is a sheaf, that admits an open cover by affinoid adic spaces; since the restriction of a sheaf to an open subspace is a sheaf, this is the condition that the object is sheafy and locally affinoid. Their full subcategory of 𝒱^pre is Wedhorn's category (Adic), here TauCeti.AdicSpace.

This file proves that the adic-space structure passes to open subspaces. The open affinoid subspaces of a restriction X|_U are the open affinoid subspaces of X contained in U: the restriction of X|_U to an open V of U is the restriction of X to the image of V, since both are open subspaces of X with the same image (restrictRestrictIso). From this and the fact that rational subsets are open affinoid subspaces of an affinoid pre-adic space, the open affinoid subspaces of a locally affinoid object form a basis of its topology (isBasis_affinoidOpens), so the restriction of a locally affinoid object to an open is locally affinoid, and the restriction of an adic space to an open, or more generally the source of an open immersion into an adic space, is an adic space: the open adic subspaces.

The basis theorem also discharges the basis hypothesis of TauCeti.PreAdicSpace.isSheafy_of_isAdapted_of_isSheaf_affinoidOpens: a pre-adic space in Wedhorn's sense is sheafy exactly when its structure presheaf is a sheaf on its open affinoid subspaces (isPreAdic.isSheafy_iff), the mechanism of Wedhorn's Remark 8.27.

Main definitions

• TauCeti.PreAdicSpace.isAdic: the adic spaces among the objects of 𝒱^pre.
• TauCeti.AdicSpace: Wedhorn's category (Adic), the full subcategory of 𝒱^pre of adic spaces.
• TauCeti.PreAdicSpace.restrictRestrictIso: restricting a restriction is restricting to the image.

Main results

• TauCeti.PreAdicSpace.mem_affinoidOpens_restrict_iff: an open of X|_U is an open affinoid subspace exactly when its image in X is.
• TauCeti.PreAdicSpace.isBasis_affinoidOpens: the open affinoid subspaces of a locally affinoid object form a basis of its topology.
• TauCeti.PreAdicSpace.isLocallyAffinoid_restrict, TauCeti.PreAdicSpace.isSheafy_restrict, TauCeti.PreAdicSpace.isAdic_restrict: being locally affinoid, sheafy, or adic passes to restrictions to opens, and TauCeti.PreAdicSpace.isAdic_of_isOpenImmersion: to the source of an open immersion.
• TauCeti.PreAdicSpace.isPreAdic.isSheafy_iff: a pre-adic space is sheafy exactly when its structure presheaf is a sheaf on its open affinoid subspaces.
• TauCeti.ValuationSpectrum.isAdic_presentationLimitPreAdicSpace: Spa(A, A⁺) with a sheaf structure presheaf is an adic space.

References

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

Open affinoid subspaces of a restriction

noncomputable def TauCeti.PreAdicSpace.restrictRestrictIso {U : TopCat} (X : PreAdicSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑(X.restrict h).toTopCat) : (X.restrict h).restrict ⋯ ≅ X.restrict ⋯

Restricting a restriction is restricting to the image: X restricted to U and then to an open V of U is isomorphic in 𝒱^pre to X restricted to the image of V in X, both being open subspaces of X with the same image. The isomorphism is compatible with the canonical morphisms to X (restrictRestrictIso_hom_ofRestrict).

Equations

• X.restrictRestrictIso h V = TauCeti.PreAdicSpace.IsOpenImmersion.isoOfRangeEq (CategoryTheory.CategoryStruct.comp ((X.restrict h).ofRestrict ⋯) (X.ofRestrict h)) (X.ofRestrict ⋯) ⋯

@[simp]

theorem TauCeti.PreAdicSpace.restrictRestrictIso_hom_ofRestrict {U : TopCat} (X : PreAdicSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑(X.restrict h).toTopCat) : CategoryTheory.CategoryStruct.comp (X.restrictRestrictIso h V).hom (X.ofRestrict ⋯) = CategoryTheory.CategoryStruct.comp ((X.restrict h).ofRestrict ⋯) (X.ofRestrict h)

@[simp]

theorem TauCeti.PreAdicSpace.restrictRestrictIso_hom_ofRestrict_assoc {U : TopCat} (X : PreAdicSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑(X.restrict h).toTopCat) {Z : PreAdicSpace} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.restrictRestrictIso h V).hom (CategoryTheory.CategoryStruct.comp (X.ofRestrict ⋯) h✝) = CategoryTheory.CategoryStruct.comp ((X.restrict h).ofRestrict ⋯) (CategoryTheory.CategoryStruct.comp (X.ofRestrict h) h✝)

theorem TauCeti.PreAdicSpace.mem_affinoidOpens_restrict_iff {U : TopCat} (X : PreAdicSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑(X.restrict h).toTopCat) : V ∈ (X.restrict h).affinoidOpens ↔ ⋯.functor.obj V ∈ X.affinoidOpens

An open V of the restriction of X along an open embedding is an open affinoid subspace of the restriction exactly when its image in X is an open affinoid subspace of X.

Open subspaces of locally affinoid and sheafy objects

theorem TauCeti.PreAdicSpace.isBasis_affinoidOpens {X : PreAdicSpace} (hX : X.isLocallyAffinoid) : TopologicalSpace.Opens.IsBasis X.affinoidOpens

The open affinoid subspaces of a locally affinoid object form a basis of its topology. Every point lies in an open affinoid subspace U, which is isomorphic to some Spa(A, A⁺), and the open affinoid subspaces of Spa(A, A⁺) form a basis of its topology; they are carried to open affinoid subspaces of X contained in U.

theorem TauCeti.PreAdicSpace.isLocallyAffinoid_restrict {U : TopCat} {X : PreAdicSpace} {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (hX : X.isLocallyAffinoid) : (X.restrict h).isLocallyAffinoid

The restriction of a locally affinoid object of 𝒱^pre to an open is locally affinoid: the open affinoid subspaces of X contained in the image of the open cover it.

theorem TauCeti.PreAdicSpace.isSheafy_restrict {U : TopCat} {X : PreAdicSpace} {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (hX : X.isSheafy) : (X.restrict h).isSheafy

The restriction of a sheafy object of 𝒱^pre to an open is sheafy, since the restriction of a sheaf to an open subspace is a sheaf.

theorem TauCeti.PreAdicSpace.isLocallyAffinoid_of_isOpenImmersion {X Y : PreAdicSpace} (hX : X.isLocallyAffinoid) (f : Y ⟶ X) [IsOpenImmersion f] : Y.isLocallyAffinoid

The source of an open immersion into a locally affinoid object is locally affinoid.

theorem TauCeti.PreAdicSpace.isSheafy_of_isOpenImmersion {X Y : PreAdicSpace} (hX : X.isSheafy) (f : Y ⟶ X) [IsOpenImmersion f] : Y.isSheafy

The source of an open immersion into a sheafy object is sheafy.

theorem TauCeti.PreAdicSpace.isPreAdic.isSheafy_iff {X : PreAdicSpace} (hX : X.isPreAdic) : X.isSheafy ↔ CategoryTheory.Presheaf.IsSheaf ((CategoryTheory.inducedFunctor Subtype.val).restrictedTopology (Opens.grothendieckTopology ↑X.toTopCat)) ((CategoryTheory.inducedFunctor Subtype.val).op.comp X.toPresheafedSpace.presheaf)

A pre-adic space is sheafy exactly when its structure presheaf is a sheaf on its open affinoid subspaces, for the topology restricted to them: the open affinoid subspaces form a basis to which the structure presheaf is adapted. This is the mechanism of Wedhorn's Remark 8.27, which produces adic spaces from pre-adic spaces covered by sheafy affinoids.

Adic spaces

def TauCeti.PreAdicSpace.isAdic : CategoryTheory.ObjectProperty PreAdicSpace

Adic spaces (Wedhorn, Definition 8.22): the objects of 𝒱, the sheafy objects of 𝒱^pre, that admit an open cover by affinoid adic spaces. Since the restriction of a sheafy object to an open is sheafy (isSheafy_restrict), an open cover by affinoid adic spaces is the same as an open cover by open affinoid subspaces: an adic space is a sheafy locally affinoid object of 𝒱^pre. Their full subcategory of 𝒱^pre is Wedhorn's category (Adic), TauCeti.AdicSpace.

Equations

• X.isAdic = (X.isSheafy ∧ X.isLocallyAffinoid)

theorem TauCeti.PreAdicSpace.isAdic_iff {X : PreAdicSpace} : X.isAdic ↔ X.isSheafy ∧ X.isLocallyAffinoid

theorem TauCeti.PreAdicSpace.isAdic.isSheafy {X : PreAdicSpace} (hX : X.isAdic) : X.isSheafy

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

theorem TauCeti.PreAdicSpace.isAdic_le_isSheafy : isAdic ≤ isSheafy

theorem TauCeti.PreAdicSpace.isAdic_le_isLocallyAffinoid : isAdic ≤ isLocallyAffinoid

instance TauCeti.PreAdicSpace.isAdic.instIsClosedUnderIsomorphisms : isAdic.IsClosedUnderIsomorphisms

Being an adic space is invariant under isomorphism in 𝒱^pre.

theorem TauCeti.PreAdicSpace.isAdic_of_isAffinoid {X : PreAdicSpace} (hX : X.isAffinoid) (hs : X.isSheafy) : X.isAdic

A sheafy affinoid pre-adic space, an affinoid adic space, is an adic space.

theorem TauCeti.PreAdicSpace.isAdic_restrict {U : TopCat} {X : PreAdicSpace} {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (hX : X.isAdic) : (X.restrict h).isAdic

The restriction of an adic space to an open is an adic space: the open adic subspaces of an adic space are its open subsets with the restricted structure.

theorem TauCeti.PreAdicSpace.isAdic_of_isOpenImmersion {X Y : PreAdicSpace} (hX : X.isAdic) (f : Y ⟶ X) [IsOpenImmersion f] : Y.isAdic

The source of an open immersion into an adic space is an adic space.

@[reducible, inline]

abbrev TauCeti.AdicSpace : Type (u + 1)

Wedhorn's category (Adic) of adic spaces: the full subcategory of 𝒱^pre whose objects are the sheafy locally affinoid objects (PreAdicSpace.isAdic).

Equations

• TauCeti.AdicSpace = TauCeti.PreAdicSpace.isAdic.FullSubcategory

@[reducible, inline]

abbrev TauCeti.AdicSpace.toSheafyPreAdicSpace : CategoryTheory.Functor AdicSpace SheafyPreAdicSpace

Adic spaces are objects of 𝒱: the full inclusion of (Adic) into the category of sheafy pre-adic spaces.

Equations

• TauCeti.AdicSpace.toSheafyPreAdicSpace = CategoryTheory.ObjectProperty.ιOfLE TauCeti.PreAdicSpace.isAdic_le_isSheafy

theorem TauCeti.ValuationSpectrum.isSheafy_presentationLimitPreAdicSpace_iff {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) : (presentationLimitPreAdicSpace P Aplus hAplus hP).isSheafy ↔ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) (presentationLimitPresheaf P Aplus)

The presentation-limit pre-adic space of (A, A⁺) is sheafy exactly when its presentation-limit presheaf is a sheaf.

theorem TauCeti.ValuationSpectrum.isAdic_presentationLimitPreAdicSpace {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (hs : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(spa Aplus)) (presentationLimitPresheaf P Aplus)) : (presentationLimitPreAdicSpace P Aplus hAplus hP).isAdic

Spa(A, A⁺) with a sheaf structure presheaf is an adic space, an affinoid adic space: it is locally affinoid, being a pre-adic space.