Comparison maps from a containment of rational subsets #
TauCeti.Huber.PairOfDefinition.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.
(1) If
U' ⊆ U, then there exists a unique continuous homomorphismσ : A⟨T/s⟩ → A⟨T'/s'⟩such thatσ ∘ ρ = ρ'.
Wedhorn's proof is "follows immediately from Lemma 8.1", and so is the one here: Spa of the
structure map A → A⟨T'/s'⟩ lands in R(T'/s') (spaComapLoc_mem_rationalSubset), so a
containment R(T'/s') ⊆ R(T/s) is exactly the geometric hypothesis of Lemma 8.1.
Applying that in both directions to two presentations of the same rational subset gives
presentation independence: 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.PairOfDefinition.presentationRingEquiv has been waiting for — it produces the
isomorphism given comparison maps both ways, and this file supplies them from an equality of
rational subsets.
The same holds in CompleteSeparatedTopCommRingCat, and there it takes the sharper form used by
the structure presheaf: presentations of one rational subset have canonically isomorphic objects,
and a refinement between two of them is an isomorphism. So the assignment
p ↦ A⟨p.num / p.den⟩ depends on the rational subset R(p) alone.
All of this assumes only that A⁺ consists of power-bounded elements, as every ring of integral
elements of A does.
Main definitions #
TauCeti.ValuationSpectrum.ringHomOfRationalSubsetSubsetandTauCeti.ValuationSpectrum.homOfRationalSubsetSubset: the comparison map of Proposition 8.2(1), respectively as a ring homomorphism and as a morphism of complete separated topological rings.TauCeti.ValuationSpectrum.completionLocObjIsoOfRationalSubsetEq: presentation independence, as an isomorphismA⟨p⟩ ≅ A⟨q⟩inCompleteSeparatedTopCommRingCat, built from the comparison morphisms of the two containments an equality of rational subsets gives.TauCeti.ValuationSpectrum.presentationRingEquivOfEq: presentation independence — two presentations of the same rational subset have canonically isomorphic coordinate rings, by the comparison maps in both directions.
Main results #
TauCeti.ValuationSpectrum.existsUnique_continuous_ringHom_of_rationalSubset_subset: Wedhorn's Proposition 8.2(1) — a containment of rational subsets induces a unique continuous comparison map compatible with the structure maps.TauCeti.ValuationSpectrum.isIso_homOfRationalSubsetSubset_of_eq: a comparison morphism between equal rational subsets is an isomorphism.TauCeti.ValuationSpectrum.restrictionHom_eq_homOfRationalSubsetSubset: the restriction morphism of a refinement is the comparison morphism of the induced containment.TauCeti.ValuationSpectrum.isIso_restrictionHom_of_rationalSubset_eq: a refinement map between two presentations of the same rational subset is an isomorphism.
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.
By the uniqueness in Proposition 8.2(1), that compatibility characterises the isomorphism among
continuous ring homomorphisms, so a consumer needs nothing else.
completionLocObjIsoOfRationalSubsetEq is a def for the same reason, and is pinned down the
same way, by completionLocObjIsoOfRationalSubsetEq_hom and
completionLocObjIsoOfRationalSubsetEq_inv.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 8.2(1), Lemma 8.1 and Proposition 7.52(2).
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). 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.
This is the containment form of
TauCeti.Huber.PairOfDefinition.existsUnique_continuous_ringHom_of_refines, which asks instead that
the second presentation refine the first syntactically. The hypothesis hAplus holds whenever
A⁺ is a ring of integral elements of A.
The comparison map of Wedhorn's Proposition 8.2(1): for a containment R(T'/s') ⊆ R(T/s)
of rational subsets, the continuous ring homomorphism A⟨T/s⟩ → A⟨T'/s'⟩ compatible with the
structure maps from A, which is unique by
existsUnique_continuous_ringHom_of_rationalSubset_subset.
The body is not exported: consumers use continuous_ringHomOfRationalSubsetSubset and
ringHomOfRationalSubsetSubset_comp_toCompletionLoc.
Equations
- TauCeti.ValuationSpectrum.ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden T' s' S' hden' hsub = Exists.choose ⋯
Instances For
The comparison map of Wedhorn's Proposition 8.2(1) is continuous.
The comparison map of Wedhorn's Proposition 8.2(1) is compatible with the structure maps
from A.
Uniqueness of the comparison map: ringHomOfRationalSubsetSubset is the only continuous
ring homomorphism A⟨T/s⟩ → A⟨T'/s'⟩ compatible with the structure maps from A.
Comparison morphisms between completed rational localizations #
The comparison morphism of a containment R(q) ⊆ R(p): Wedhorn's Proposition 8.2(1) map
A⟨p⟩ → A⟨q⟩, the unique continuous ring homomorphism compatible with the structure maps from A,
as a morphism of CompleteSeparatedTopCommRingCat.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The comparison morphism of R(p) ⊆ R(p) is the identity.
Comparison morphisms compose along a chain of containments.
Comparison morphisms compose along a chain of containments.
Comparison maps through the identification with A⟨p⟩: under
Presentation.completionLocObjCommRingCatIso, the underlying ring map of the comparison morphism of
R(q) ⊆ R(p) is the comparison ring homomorphism ringHomOfRationalSubsetSubset.
Presentation independence in CompleteSeparatedTopCommRingCat #
Presentation independence: two presentations of the same rational subset have
canonically isomorphic objects A⟨p⟩ ≅ A⟨q⟩.
Its two components are the comparison morphisms of the two containments the equality gives, so a consumer that already has one of those can use it directly.
This is the categorical counterpart of presentationRingEquivOfEq: it says the assignment
p ↦ A⟨p.num / p.den⟩ depends on the rational subset R(p) alone. The body is not exported:
consumers use completionLocObjIsoOfRationalSubsetEq_hom and
completionLocObjIsoOfRationalSubsetEq_inv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward morphism of the presentation-independence isomorphism is the comparison morphism
of the containment R(q) ⊆ R(p).
The inverse morphism of the presentation-independence isomorphism is the comparison morphism
of the containment R(p) ⊆ R(q).
A comparison morphism between equal rational subsets is an isomorphism. This is the
form to use when the comparison morphism is already in hand and only its invertibility is
wanted; completionLocObjIsoOfRationalSubsetEq is the bundled isomorphism itself.
The restriction morphism of a refinement is a comparison morphism: both are continuous
and compatible with the structure maps from A, which determines the map.
A refinement map between two presentations of the same rational subset is an
isomorphism: the restriction morphism A⟨p⟩ ⟶ A⟨q⟩ of a refinement p ≤ q is invertible as
soon as R(p) = R(q).
A refinement can only shrink the rational subset; this says that when it shrinks it by nothing,
nothing is lost on coordinate rings either. So p ↦ A⟨p.num / p.den⟩ descends, up to canonical
isomorphism, to a function of the rational subset alone.
Presentation independence: two presentations of the same rational subset have canonically isomorphic coordinate rings.
It is TauCeti.Huber.PairOfDefinition.presentationRingEquiv at the comparison maps that
existsUnique_continuous_ringHom_of_rationalSubset_subset gives for the two containments, so it
needs only the equality heq of rational subsets. The body is not exported: consumers use
presentationRingEquivOfEq_coe_comp_toCompletionLoc, continuous_presentationRingEquivOfEq and
their symm counterparts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presentation-independence isomorphism is continuous.
The presentation-independence isomorphism is compatible with the structure maps from A;
among continuous ring homomorphisms A⟨T/s⟩ → A⟨T'/s'⟩ this compatibility characterises it
(existsUnique_continuous_ringHom_of_rationalSubset_subset).
The inverse of the presentation-independence isomorphism is compatible with the structure maps
from A: the symm counterpart of presentationRingEquivOfEq_coe_comp_toCompletionLoc.
The inverse of the presentation-independence isomorphism is continuous, so together with
continuous_presentationRingEquivOfEq the isomorphism is one of topological rings.