The plus presheaf 𝒪_X⁺ of the presentation-limit presheaf #
Let X = Spa(A,A⁺) and let 𝒪_X be the presentation-limit structure presheaf, read as a presheaf
of commutative rings. Every point x ∈ X carries the stalk valuation v_x on 𝒪_{X,x}, and
Wedhorn defines the plus presheaf by
𝒪_X⁺(V) = { f ∈ 𝒪_X(V) : v_x(f_x) ≤ 1 for every x ∈ V },
where f_x is the germ of f at x. This file defines 𝒪_X⁺(V) as a subring of 𝒪_X(V),
shows that the restriction maps of 𝒪_X carry 𝒪_X⁺(V) into 𝒪_X⁺(W) for W ⊆ V, and packages
the result as a presheaf of commutative rings 𝒪_X⁺ with a monomorphism 𝒪_X⁺ ⟶ 𝒪_X.
On a rational open U = R(T/s) the sections 𝒪_X(U) are the coordinate ring A⟨T/s⟩, and the
main result identifies 𝒪_X⁺(U) with its plus ring A_U⁺ = completedPlusSubring: this is the
second component of Wedhorn's Proposition 8.16. The identification is the sub-unit description of
A_U⁺ from Spa/Localization/CompletedPlus.lean read through the stalk valuations, which restrict
to the points of A⟨T/s⟩ determined by the points of U.
The hypotheses are those of the stalk valuation: A⁺ consists of power-bounded elements and
contains the ring of definition of the chosen pair of definition.
Main definitions #
TauCeti.ValuationSpectrum.presentationLimitPlusSubring:𝒪_X⁺(V), a subring of𝒪_X(V).TauCeti.ValuationSpectrum.presentationLimitPlusPresheaf:𝒪_X⁺as a presheaf of commutative rings onSpa(A,A⁺).TauCeti.ValuationSpectrum.presentationLimitPlusPresheafι: the inclusion𝒪_X⁺ ⟶ 𝒪_X, a monomorphism.
Main results #
TauCeti.ValuationSpectrum.mem_presentationLimitPlusSubring_iff: a section lies in𝒪_X⁺(V)exactly when its germ at every point ofVis sub-unit for the stalk valuation.TauCeti.ValuationSpectrum.presentationLimitPlusSubring_le_comap: restriction carries𝒪_X⁺(V)into𝒪_X⁺(W).TauCeti.ValuationSpectrum.comap_presentationLimitPlusSubring_spaBasicOpenandTauCeti.ValuationSpectrum.map_completedPlusSubring_eq_presentationLimitPlusSubring: on a rational openR(T/s), the subring𝒪_X⁺(R(T/s))corresponds toA_U⁺ ⊆ A⟨T/s⟩under the identification𝒪_X(R(T/s)) ≅ A⟨T/s⟩.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1 and Proposition 8.16.
The plus subring of the sections over an open #
𝒪_X⁺(V), the plus subring of the sections of the presentation-limit presheaf over an
open V ⊆ Spa(A,A⁺): the sections whose germ at every point x ∈ V is sub-unit for the stalk
valuation v_x. It is the intersection over x ∈ V of the preimages, under the germ maps, of the
valuation rings of the stalk valuations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in 𝒪_X⁺(V): a section over V lies in the plus subring exactly when its germ
at every point x ∈ V is sub-unit for the stalk valuation at x.
Restriction preserves the plus subrings: the restriction map of the presentation-limit
presheaf along i : V ⟶ W in (Opens X)ᵒᵖ, that is along W ⊆ V, carries 𝒪_X⁺(V) into
𝒪_X⁺(W).
The plus presheaf #
The plus presheaf 𝒪_X⁺ of X = Spa(A,A⁺): the presheaf of commutative rings whose
sections over V are the plus subring 𝒪_X⁺(V) of the sections of the presentation-limit
presheaf, with the restriction maps of that presheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sections of 𝒪_X⁺ over V are the plus subring 𝒪_X⁺(V).
The restriction maps of 𝒪_X⁺ are those of the presentation-limit presheaf, restricted to
the plus subrings. The equality transports account for the sealed evaluation theorem
presentationLimitPlusPresheaf_obj.
The inclusion 𝒪_X⁺ ⟶ 𝒪_X of the plus presheaf into the presentation-limit presheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion 𝒪_X⁺ ⟶ 𝒪_X is, over each open V, the inclusion of the subring 𝒪_X⁺(V).
The equality transport accounts for the sealed evaluation theorem
presentationLimitPlusPresheaf_obj.
The inclusion 𝒪_X⁺ ⟶ 𝒪_X is a monomorphism: 𝒪_X⁺ is a sub-presheaf of 𝒪_X.
The plus subring of a rational open is A_U⁺ #
𝒪_X⁺(R(T/s)) = A_U⁺ (Wedhorn, Proposition 8.16, second component): under the
identification A⟨T/s⟩ ≅ 𝒪_X(R(T/s)) of the coordinate ring of an admissible presentation with the
sections of the presentation-limit presheaf over its rational open, the plus subring
𝒪_X⁺(R(T/s)) pulls back to the plus ring A_U⁺ of A⟨T/s⟩.
𝒪_X⁺(R(T/s)) = A_U⁺ (Wedhorn, Proposition 8.16, second component), as the image of
A_U⁺ under the identification A⟨T/s⟩ ≅ 𝒪_X(R(T/s)).