Affinoid pre-adic spaces

An affinoid pre-adic space is an object of 𝒱^pre isomorphic, in that category, to the adic spectrum of a Huber pair with its presentation-limit structure presheaf and point valuations. The isomorphism therefore remembers the complete topological rings on every open and the residue-field valuations, not only a homeomorphism of the underlying spaces.

The predicate is independent of the chosen representative by construction and is registered as closed under isomorphisms. Canonical presentation-limit spectra are affinoid, and every affinoid pre-adic space has a spectral underlying topological space. The latter is the quasi-compactness input used to distinguish genuinely non-affinoid spaces later.

The further condition defining a pre-adic space in Wedhorn's sense is local: it asks for an affinoid open cover and for the structure presheaf to be adapted to the set of all affinoid open subspaces. That condition is not imposed here.

Main definitions

• TauCeti.PreAdicSpace.isAffinoidModel: the object property of being a presentation-limit pre-adic space of a Huber pair.
• TauCeti.PreAdicSpace.isAffinoid: the isomorphism closure of isAffinoidModel, the isomorphism-invariant object property of being an affinoid pre-adic space.
• TauCeti.AffinoidPreAdicSpace: the full subcategory of affinoid pre-adic spaces.
• TauCeti.AffinoidPreAdicSpace.ofPresentation: the canonical affinoid object attached to a Huber pair, a compatible pair of definition, and its presentation-limit presheaf.

References

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

def TauCeti.PreAdicSpace.isAffinoidModel : CategoryTheory.ObjectProperty PreAdicSpace

The presentation-limit pre-adic spaces of Huber pairs, as an object property of 𝒱^pre. The affinoid pre-adic spaces are the objects isomorphic to one of these.

Equations

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

@[reducible, inline]

abbrev TauCeti.PreAdicSpace.isAffinoid : CategoryTheory.ObjectProperty PreAdicSpace

An object of 𝒱^pre is affinoid when it is isomorphic to the presentation-limit pre-adic space of a Huber pair. The pair of definition is required to lie in the plus ring, as in the construction of presentationLimitPreAdicSpace.

The existentially quantified type carries all of its topological-ring and Huber instances. This keeps the property at the natural universe of PreAdicSpace and does not choose a global plus ring or pair of definition. The definition is reducible so that the instances of ObjectProperty.isoClosure, in particular closure under isomorphisms, apply to isAffinoid.

Equations

• TauCeti.PreAdicSpace.isAffinoid = TauCeti.PreAdicSpace.isAffinoidModel.isoClosure

theorem TauCeti.PreAdicSpace.isAffinoid_iff (X : PreAdicSpace) : X.isAffinoid ↔ ∃ (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), Nonempty (X ≅ ValuationSpectrum.presentationLimitPreAdicSpace P S.plus ⋯ hP)

Characterisation of an affinoid pre-adic space by an affinoid presentation and an isomorphism in 𝒱^pre.

theorem TauCeti.PreAdicSpace.isAffinoid_presentationLimitPreAdicSpace {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) : (ValuationSpectrum.presentationLimitPreAdicSpace P S.plus ⋯ hP).isAffinoid

The presentation-limit pre-adic space of a Huber pair is affinoid.

theorem TauCeti.PreAdicSpace.spectralSpace_of_isAffinoid {X : PreAdicSpace} (hX : X.isAffinoid) : SpectralSpace ↑X.toTopCat

The underlying topological space of an affinoid pre-adic space is spectral.

@[reducible, inline]

abbrev TauCeti.AffinoidPreAdicSpace : Type (u + 1)

The full subcategory of affinoid pre-adic spaces.

Equations

• TauCeti.AffinoidPreAdicSpace = TauCeti.PreAdicSpace.isAffinoid.FullSubcategory

noncomputable def TauCeti.AffinoidPreAdicSpace.ofPresentation {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) : AffinoidPreAdicSpace

The canonical affinoid pre-adic space associated to a Huber pair and a compatible pair of definition.

Equations

• TauCeti.AffinoidPreAdicSpace.ofPresentation S P hP = { obj := TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace P S.plus ⋯ hP, property := ⋯ }

@[simp]

theorem TauCeti.AffinoidPreAdicSpace.ofPresentation_obj {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) : (ofPresentation S P hP).obj = ValuationSpectrum.presentationLimitPreAdicSpace P S.plus ⋯ hP

The underlying pre-adic space of the canonical affinoid object is the presentation-limit adic spectrum.

instance TauCeti.AffinoidPreAdicSpace.instSpectralSpaceCarrierToTopCatObjPreAdicSpaceIsAffinoid (X : AffinoidPreAdicSpace) : SpectralSpace ↑X.obj.toTopCat

Affinoid pre-adic spaces have spectral underlying topological spaces.