Restriction maps for a refined presentation #
The structure presheaf of an adic space sends a rational subset R(T/s) to A⟨T/s⟩ and a
containment R(T'/s') ⊆ R(T/s) to a restriction map A⟨T/s⟩ → A⟨T'/s'⟩ (Adic Spaces,
arXiv:1910.05934v1, §8.1–§8.2). This file builds such a map whenever the target presentation
refines the source one in the elementary sense that its denominator is a multiple
s'' = s * r of the source denominator, and each t * r, for t ∈ T, is one of its numerators.
Under those hypotheses both conditions of the universal property of A⟨T/s⟩ hold outright. The
denominator condition exhibits s as a factor of an inverted element, so s becomes a unit in
A⟨T''/s''⟩ with the cofactor r/s'' as an explicit inverse; the numerator condition
identifies t/s with the distinguished fraction (t * r)/s'', which is power-bounded because
every distinguished fraction is. So the map comes from
existsUnique_continuous_ringHom_completion_locTopology, and it is the unique continuous ring
homomorphism compatible with the structure maps from A.
Refinement is the shape the intersection of two rational subsets produces: R(T₁/s₁) ∩ R(T₂/s₂)
is presented with denominator s₁ * s₂, a multiple of each. That is why this elementary notion is
enough to compare presentations, and it is what keeps a valuative criterion for integrality out
of the construction — see the Provenance section.
The statements below repeat the uniformity preamble of locUniformSpace,
isUniformAddGroup_locUniformSpace and isTopologicalRing_locUniformSpace, once per presentation,
because locTopology is deliberately not an instance; this is the same preamble the sibling module
LocalizationTopology.Presentation carries.
Main definitions #
TauCeti.Huber.PairOfDefinition.restrictionRingHom: the restriction mapA⟨T/s⟩ →+* A⟨T''/s''⟩attached to a refinement.
Main results #
TauCeti.Huber.PairOfDefinition.isUnit_toCompletionLoc_of_dvd: a factor of the denominator is a unit inA⟨T/s⟩.TauCeti.Huber.PairOfDefinition.toCompletionLoc_unit_inv_eq: its inverse is the cofactor fraction, so it can be computed with.TauCeti.Huber.PairOfDefinition.isPowerBounded_toCompletionLoc_mul_unit_inv: the fractionst/sare power-bounded in a refining presentation.TauCeti.Huber.PairOfDefinition.existsUnique_continuous_ringHom_of_refines: exactly one continuous ring homomorphismA⟨T/s⟩ → A⟨T''/s''⟩is compatible with the structure maps.TauCeti.Huber.PairOfDefinition.continuous_restrictionRingHomand…restrictionRingHom_comp_toCompletionLoc: the two properties that determine it.TauCeti.Huber.PairOfDefinition.eq_restrictionRingHom: anything with those two properties is it.TauCeti.Huber.PairOfDefinition.restrictionRingHom_coeand…restrictionRingHom_mem_completionIdealImage: on the image ofAₛit is the map of localisations, and it carries the closure of each basic neighbourhoodlocIdealImageinto the corresponding closure.TauCeti.Huber.PairOfDefinition.restrictionRingHomOfSubset_heq: changing the source and target presentations without changing their candidate rings of definition leaves the restriction map unchanged.TauCeti.Huber.PairOfDefinition.restrictionRingHom_selfand…restrictionRingHom_comp_restrictionRingHom: the identity and composition laws — a presentation refines itself with cofactor1and gives the identity map, and refinements compose with cofactorr * r₂, the restriction map of the composite being the composite of the restriction maps. Together these are the functoriality of the assignment.
What this file does not do #
It does not derive the refinement hypotheses from a containment R(T'/s') ⊆ R(T/s) of rational
subsets. Doing that means re-presenting the smaller subset as the intersection, which
rationalSubset_inter does at the level of sets, and then supplying HasDenominatorPower for that
presentation — a separate obligation, left to a consumer, since nothing here mentions Spa.
Nor is there a presheaf yet. Both functoriality laws are proved, but the indexing of the values by
rational subsets rather than by presentations, and the assignment itself, are later work: that
needs presentation-independence, whose conditional half is Presentation.presentationRingEquiv.
Provenance #
AINTLIB constructs restriction maps in projects/AdicSpaces/Adic spaces/Presheaf.lean (branch
dev/adic-spaces, commit 37bbdaeb) from a containment of rational subsets rather than from a
refinement, and the comparison is instructive. Its unit condition, isUnit_algebraMap_s_of_huber,
is proved: s lies in the radical of the ideal generated by s', hence divides a power of it,
the same factor-of-an-inverted-element argument Mathlib packages as
IsLocalization.Away.isUnit_of_dvd, which isUnit_toCompletionLoc_of_dvd below simply carries
across the completion. Its
power-boundedness condition is not proved — it is carried as the field
HasLocLiftPowerBounded.locLift_divByS_isPowerBounded of a hypothesis class, because from a bare
containment it needs a valuative criterion for integrality. Wedhorn's is Proposition 7.18, whose
own proof is the bare citation [Hu2] Lemma 3.3; he applies it in Lemma 8.1 through Proposition
7.52(1), a reformulation of 7.18(1). AINTLIB instead reduces to height one, pairing 7.18 with
Proposition 7.41, which bounds a height-one continuous valuation by 1 on A°; it calls that
combination an adic Nullstellensatz, a name Wedhorn does not use, and records it as an open
ticket. Restricting
attention to a refining presentation is what removes that dependency: the fraction in question is
then a distinguished one, and isPowerBounded_divBy already covers it.
So the construction here is unconditional where AINTLIB's rests on an assumed class.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1–§8.2 for the structure presheaf and its restriction maps, and Proposition 8.2 for the containment form. Proposition 7.18 is the criterion it needs, reached in Lemma 8.1 via Proposition 7.52(1); Proposition 7.41 belongs to AINTLIB's height-one reduction rather than to Wedhorn's route. Definition 7.14, which names rings of integral elements, is a different result and does not supply it.
- C. Birkbeck, AINTLIB, branch
dev/adic-spaces, commit37bbdaeb9, underprojects/AdicSpaces/:Adic spaces/Presheaf.lean— the restriction maps built from a containment.Adic spaces/PresheafIdentification.lean— the decomposition into Propositions 7.18 and 7.41.docs/TICKETS-axiom-clean.md— records that combination as an open ticket, under the adic Nullstellensatz name used above.
A factor of the denominator, and its inverse #
A factor of the denominator is a unit in A⟨T/s⟩. The localisation inverts s, hence
every factor of it, and the completion map carries units to units.
The inverse of that unit is the cofactor fraction. If s = a * r then the inverse of the
image of a in A⟨T/s⟩ is the image of r/s.
The hypothesis is unitness rather than divisibility, so the statement applies to whichever proof of it a caller already holds.
Multiplying the image of t by the inverse of the image of the denominator gives the
distinguished fraction t/s in A⟨T/s⟩.
t/a is power-bounded when t * r is a numerator. If the denominator factors as
s = a * r and t * r lies in T, then t/a is the distinguished fraction (t * r)/s, which is
power-bounded.
This is the remaining hypothesis of the universal property of A⟨T'/a⟩, stated for whichever
proof hu of unitness the caller will pass to it.
The restriction map #
The universal property applied to a refinement. If s'' = s * r and every t * r, for
t ∈ T, is a numerator of the second presentation, then exactly one continuous ring homomorphism
A⟨T/s⟩ → A⟨T''/s''⟩ is compatible with the structure maps from A.
Nothing is assumed beyond the refinement: the invertibility and power-boundedness the universal property asks for are consequences of it.
The restriction map of a refinement, A⟨T/s⟩ → A⟨T''/s''⟩: the unique continuous ring
homomorphism compatible with the structure maps from A.
Its two defining properties are continuous_restrictionRingHom and
restrictionRingHom_comp_toCompletionLoc, and eq_restrictionRingHom says they determine it. Those
three are the interface to use.
Equations
- P.restrictionRingHom T s S hden T'' s'' S'' hden'' r hs'' hT = Exists.choose ⋯
Instances For
The restriction map is continuous.
The restriction map is compatible with the structure maps from A. This is the equation
that characterises it, and the reason it is a map of A-algebras.
The two properties determine the restriction map. Any continuous ring homomorphism
compatible with the structure maps from A is it.
On the image of Aₛ, the restriction map is the map of localisations. The restriction map
of a refinement sends the image of x ∈ Aₛ in A⟨T/s⟩ to the image in A⟨T''/s''⟩ of the
element of A_{s''} that IsLocalization.Away.lift assigns to x. That comparison map
Aₛ → A_{s''} sends a/s to (a * r)/s'' (TauCeti.Localization.awayLift_divBy).
On the image of A this is restrictionRingHom_comp_toCompletionLoc, evaluated at a point.
The restriction map carries each basic neighbourhood of zero into the corresponding one.
For a refinement, restrictionRingHom maps completionIdealImage n of A⟨T/s⟩, the closure of
the image of locIdealImage P T s S n (by localizationUniform_idealImage), into
completionIdealImage n of A⟨T''/s''⟩, at the same index n. This is the completed form of
awayLift_mem_locIdealImage.
The identity law. A presentation refines itself with cofactor 1, and the restriction map
that gives is the identity — the unit axiom for this family of maps.
The composition law. Refinements compose — a refinement with cofactor r followed by one
with cofactor r₂ is a refinement with cofactor r * r₂ — and the restriction map of the
composite is the composite of the restriction maps. This is the cocycle axiom for this family of
maps, and with restrictionRingHom_self it is what makes the assignment functorial.
The composite refinement is derived here rather than assumed: its denominator and numerator conditions follow from the two given refinements by associativity.
Refining by enlarging the numerators #
The restriction map of a numerator enlargement. A presentation (T', s) whose numerators
contain those of (T, s) refines it with cofactor 1, so
TauCeti.Huber.PairOfDefinition.restrictionRingHom applies; this names the resulting map and
discharges its side conditions. Adjoining a single numerator, T' = insert t T, is the case
Wedhorn's Remark 7.55 chains; keeping T' abstract keeps DecidableEq A out of the API.
Equations
- P.restrictionRingHomOfSubset T s S hden T' S' hden' hTT' = P.restrictionRingHom T s S hden T' s S' hden' 1 ⋯ ⋯
Instances For
The enlargement restriction map is continuous.
The enlargement restriction map commutes with the structure maps from A.
The two properties determine the enlargement restriction map, the specialisation of
TauCeti.Huber.PairOfDefinition.eq_restrictionRingHom.
Restriction maps are independent of a simultaneous change of presentation. Suppose two
source presentations give the same candidate ring of definition inside S, and two target
presentations do likewise inside S'. Then the corresponding numerator-enlargement restriction
maps are heterogeneously equal.
The conclusion is HEq because changing a presentation changes the uniformity used to form each
completion.
The restriction map carries t/s to t/s, for every t. This is the fact the Laurent
presentation of a refinement rests on; the numerator condition t ∈ T' is not needed here, only
where power-boundedness of t/s is.
Both structure maps from A commute with restriction, so t goes to t and s goes to s. The
image of s⁻¹ is then forced: Units.map carries the unit upstairs to the unit downstairs, and a
unit determines its inverse.
The identity law. A presentation enlarges itself, and the map that gives is the identity.
The composition law. Enlargements compose, and the map of the composite is the composite of
the maps. With TauCeti.Huber.PairOfDefinition.restrictionRingHomOfSubset_self this makes the
assignment functorial along a chain of enlargements — the shape Wedhorn's Remark 7.55 produces.
A homomorphism that agrees with another after the structure maps sends t/s to t/s.
Given g out of A⟨T'/s⟩ and φ out of A⟨T/s⟩ into a common ring, agreeing after the two
structure maps from A, the distinguished fractions correspond. Both s-inverses are inverses of
the same element of the target, and inverses in a monoid are unique.
This is the transport that identifies the fraction t/s across a numerator enlargement, and it
needs nothing of the target beyond its ring structure.