Evaluating A⟨X₁, …, Xₖ⟩ at the fractions of a rational localisation #
For numerators t₁, …, tₖ drawn from T, this file constructs the continuous A-algebra map
A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩, Xᵢ ↦ tᵢ/s
by instantiating the universal property of the completed restricted power-series algebra at the
trivial weight family. Membership of each tᵢ in T is what makes the fraction tᵢ/s
power-bounded, which is the hypothesis that universal property needs.
Main results #
TauCeti.Huber.PairOfDefinition.rationalEvalHom: the evaluation map, withTauCeti.Huber.PairOfDefinition.continuous_rationalEvalHom,TauCeti.Huber.PairOfDefinition.rationalEvalHom_coe_weightedC,TauCeti.Huber.PairOfDefinition.rationalEvalHom_coe_weightedXandTauCeti.Huber.PairOfDefinition.rationalEvalHom_comp_algebraMapas its interface. Uniqueness isTauCeti.Huber.existsUnique_continuous_ringHom_completion_weightedRestrictedSubring, which already characterises any continuous homomorphism by its two evaluations.TauCeti.Huber.PairOfDefinition.coe_mem_range_rationalEvalHom_of_mem_adjoin: the range of the evaluation map contains theA-subalgebra generated by the fractions, with no hypothesis on the numerators.TauCeti.Huber.PairOfDefinition.coe_mem_range_rationalEvalHomandTauCeti.Huber.PairOfDefinition.denseRange_rationalEvalHom: when the numerators together with the denominatorsgenerate the unit ideal, that subalgebra is everything, so the range already containsAₛand is therefore dense inA⟨T/s⟩.
The corresponding statements for polynomials, which need no completion theory, live one level
down in TauCeti.RingTheory.Huber.LocalizationTopology.PolynomialEvaluation and are re-exported
by this module — chiefly TauCeti.Huber.polyEvalHom and
TauCeti.Huber.PairOfDefinition.isOpenQuotientMap_polyEvalHom.
TauCeti.Huber.PairOfDefinition.rationalEvalHom_comp_completionMap, the comparison square identifying the completed polynomial evaluation withrationalEvalHomafter the map induced by the polynomial inclusion, andTauCeti.Huber.PairOfDefinition.rationalEvalHom_surjective: for numerators which together withsgenerate the unit ideal and whose fractions cover those ofT, evaluationA⟨X₁, …, Xₖ⟩ → A⟨T/s⟩is onto. Density is not what gives this; the open quotient carried up to the completions is.TauCeti.Huber.PairOfDefinition.isOpenMap_rationalEvalHomandTauCeti.Huber.PairOfDefinition.isOpenQuotientMap_rationalEvalHom: under the same hypotheses that evaluation is also open, hence an open quotient map. Over a Tate ring openness is a consequence of the surjectivity, not a further hypothesis.TauCeti.Huber.PairOfDefinition.isStrictlyTopologicallyFiniteType_toCompletionLoc: consequentlyA → A⟨T/s⟩is strictly topologically of finite type — Wedhorn's Definition 6.28 at Example 6.38. Its only hypothesis is the rational-subset condition, thatTtogether withsgenerates the unit ideal: the conclusion does not mention a family, so neither does the statement, andTis enumerated inside the proof.
What this is not #
TauCeti.Huber.PairOfDefinition.rationalEvalHom is an evaluation map, and for an arbitrary
family of numerators it is not a presentation: the family may repeat elements of T and may omit
every one of them, and then nothing exhibits A⟨T/s⟩ as generated by the chosen fractions. The
surjectivity above is not free of that — it is exactly what the two hypotheses on the family buy.
Dense range is not surjectivity, and the two are proved separately here.
TauCeti.Huber.PairOfDefinition.denseRange_rationalEvalHom gives density from the range
containing the image of Aₛ; density alone does not make a subring the whole of a complete ring.
Surjectivity additionally needs the range to be closed, which is what the open-quotient route
supplies.
Strong noetherianity of A⟨T/s⟩ is not proved here: it follows from the finite-type result
above by TauCeti.Huber.IsStrictlyTopologicallyFiniteType.isStronglyNoetherian, and that
derivation lives in
TauCeti.RingTheory.Huber.LocalizationTopology.StronglyNoetherian, beside the other
strong-noetherianity results for localisations.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 5.50 for the universal property, and Examples 6.38 and 6.39 for the intended use.
The evaluation map A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩, sending each variable Xᵢ to the fraction
tᵢ/s and each constant to its image under the structure map.
It is TauCeti.Huber.weightedEvalHomCompletion — Wedhorn's Proposition 5.50 carried to the
completion — at the trivial weight family, where the domain is A⟨X₁, …, Xₖ⟩ itself. The
numerators are given as a family t : Fin k → A landing in T rather than as T itself, so
that a caller may repeat or omit numerators. What their membership buys is power-boundedness of
each tᵢ/s in A⟨T/s⟩, which is the hypothesis the universal property needs.
Equations
- P.rationalEvalHom T s S hden t ht = TauCeti.Huber.weightedEvalHomCompletion ⋯ ⋯ ⋯
Instances For
The evaluation map is continuous.
The evaluation map sends a constant to its image under the structure map A → A⟨T/s⟩.
The evaluation map sends Xᵢ to tᵢ/s — the defining property.
The evaluation map is a map over A: composing it with the structure map of
A⟨X₁, …, Xₖ⟩ returns the structure map of A⟨T/s⟩.
This is the commutative triangle a finite-type presentation is asked for — see
TauCeti.Huber.IsStrictlyTopologicallyFiniteType, whose definition pairs an open quotient map
with exactly this compatibility — so it is the form a consumer needs, rather than the pointwise
rationalEvalHom_coe_weightedC.
An element of the A-subalgebra generated by the fractions is already in the range of the
evaluation map, after the completion map.
This is the general statement, with no hypothesis on the numerators:
TauCeti.Huber.PairOfDefinition.coe_mem_range_rationalEvalHom is the special case where that
subalgebra is everything, which is what the numerators and s generating the unit ideal buys.
Every element of Aₛ is already in the range of the evaluation map, when the numerators
together with the denominator s generate the unit ideal.
Including s among the generators is the weaker hypothesis, and the one a rational subset
supplies: dividing 1 = c · s + ∑ cₜ · t through by s makes the s term contribute the
coefficient c, which lies in A, rather than a new fraction.
This is the sharp form of the statement: not merely that the range is dense, but that it contains the image of the whole localisation.
The evaluation map has dense range when the numerators together with the denominator s
generate the unit ideal.
Density on its own does not give surjectivity: a dense subring of a complete ring need not be all of it. What closes the gap is the open-quotient route, not this theorem.
The two evaluations agree on polynomials #
On a polynomial the two evaluations agree: evaluating it in A⟨X₁, …, Xₖ⟩ by
TauCeti.Huber.PairOfDefinition.rationalEvalHom gives the image in the completion of its value
at the fractions.
On the copy of a polynomial inside A⟨X₁, …, Xₖ⟩ the completed evaluation is therefore
determined by the elementary one at the fractions: the two agree once both are carried into the
completions, the polynomial along A[X₁, …, Xₖ] → A⟨X₁, …, Xₖ⟩ and its value along
Aₛ → A⟨T/s⟩.
Surjectivity on the completions #
TauCeti.Huber.PairOfDefinition.continuous_polyEvalHom read at the packaged uniformity.
locTopology and locUniformSpace have unexposed bodies, so the two statements are not
interchangeable by unfolding; locUniformSpace_toTopologicalSpace is what relates them.
TauCeti.Huber.PairOfDefinition.isOpenMap_polyEvalHom read at the packaged uniformity.
The completed polynomial evaluation is surjective: the completion of A[X₁,…,Xₖ] maps
onto the completion of Aₛ.
The hypotheses are those under which the polynomial evaluation is an open quotient map: the
numerators generate the unit ideal with s, and their fractions cover those of T. Countable
generation of 𝓝 (0 : A) is what makes the completions metrisable, and is a hypothesis rather
than a background assumption.
The comparison square on the completions. Evaluating in A⟨X₁, …, Xₖ⟩ after the map
induced by the inclusion of the polynomials is the completion of the polynomial evaluation.
What the equality transports is surjectivity, in one direction: the left-hand side is
rationalEvalHom precomposed with the map induced by the polynomial inclusion, so if the
completed polynomial evaluation is onto then so is rationalEvalHom. That is the use made of it
in TauCeti.Huber.PairOfDefinition.rationalEvalHom_surjective.
The evaluation map A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩ is surjective, for numerators which together
with the denominator s generate the unit ideal, and whose fractions cover those of T.
Every element of A⟨T/s⟩ is thus the value of a restricted power series in the fractions
tᵢ/s. This is the surjectivity half of exhibiting A⟨T/s⟩ as a quotient of A⟨X₁, …, Xₖ⟩;
openness is the other half, and
TauCeti.Huber.PairOfDefinition.isOpenMap_rationalEvalHom supplies it.
The evaluation map A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩ is open, under the hypotheses that make it
surjective.
Over a Tate ring openness is not an independent hypothesis: it already follows from the
surjectivity and continuity of the same map. The hypotheses are therefore exactly those of
TauCeti.Huber.PairOfDefinition.rationalEvalHom_surjective, with A additionally Tate.
The evaluation map A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩ is an open quotient map: it presents A⟨T/s⟩
as a topological quotient of the restricted power series ring.
This is the form Wedhorn's Definition 6.28 asks for, and the form
TauCeti.Huber.isStrictlyTopologicallyFiniteType_iff consumes; it bundles
TauCeti.Huber.PairOfDefinition.rationalEvalHom_surjective,
TauCeti.Huber.PairOfDefinition.continuous_rationalEvalHom and
TauCeti.Huber.PairOfDefinition.isOpenMap_rationalEvalHom with no further hypotheses.
A rational localisation is strictly topologically of finite type over A, whenever the
numerators together with the denominator s generate the unit ideal.
That is the rational-subset condition itself, and it is all this asks: no auxiliary family and no choice of covering fractions.
This is Wedhorn's Definition 6.28 at Example 6.38. The presenting algebra is the trivial-weight
one, A⟨X₁, …, Xₖ⟩, which is what makes this strict topological finite type rather than the
weaker notion of Definition 6.29.
Strict finite type is the hypothesis under which strong noetherianity descends from A to
A⟨T/s⟩; TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion is that consequence.