Evaluating polynomials at the fractions of a rational subset #
For numerators t₁, …, tₖ drawn from T, the evaluation Xᵢ ↦ tᵢ/s of polynomials lands in
the localisation Aₛ = A⟨T/s⟩ itself, not in its completion: a polynomial in the fractions is a
finite sum, so no convergence is involved. That is what makes this map one the completion functor
can be applied to, and it is why this material sits below
TauCeti.RingTheory.Huber.LocalizationTopology.Evaluation rather than beside the completed
evaluation defined there — nothing here needs completion theory.
The three properties together present Aₛ as an open quotient of a polynomial ring. They need
different hypotheses, and the distinction matters:
- surjectivity asks the numerators together with
sto generate the unit ideal, which is what makes the fractions generateAₛoverA; - openness asks that every fraction
t/switht ∈ T— and these are what the neighbourhoods ofAₛare built from — already occurs among thetᵢ/s. It is the fractions that must be matched, not the numerators: distincttmay have the same image inAₛ; - continuity asks that each fraction
tᵢ/slie in the ring of definitionDofAₛ. That is weaker than either of the others and is implied bytᵢ ∈ T, viaTauCeti.Huber.PairOfDefinition.divBy_mem_locSubring; it is stated in this form so that a caller whose fractions lie inDfor another reason need not exhibit them as elements ofT.
None of the three implies another, so the bundled result carries all three hypotheses.
Main results #
TauCeti.Huber.polyEvalHom, withTauCeti.Huber.polyEvalHom_weightedPolynomialsEquiv_applyas its characteristic equation, andTauCeti.Huber.PairOfDefinition.isOpenQuotientMap_polyEvalHombundling the three properties above.TauCeti.Huber.PairOfDefinition.exists_aeval_eq_of_mem_locIdealImage: every element of then-th neighbourhood ofAₛis the value of a polynomial whose coefficients lie inIⁿ. This direction is what makes the evaluation open; it is an existence statement, not a characterisation.- the two directions of that characterisation in the
Fin kindexing the evaluation uses,TauCeti.Huber.PairOfDefinition.exists_polynomial_coeff_mem_idealImageandTauCeti.Huber.PairOfDefinition.aeval_mem_locIdealImage_of_coeff_mem. Openness is proved from the first and continuity from the second, and a consumer wanting either half of the correspondence between neighbourhoods and coefficient conditions should use these.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 6.28 and Example 6.38, for which this is the downstairs half. Example 6.38 is what Proposition 8.30 cites by name; the proposition's own conclusion is flatness of restriction maps, so this file is upstream of it and is not part of its statement.
The evaluation of polynomials at the fractions, Xᵢ ↦ tᵢ/s, read on the subring of
polynomials inside A⟨X₁, …, Xₖ⟩.
Unlike TauCeti.Huber.PairOfDefinition.rationalEvalHom this lands in Aₛ itself, not its
completion: a polynomial in the fractions is a finite sum, so no convergence is involved. That
is what makes it a map to which the completion functor can be applied.
Equations
- TauCeti.Huber.polyEvalHom s S t = (MvPolynomial.aeval fun (i : Fin k) => TauCeti.Localization.divBy (t i) s).comp (TauCeti.Huber.weightedPolynomialsEquiv ⋯).symm.toRingHom
Instances For
The polynomial evaluation is onto Aₛ when the numerators together with the denominator
s generate the unit ideal: its range is the A-subalgebra the fractions generate, which is
everything by TauCeti.Localization.adjoin_divBy_eq_top.
Including s among the generators is the weaker hypothesis, and the one a rational subset
supplies.
How TauCeti.Huber.polyEvalHom acts: on the copy of a polynomial inside
A⟨X⟩ it is evaluation of that polynomial at the fractions. This is the characteristic equation;
consumers should use it rather than unfolding the definition.
Every element of the n-th neighbourhood of Aₛ is the value of a polynomial with
coefficients in Iⁿ. Only this direction is proved here; the converse, that every such value
lies in the neighbourhood, is TauCeti.Huber.PairOfDefinition.aeval_mem_locIdealImage_of_coeff_mem
in the Fin k indexing. This direction is what makes the polynomial evaluation an open map.
The polynomial evaluation is open #
Every element of the n-th neighbourhood of Aₛ is the value at the fractions of a
polynomial over A whose coefficients all lie in the image of Iⁿ.
This is the Fin k-indexed form over A of
TauCeti.Huber.PairOfDefinition.exists_aeval_eq_of_mem_locIdealImage, which is indexed by T
and has coefficients in A₀.
The polynomial evaluation Xᵢ ↦ tᵢ/s is an open map, when the fractions of T all
occur among the tᵢ/s.
This asserts openness only. Surjectivity is a separate statement with a separate hypothesis —
TauCeti.Huber.polyEvalHom_surjective, which asks the numerators together with s
to generate the unit ideal.
Together with TauCeti.Huber.polyEvalHom_surjective and
TauCeti.Huber.PairOfDefinition.continuous_polyEvalHom — the three bundled as
TauCeti.Huber.PairOfDefinition.isOpenQuotientMap_polyEvalHom — this presents Aₛ as an
open quotient of a polynomial ring. That is exactly the input AddMonoidHom.surjective_completion
and AddMonoidHom.isOpenMap_completion take, so it is what carries the presentation to the
completions A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩, exhibiting A⟨T/s⟩ as strictly topologically of finite
type over A — Wedhorn's Definition 6.28 at Example 6.38 — and through it the strong
noetherianity of a rational localisation. That strong noetherianity is what Proposition 8.30
consumes; the proposition itself concludes flatness of restriction maps and is not proved here.
Openness is the half of the presentation that does not come for free. Surjectivity is a
statement about generation, whereas openness compares two topologies that were defined
independently: Aₛ carries the localisation topology, not a quotient topology transported
from the polynomials.
hTt asks that every fraction generating a neighbourhood of Aₛ already occurs among the
tᵢ/s. It is stated on fractions rather than on numerators — ↑T ⊆ Set.range t would do, and
is what a caller usually has, but the argument only ever compares images in Aₛ. It neither
implies nor is implied by the unit-ideal condition surjectivity needs.
The polynomial evaluation is continuous #
A polynomial whose coefficients all lie in the image of Iⁿ takes its value at the fractions
inside the n-th neighbourhood of Aₛ.
This is the converse direction to
TauCeti.Huber.PairOfDefinition.exists_polynomial_coeff_mem_idealImage, and it is what makes the
polynomial evaluation continuous.
The polynomial evaluation is continuous.
The polynomial evaluation is an open quotient map onto Aₛ. It is continuous, open and
surjective, which is the bundled form a consumer of the completion needs: this is what
AddMonoidHom.surjective_completion and AddMonoidHom.isOpenMap_completion take in order to
conclude the same for A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩.
The three hypotheses are independent: surjectivity needs the numerators together with s to
generate the unit ideal, openness needs the fractions of T to occur among theirs, and
continuity needs each fraction
tᵢ/s to lie in the ring of definition. A caller holding tᵢ ∈ T gets the last from
TauCeti.Huber.PairOfDefinition.divBy_mem_locSubring.