Comparison maps from a containment of rational subsets #
TauCeti.Huber.existsUnique_continuous_ringHom_of_refines compares two coordinate rings when the
second presentation refines the first syntactically — s'' = s * r with every t * r a
numerator. Wedhorn's Proposition 8.2(1) asks for the comparison under the weaker, geometric
hypothesis that the rational subsets are contained in one another, and this file instantiates
Lemma 8.1 at a coordinate ring to get it.
Neither result is yet Wedhorn's in the generality he states it. Instantiating Lemma 8.1 at a
coordinate ring inherits what Lemma 8.1 asks of a target pair, and below that is two hypotheses
carried rather than derived: invertibility of the containing presentation's denominator s in
A⟨T'/s'⟩, and openness of the plus subring A_U⁺. Until both are discharged neither result may
be cited as the statement Wedhorn gives. See The hypotheses both results carry.
(1) If
U' ⊆ U, then there exists a unique continuous homomorphismσ : A⟨T/s⟩ → A⟨T'/s'⟩such thatσ ∘ ρ = ρ'.
Wedhorn's entire proof is "follows immediately from Lemma 8.1", and so is the one here: the point
of Spa is that Spa ρ' already factors through R(T'/s')
(spaComapLoc_mem_rationalSubset), so a containment R(T'/s') ⊆ R(T/s) hands the geometric
hypothesis of Lemma 8.1 over directly.
Applying that in both directions to two presentations of the same rational subset gives
presentation independence under the same hypothesis: each composite fixes the structure map
from A, hence is the identity, so the two coordinate rings are canonically isomorphic. That
is the shape TauCeti.Huber.presentationRingEquiv has been waiting for — it produces the
isomorphism given comparison maps both ways, and nothing supplies them from an equality of
rational subsets. This file supplies them, assuming that each denominator is invertible in the
other presentation's coordinate ring and that the plus subrings are open.
Main results #
TauCeti.ValuationSpectrum.existsUnique_continuous_ringHom_of_rationalSubset_subset: Wedhorn's Proposition 8.2(1) for a target in whichsis invertible and whose plus subring is open — under those two hypotheses a containment of rational subsets induces a unique continuous comparison map. Wedhorn asks for neither, so this is not yet his statement.TauCeti.ValuationSpectrum.presentationRingEquivOfEq: presentation independence under the same two hypotheses in each direction — two presentations of the same rational subset then have canonically isomorphic coordinate rings.
presentationRingEquivOfEq is a def, so it comes with the lemmas that pin down what it is
without unfolding the proof term: continuous_presentationRingEquivOfEq and
continuous_presentationRingEquivOfEq_symm, which make it an isomorphism of topological
rings, and presentationRingEquivOfEq_coe_comp_toCompletionLoc together with its symm
counterpart, which say the isomorphism and its inverse commute with the structure maps from A.
That compatibility is what determines it, so a consumer needs nothing else.
The hypotheses both results carry #
Wedhorn's Proposition 7.52(1) is no longer among them. It landed in #4552 as
TauCeti.ValuationSpectrum.mem_of_forall_vle_one and is consumed inside Lemma 8.1, so
instantiating Lemma 8.1 at a coordinate ring no longer inherits it. What each instantiation does
inherit is what 7.52(1) asks of that coordinate ring as a pair:
- invertibility of
s, the containing presentation's denominator, in the contained presentation's coordinate ring — carried rather than derived. This is step 1 of Lemma 8.1, and it is the satisfiable form of that step: an earlier revision of this file instead carriedhmax, openness of the target's maximal ideals, which byIsTateRing.isOpen_iff_eq_topno nonzero Tate ring has — so it made both results vacuous on exactly the coordinate rings §8 is about. The Lemma 8.1 variant used here,existsUnique_continuous_ringHom_of_isUnit_of_forall_comap_mem_rationalSubset, takes the unit instead ofhmax; - openness of the plus subring
A_U⁺, which is not proved anywhere on main and is the one remaining obligation of this file. It is a strictly smaller one than thehmemit replaces:hmemwas "prove Wedhorn 7.52(1) at this coordinate ring", whereas this is a single concrete topological fact about a subring the repository already constructs. Integral closedness needs no hypothesis at all —isIntegrallyClosedIn_completedPlusSubringis an instance, becausecompletedPlusSubringis defined as an integral closure.
The gap that remains is exactly the one
TauCeti.RingTheory.Huber.LocalizationTopology.Restriction already names: it records that the
refinement route "removes that dependency" precisely because a refining presentation makes the
fraction distinguished, so that isPowerBounded_divBy covers it — which a bare containment does
not. Everything else Lemma 8.1 asks of the target is discharged here from what is on main:
power-boundedness of the plus ring by completedPlusSubring_le_powerBoundedSubring, the Huber
structure by isHuberRing_completion_locTopology, and continuity by
continuous_toCompletionLoc.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 8.2(1) and Lemma 8.1.
Provenance #
Developed here; nothing is ported. AINTLIB reaches presentation independence through a height-one reduction resting on unproved bodies, which is not followed.
Wedhorn's Proposition 8.2(1), for a target in which s is invertible and whose plus
subring is open: under those two hypotheses, if the rational subset presented by T' over s'
is contained in the one presented by T over s, then exactly one continuous ring homomorphism
A⟨T/s⟩ → A⟨T'/s'⟩ is compatible with the structure maps from A.
Wedhorn imposes neither hypothesis, so this is not yet Proposition 8.2(1) in the generality he states it, and it should not be cited as that. The two are inherited from Lemma 8.1 and are discussed in the module docstring.
This is the containment form of TauCeti.Huber.existsUnique_continuous_ringHom_of_refines, which
asks instead that the second presentation refine the first syntactically. The proof is Wedhorn's:
Spa ρ' factors through R(T'/s') by spaComapLoc_mem_rationalSubset, so the containment makes
it factor through R(T/s), which is the hypothesis of Lemma 8.1.
The two hypotheses on the target are Lemma 8.1's, and neither is Proposition 7.52(1) — that is
now consumed inside Lemma 8.1 itself. The first is invertibility of s in A⟨T'/s'⟩, which is
Lemma 8.1's step 1 taken as a hypothesis rather than derived from openness of the maximal ideals;
the second is openness of the target's plus subring A_U⁺, which 7.52(1) asks of the pair and
which is not proved anywhere on main. Integral closedness of A_U⁺ needs no hypothesis:
isIntegrallyClosedIn_completedPlusSubring is an instance.
Presentation independence, when each denominator is invertible in the other coordinate ring and both plus subrings are open: under those hypotheses, two presentations of the same rational subset have canonically isomorphic coordinate rings.
As with Proposition 8.2(1) above, the unconditional statement is not proved here: the hypotheses are inherited from Lemma 8.1 and Wedhorn asks for neither.
Wedhorn's Proposition 8.2(1) applies in both directions, and
TauCeti.Huber.presentationRingEquiv turns the two comparison maps into an isomorphism — each
composite is compatible with the structure map from A, hence is the identity. Supplying those
two maps from an equality of rational subsets is the step that presentationRingEquiv's own
docstring calls "a separate step"; this takes that step.
Each direction carries the target-side hypotheses of Lemma 8.1, so there are two of each: the
primed pair for A⟨T'/s'⟩ and the unprimed pair for A⟨T/s⟩.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presentation-independence isomorphism is continuous. This is
TauCeti.Huber.continuous_presentationRingEquiv at the two comparison maps this file supplies.
The isomorphism is compatible with the structure maps from A, which is the property that
determines it.
The inverse is compatible with the structure maps the other way.
The inverse of the presentation-independence isomorphism is continuous. Together with
continuous_presentationRingEquivOfEq this says the isomorphism is one of topological rings, so
a consumer never has to unfold it to move continuously in either direction.