The structure presheaf on a rational subset is the structure presheaf of A⟨T/s⟩ #
Let U = R(T/s) be a rational subset of X = Spa(A, A⁺), let B = A⟨T/s⟩ with plus ring
A_U⁺, and let j : Spa(B, A_U⁺) → X be the open embedding induced by the structure map
A → B. Wedhorn's Remark 8.4 identifies 𝒪_X(V) with 𝒪_U(j⁻¹(V)) for every open V ⊆ U,
compatibly with restriction; equivalently, the presheaf 𝒪_X restricted along j is 𝒪_U. This
file proves that statement for the presentation-limit presheaves: j''ᵒᵖ ⋙ 𝒪_X ≅ 𝒪_U, where j''
is the image functor on opens, when A⁺ consists of power-bounded elements and contains the ring of
definition. It is the presheaf half of Wedhorn's Remark 8.8, that j is an open immersion of
pre-adic spaces with image U; the compatibility of the stalk valuations is not treated here.
The isomorphism on arbitrary opens #
For an open W of Spa(B, A_U⁺), the component of presentationLimitPresheafLocIso at W is an
isomorphism 𝒪_X(j(W)) ≅ 𝒪_U(W) of complete separated topological rings, natural in W. On a
rational open W it is the identification presentationLimitLocIso of
TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.Localization, indexed by W through
j(W) (presentationLimitLocImageIso, presentationLimitPresheafLocIso_hom_app); on a general
W it is determined by its restrictions to the rational opens W' ⊆ W
(presentationLimitPresheafLocIso_hom_app_comp_map), since both presheaves are the limits of their
values on rational opens (presentationLimitPresheafIsPointwiseRightKanExtension). The
restricted presheaf j''ᵒᵖ ⋙ 𝒪_X is the structure presheaf of the presheafed space X restricted
along j (Mathlib's PresheafedSpace.restrict), so presentationLimitPresheafLocIso is the
isomorphism of presheafed spaces underlying the open immersion; together with the compatibility of
the stalk valuations, it makes the rational subset U an open affinoid subspace of X.
Main definitions #
TauCeti.ValuationSpectrum.presentationLimitLocImageIso: the identification𝒪_X(j(W)) ≅ 𝒪_U(W)for a rational openWofSpa(B, A_U⁺).TauCeti.ValuationSpectrum.presentationLimitPresheafLocIso: Wedhorn's Remark 8.4 for the presentation-limit presheaves,j''ᵒᵖ ⋙ 𝒪_X ≅ 𝒪_Uas presheaves onSpa(B, A_U⁺).
Main results #
TauCeti.ValuationSpectrum.presentationLimitMap_comp_presentationLimitLocImageIso_hom: the rational-level identification commutes with restriction.TauCeti.ValuationSpectrum.presentationLimitLocImageIso_hom: the rational-level identification ispresentationLimitLocIsoatj(W), up to transport alongj⁻¹(j(W)) = W.TauCeti.ValuationSpectrum.presentationLimitPresheafLocIso_hom_app_comp_mapandTauCeti.ValuationSpectrum.presentationLimitPresheafLocIso_hom_app: the presheaf isomorphism, followed by restriction to a rational open, is the rational-level identification; on a rational open it is that identification.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remarks 8.4 and 8.8.
The identification on rational opens, indexed by the opens of Spa(B, A_U⁺) #
Wedhorn's Remark 8.4 on a rational open of Spa(B, A_U⁺). For a rational open W of
Spa(B, A_U⁺), the presentation limit of Spa(A, A⁺) on the image j(W) is isomorphic to the
presentation limit of Spa(B, A_U⁺) on W. This is presentationLimitLocIso at the rational open
j(W) ⊆ R(T/s), whose pullback j⁻¹(j(W)) is W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On a rational open W of Spa(B, A_U⁺), the identification presentationLimitLocImageIso is
presentationLimitLocIso at the rational open j(W), followed by the transport along
j⁻¹(j(W)) = W.
The identification on rational opens is natural: for rational opens W' ⊆ W of
Spa(B, A_U⁺), the isomorphisms at W and W' carry the restriction map from j(W) to j(W')
over A to the restriction map from W to W' over B.
The comparison maps #
Wedhorn's Remark 8.4 as an isomorphism of presheaves #
Wedhorn's Remark 8.4 for the presentation-limit presheaves. Let U = R(T/s) be a rational
subset of X = Spa(A, A⁺), where T spans an open ideal and A⁺ consists of power-bounded
elements and contains the ring of definition, and let j : Spa(A⟨T/s⟩, A_U⁺) → X be the open
embedding induced by the structure map. The presheaf 𝒪_X restricted along j — the presheaf
W ↦ 𝒪_X(j(W)) on Spa(A⟨T/s⟩, A_U⁺), which is the structure presheaf of the restriction of the
presheafed space X along j — is isomorphic to the presentation-limit presheaf of
Spa(A⟨T/s⟩, A_U⁺). On a rational open the isomorphism is presentationLimitLocImageIso
(presentationLimitPresheafLocIso_hom_app).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presheaf isomorphism restricts to the identification on rational opens: for an open
W of Spa(A⟨T/s⟩, A_U⁺) and a rational open W' ⊆ W, the component of
presentationLimitPresheafLocIso at W followed by restriction to W' is restriction from
j(W) to j(W') followed by presentationLimitLocImageIso.
On a rational open, the presheaf isomorphism is the identification
presentationLimitLocImageIso.