The integral sections 𝒪_X⁺ of a pre-adic space #
Every point x of a pre-adic space X carries the stalk valuation v_x on 𝒪_{X,x}. Following
Wedhorn, the integral sections over an open U ⊆ X are
𝒪_X⁺(U) = { f ∈ 𝒪_X(U) : v_x(f_x) ≤ 1 for every x ∈ U },
where f_x is the germ of f at x. This file defines 𝒪_X⁺(U) as a subring of 𝒪_X(U) and
shows that it is functorial in the category 𝒱^pre of pre-adic spaces: restriction maps carry
𝒪_X⁺(U) into 𝒪_X⁺(V) for V ⊆ U, which packages 𝒪_X⁺ as a presheaf of commutative rings
with a monomorphism 𝒪_X⁺ ⟶ 𝒪_X, and for a morphism f : X ⟶ Y the map on sections
𝒪_Y(V) → 𝒪_X(f⁻¹V) carries 𝒪_Y⁺(V) into 𝒪_X⁺(f⁻¹V). Over an open V contained in the image
of f the preimage of 𝒪_X⁺(f⁻¹V) is exactly 𝒪_Y⁺(V); this applies to every isomorphism and
to every open immersion over its image. So the plus subrings are determined by the stalk
valuations, and a morphism of 𝒱^pre which is an isomorphism, or an open immersion, identifies
them.
For the pre-adic space Spa(A, A⁺) of a Huber pair, 𝒪_X⁺(U) is the plus subring
TauCeti.ValuationSpectrum.presentationLimitPlusSubring
(Spa/StructurePresheaf/Plus/PreAdicSpace.lean).
Main definitions #
TauCeti.PreAdicSpace.plusSubring: the subring𝒪_X⁺(U)of𝒪_X(U).TauCeti.PreAdicSpace.plusPresheaf:𝒪_X⁺as a presheaf of commutative rings onX.TauCeti.PreAdicSpace.plusPresheafι: the inclusion𝒪_X⁺ ⟶ 𝒪_X, a monomorphism.
Main results #
TauCeti.PreAdicSpace.mem_plusSubring_iff: a section lies in𝒪_X⁺(U)exactly when its germ at every point ofUis sub-unit for the stalk valuation.TauCeti.PreAdicSpace.plusSubring_le_comap: restriction preserves integral sections.TauCeti.PreAdicSpace.Hom.plusSubring_le_comap: morphisms of pre-adic spaces preserve integral sections.TauCeti.PreAdicSpace.Hom.comap_plusSubring_of_subset_range: over an open in the image of a morphism, a section is integral exactly when its pullback is.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1.
The integral sections 𝒪_X⁺(U) of a pre-adic space over an open U: the sections whose
germ at every point x ∈ U is sub-unit for the stalk valuation v_x. It is the intersection over
x ∈ U of the preimages, under the germ maps, of the valuation rings of the stalk valuations.
Instances For
Membership in 𝒪_X⁺(U): a section over U is integral exactly when its germ at every
point x ∈ U is sub-unit for the stalk valuation at x.
Restriction preserves integral sections: for opens V ⊆ U, the restriction map
𝒪_X(U) → 𝒪_X(V) carries 𝒪_X⁺(U) into 𝒪_X⁺(V).
The presheaf of integral sections #
The presheaf of integral sections 𝒪_X⁺ of a pre-adic space: the presheaf of commutative
rings whose sections over U are the subring 𝒪_X⁺(U) of 𝒪_X(U), with the restriction maps of
𝒪_X.
Instances For
The sections of 𝒪_X⁺ over U are the subring 𝒪_X⁺(U).
The restriction maps of 𝒪_X⁺ are those of 𝒪_X, restricted to the integral sections. The
equality transports account for the evaluation theorem plusPresheaf_obj.
The inclusion 𝒪_X⁺ ⟶ 𝒪_X of the integral sections into the sections.
Instances For
The inclusion 𝒪_X⁺ ⟶ 𝒪_X is, over each open U, the inclusion of the subring 𝒪_X⁺(U).
The equality transport accounts for the evaluation theorem plusPresheaf_obj.
The inclusion 𝒪_X⁺ ⟶ 𝒪_X is a monomorphism: 𝒪_X⁺ is a sub-presheaf of 𝒪_X.
Morphisms preserve integral sections: for a morphism f : X ⟶ Y of pre-adic spaces and an
open V ⊆ Y, the map on sections 𝒪_Y(V) → 𝒪_X(f⁻¹V) carries 𝒪_Y⁺(V) into 𝒪_X⁺(f⁻¹V).
Over the image of a morphism, integrality is detected after pullback: if the open V ⊆ Y
lies in the image of f : X ⟶ Y, a section of 𝒪_Y over V is integral exactly when its pullback
to f⁻¹V is. This applies to an isomorphism, and to an open immersion over an open of its
image.