The adic spectrum of a rational localisation covers the rational subset #
For a rational subset R(T/s) of Spa(A, A⁺), this file shows that the continuous map
Spa (Aₛ, Aₛ⁺) → Spa (A, A⁺)
induced by the structure map A → Aₛ has image exactly R(T/s), where Aₛ carries Wedhorn's
localisation topology A(T/s) and Aₛ⁺ is the integral closure of A⁺[t₁/s, …, tₙ/s] in it —
the plus ring that
TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_integralClosure_adjoin_plus makes a ring
of integral elements of Aₛ.
The content is the inclusion ⊇: a point of R(T/s) inverts s and makes each t/s sub-unit,
so its canonical valuation extends to Aₛ, and Localization.Valuation shows the extension is
continuous and sub-unit on Aₛ⁺. The inclusion ⊆ is comap_mem_rationalSubset applied to the
structure map.
Main results #
TauCeti.ValuationSpectrum.exists_mem_spa_comap_algebraMap_eq: every point ofR(T/s)is the pullback of a point ofSpa (Aₛ, Aₛ⁺).TauCeti.ValuationSpectrum.image_comap_algebraMap_spa_subset_rationalSubset: pullback sends every point ofSpa (Aₛ, Aₛ⁺)intoR(T/s).TauCeti.ValuationSpectrum.image_comap_algebraMap_spa_eq_rationalSubset: the image ofSpa (Aₛ, Aₛ⁺)inSpa (A, A⁺)isR(T/s).
Scope: the uncompleted localisation #
Every statement below is about Aₛ carrying locTopology, not the completed localisation
A⟨T/s⟩.
The hypothesis P.ringOfDefinition ≤ A⁺ #
Both results fix a pair of definition P = (A₀, I) of A with A₀ ⊆ A⁺. The choice of pair of
definition is free — locTopology takes it as an argument — and such a P always exists, because
a ring of integral elements is open and
TauCeti.Huber.PairOfDefinition.exists_pairOfDefinition_ringOfDefinition_le produces a ring of
definition inside any open subring. The module docstring of
TauCeti.RingTheory.Huber.LocalizationTopology.Valuation explains why the hypothesis cannot be
dropped: without it the extension need not be ≤ 1 on A₀[T/s], and the neighbourhoods of zero
in Aₛ are modules over that ring.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.29 for rational subsets, Proposition and Definition 5.51 for the localisation topology, and §8.1 for the coordinate ring of a rational subset.
Provenance #
Assembled from this repository's LocalizationTopology API and the valuation-extension results of
TauCeti.RingTheory.Huber.LocalizationTopology.Valuation; nothing is ported. As in
Localization.Basic, AINTLIB was not consulted — no checkout of it was available in the
authoring environment.
At a point of a rational subset the denominator is off the support, read on the canonical
valuation rather than on the valuative relation. This is the third conjunct of
mem_rationalSubset_iff in the form the extension results consume, Valuation.extendToLocalization
being stated for valuations.
The canonical valuation of a point in R(T/s) extends continuously to the algebraic
localisation with locTopology, provided the ring of definition lies in Aplus.
Every point of R(T/s) is the pullback of a point of the adic spectrum of the rational
localisation. The canonical valuation of the point is continuous, dominates every numerator by
the denominator, and is ≤ 1 on A⁺; extending it along A → Aₛ therefore gives a continuous
valuation on Aₛ that is ≤ 1 on the integral closure of A⁺[T/s], and restricting it back
along the structure map returns the point.
Here Aₛ carries locTopology, not the topology of the completion.
Pullback from the adic spectrum of the rational localisation lands in R(T/s). The structure
map inverts s and sends each t/s into the plus ring of the localisation.
The image of the adic spectrum of the rational localisation is exactly R(T/s). The
inclusion ⊆ is image_comap_algebraMap_spa_subset_rationalSubset; the inclusion ⊇ is
exists_mem_spa_comap_algebraMap_eq.