The map induced on a quotient of A⟨X⟩_T #
Wedhorn's Example 6.38(a) presents a rational localisation A⟨T/s⟩ as a quotient C ⧸ 𝔞 of a
ring of restricted power series, and one of the two maps that identify them goes out of that
quotient. This file supplies it: an evaluation A⟨X⟩_T →+* B that kills an ideal 𝔞 factors
through A⟨X⟩_T ⧸ 𝔞, and the factorisation is again continuous.
The same factorisation exists one level up, for morphisms of Huber pairs
(TauCeti.Huber.Pair.Hom.quotientLift). The two differ in what the objects carry: a Huber pair
comes with a ring of integral elements and its morphisms must preserve it, whereas Wedhorn's
Proposition 5.50 — the universal property being transported here — speaks about ring
homomorphisms of topological rings and asks for no such structure. Use the pair-level version when
the source and target are Huber pairs, and this one otherwise.
What is not assumed, and why it is worth saying #
𝔞 is not assumed closed. Closedness of 𝔞 is what makes C ⧸ 𝔞 separated
(Ideal.Quotient.instT1Space), and Example 6.38 does need it — but for the other direction,
where C ⧸ 𝔞 is the complete Hausdorff nonarchimedean target of the universal property of
A⟨T/s⟩, alongside Ideal.Quotient.instNonarchimedeanRing. For a map out of C ⧸ 𝔞 none of
that is used: the quotient topology exists for any ideal, and it is all the argument needs. The
hypothesis is therefore omitted rather than carried, and a consumer that also needs C ⧸ 𝔞 to be
a well-behaved target should assume closedness alongside.
Main definitions #
TauCeti.Huber.weightedEvalQuotientHom: the induced ring homomorphismA⟨X⟩_T ⧸ 𝔞 →+* B.
Main results #
TauCeti.Huber.weightedEvalQuotientHom_comp_mk: it is a factorisation ofTauCeti.Huber.weightedEvalHomthrough the quotient map. This is the property that characterises the induced map, and it determines its values on the images of the constants and of the variables.TauCeti.Huber.continuous_weightedEvalQuotientHom: the induced map is continuous.TauCeti.Huber.existsUnique_continuous_ringHom_quotient_weightedRestrictedSubring: it is the only continuous homomorphism out ofA⟨X⟩_T ⧸ 𝔞with the prescribed values on the images of the constants and the variables — the universal property ofA⟨X⟩_Tread on the quotient.
References #
- Wedhorn, Adic Spaces, Example 6.38(a), and Proposition 5.50 for the universal property this factors.
The map induced on A⟨X⟩_T ⧸ 𝔞 by an evaluation that kills 𝔞. Given the data of the
universal property — φ continuous at zero and values b making the weighted monomials bounded
— together with an ideal 𝔞 contained in the kernel of the resulting evaluation, this is the
homomorphism A⟨X⟩_T ⧸ 𝔞 →+* B through which that evaluation factors.
Its continuity is TauCeti.Huber.continuous_weightedEvalQuotientHom.
Equations
- TauCeti.Huber.weightedEvalQuotientHom hT hφ hb h𝔞 = Ideal.Quotient.lift 𝔞 (TauCeti.Huber.weightedEvalHom hT hφ hb) ⋯
Instances For
The induced map computes the evaluation on a representative.
The defining factorisation: composing the induced map with the quotient map returns the
evaluation. With Ideal.Quotient.ringHom_ext this is what pins the induced map down.
The induced map is continuous.
The universal property of A⟨X⟩_T, read on the quotient. When 𝔞 lies in the kernel of
the evaluation, there is exactly one continuous ring homomorphism A⟨X⟩_T ⧸ 𝔞 →+* B taking the
prescribed values on the images of the constants and of the variables.
The witness is TauCeti.Huber.weightedEvalQuotientHom, so a consumer holding a continuous
homomorphism with those values gets to identify it as that map.
The universal property of A⟨X⟩_T on the quotient, under Wedhorn's own hypothesis. The
coordinatewise condition IsWeightedVarPowerBounded — each weighted variable power-bounded as a
set, one index at a time — is the form Proposition 5.50 states, and this is the version to cite as
5.50 on the quotient.