The adic spectrum of a rational localisation lies over the rational subset #
Roadmap Layer 3.1 attaches to a rational subset U = R(T/s) of X = Spa(A, A⁺) the complete
topological coordinate ring A_U = A⟨T/s⟩ together with its ring of integral elements A_U⁺,
and asks for a natural homeomorphism
Spa (A_U, A_U⁺) ≃ U.
This file builds the map underlying that homeomorphism and proves that it lands in U. The
structure map A → A⟨T/s⟩ is continuous and carries A⁺ into A_U⁺, so
TauCeti.ValuationSpectrum.spaComap already gives a continuous map
Spa (A_U, A_U⁺) → Spa (A, A⁺),
and the content here is that its image is contained in R(T/s), so that it corestricts to a
continuous map into the rational subset.
The two valuation-theoretic conditions cutting out R(T/s) come from the two defining features
of the localisation. The denominator s becomes a unit in A⟨T/s⟩, so no point of
Spa (A_U, A_U⁺) has it in its support; and each fraction t/s lies in A_U⁺, so every point
is sub-unit on it, which after clearing the denominator says v(t) ≤ v(s). Neither uses a Huber
hypothesis, so both are extracted first as a statement about an arbitrary continuous
homomorphism inverting s.
The reverse map — extending a point of R(T/s) to a continuous valuation on the completed
localisation — is not constructed here; it is the remaining half of the roadmap's homeomorphism.
Its pre-completion form is
TauCeti.AlgebraicGeometry.AdicSpace.Spa.Localization.Surjective, which extends a point of
R(T/s) to the uncompleted localisation Aₛ and so identifies the image of
Spa (Aₛ, Aₛ⁺) with R(T/s); passing from Aₛ to A⟨T/s⟩ is still open.
Main definitions #
TauCeti.ValuationSpectrum.spaComapLoc: the mapSpa (A_U, A_U⁺) → Spa (A, A⁺)induced by the structure mapA → A⟨T/s⟩.TauCeti.ValuationSpectrum.spaLocToRationalSubset: its corestriction toR(T/s).
Main results #
TauCeti.ValuationSpectrum.spaComapLoc_eq_comp: pullback along the structure map is pullback along the completion map followed by pullback along the localisation map.TauCeti.ValuationSpectrum.spaComapLoc_mem_rationalSubsetandTauCeti.ValuationSpectrum.range_spaComapLoc_subset: the rational localisation satisfies that criterion, soSpa (A_U, A_U⁺)lies overR(T/s).TauCeti.ValuationSpectrum.continuous_spaLocToRationalSubset: the corestriction is continuous.TauCeti.ValuationSpectrum.rationalSubset_image_toCompletionLoc_eq_spa: overA_Uthe conditions definingR(T/s)become vacuous — the rational subset presented by the images ofTandsis all ofSpa (A_U, A_U⁺).TauCeti.ValuationSpectrum.spa_completedPlusSubring_eq_empty_of_rationalSubset_eq_empty: an empty rational subset has a coordinate ring with empty adic spectrum.
Provenance #
The mathematics is Wedhorn's §8.1 description of the coordinate ring of a rational subset; the proofs here are direct and follow no existing formalisation. AINTLIB — the roadmap's designated prior formalisation of this material — was not consulted for this file: no checkout of it was available in the authoring environment. Nothing is ported.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 7.29 and §8.1.
The rational localisation #
Throughout this section S is an algebraic localisation of A away from s, carrying the
localisation topology of TauCeti.Huber.PairOfDefinition.locTopology, and A⟨T/s⟩ is its
separated completion. The three letIs that name the uniformity and its two companions are the
ones every statement about A⟨T/s⟩ carries.
The map Spa (A_U, A_U⁺) → Spa (A, A⁺) induced by the structure map A → A⟨T/s⟩: the
structure map is continuous and carries A⁺ into A_U⁺, which is all
TauCeti.ValuationSpectrum.spaComap needs.
Equations
- TauCeti.ValuationSpectrum.spaComapLoc P Aplus T s S hden = TauCeti.ValuationSpectrum.spaComap (P.toCompletionLoc T s S hden) ⋯ Aplus (P.completedPlusSubring Aplus T s S hden) ⋯
Instances For
The underlying point of spaComapLoc is the pullback along the structure map. The body is
sealed across the module boundary, so this is how a consumer computes with it.
spaComapLoc is continuous.
Pullback along the structure map factors through the uncompleted localization. The
structure map ρ : A → A⟨T/s⟩ is the localization map A → Aₛ followed by the completion map
Aₛ → A⟨T/s⟩, so spaComapLoc is the composite of the two induced maps of adic spectra.
Both factors are ordinary spaComaps with a visible plus ring, which is what makes the generic
descent results for a localization and for a map with dense range applicable; neither is
available for ρ itself.
The two continuity proofs and the two plus-ring conditions are quantified rather than fixed, so
that a consumer can supply exactly the proofs its own spaComap was built from.
Every point of Spa (A_U, A_U⁺) lies over the rational subset R(T/s) — the half of
roadmap Layer 3.1's homeomorphism Spa (A_U, A_U⁺) ≃ R(T/s) that the localisation supplies
directly.
The denominator is inverted in A⟨T/s⟩, so it is off the support of every point, and each
t/s lies in A_U⁺, so every point is sub-unit on it.
The range of spaComapLoc is contained in the rational subset R(T/s), as a subset of the
subtype ↥(Spa (A, A⁺)).
The canonical map Spa (A_U, A_U⁺) → R(T/s): spaComapLoc corestricted to the rational
subset it lands in. This is the map that roadmap Layer 3.1 asks to be a homeomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The corestriction forgets to spaComapLoc.
The canonical map into the rational subset is continuous.
In the coordinate ring of U = R(T/s), the rational subset cut out by the images of the
defining data is the whole adic spectrum.
This is the point of passing to A_U: the conditions v(t) ≤ v(s) ≠ 0 that carve U out of
Spa (A, A⁺) become vacuous over A⟨T/s⟩, because there s is a unit and each t/s is a
sub-unit. It is the degenerate case of Wedhorn's comparison of rational subsets of U with
rational subsets of X (§8.2), and it is what makes Spa (A_U, A_U⁺) a candidate for U
rather than for a proper subset of it.
The coordinate ring of an empty rational subset has empty adic spectrum. Every point of
Spa (A_U, A_U⁺) lies over a point of R(T/s), so there is none to have when R(T/s) is
empty.