The universal property of the completed algebra of A⟨X⟩_T #
Wedhorn's Proposition 5.50 —
existsUnique_continuous_ringHom_weightedRestrictedSubring_of_isWeightedVarPowerBounded — is the
universal property of the restricted-series ring A⟨X⟩_T itself. This file carries it across the
separated completion: a ring homomorphism φ : A →+* B into a complete Hausdorff nonarchimedean
ring, continuous at zero, together with weight-bounded values bᵢ, extends to the completion of
A⟨X⟩_T in exactly one continuous way.
Neither half is new mathematics; both compose 5.50 with a standard property of the completion.
Existence is UniformSpace.Completion.extensionHom applied to the evaluation homomorphism, which
is available exactly because the target is already assumed complete and Hausdorff — the same
hypotheses 5.50 carries, so the completed statement asks for nothing extra. Uniqueness is
completion_weightedRestrictedSubring_ringHom_ext_of_continuous, itself
UniformSpace.Completion.ringHom_ext_of_continuous — two continuous ring homomorphisms out of a
completion that agree after composing with the coercion are equal — applied to 5.50's own
uniqueness clause for the restrictions along
UniformSpace.Completion.coeRingHom.
At the trivial weight family Tᵢ = {1} the domain is the completed restricted power-series
algebra TauCeti.Huber.restrictedMvPowerSeriesCompletion k A, which the roadmap writes
A⟨X₁,…,Xₖ⟩ for an arbitrary Tate ring, so this is that algebra's universal property. It is
stated for a general weight family because nothing in the argument uses triviality.
Main definitions #
weightedEvalHomCompletion: the evaluation homomorphism of 5.50, extended to the completion.
Main results #
existsUnique_continuous_ringHom_completion_weightedRestrictedSubring: the∃!that the phrase "universal property" names, underIsWeightBounded.- existsUnique_continuous_ringHom_completion_weightedRestrictedSubring_of_isWeightedVarPowerBounded
— the same under
IsWeightedVarPowerBounded, the coordinatewise condition Proposition 5.50 states. This is the one to cite as 5.50. completion_weightedRestrictedSubring_ringHom_ext_of_continuous: the uniqueness half on its own, which asks of the target only a semiring structure and a Hausdorff topology.weightedEvalHomCompletion_coe: the value of the extension on the image ofA⟨X⟩_T. The body of the definition is not exported, so this is how a consumer computes with it.continuous_weightedEvalHomCompletion: the extension is continuous.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 5.50.
Uniqueness #
Uniqueness asks far less of the target than existence does, so it is proved first, under its own
hypotheses on B.
A continuous homomorphism out of the completion of A⟨X⟩_T is determined by its values on
the generators. Two of them agreeing on every constant series and every variable are equal.
This is weightedRestrictedSubring_ringHom_ext_of_continuous carried across the completion: that
lemma identifies the two restrictions along UniformSpace.Completion.coeRingHom, and
UniformSpace.Completion.ringHom_ext_of_continuous propagates the agreement to the completion
by density of the image of the coercion. The completeness and T3Space hypotheses that the
universal property below carries are what the evaluation homomorphism needs in order to exist;
uniqueness needs neither.
The extended evaluation homomorphism and the universal property #
The evaluation homomorphism of Proposition 5.50, extended to the completion of A⟨X⟩_T.
The extension exists because the target is complete and Hausdorff.
Equations
Instances For
The extension is the evaluation homomorphism on the image of A⟨X⟩_T. The body of
weightedEvalHomCompletion is not exported, so this is how a consumer computes with it.
The extended evaluation homomorphism is continuous: it is a UniformSpace.Completion
extension, and those are continuous by construction.
The universal property of the completion of A⟨X⟩_T, under IsWeightBounded. Given
φ : A →+* B continuous at zero and weight-bounded values b, there is exactly one continuous
ring homomorphism from the completion of A⟨X⟩_T to B restricting to φ on the constants and
sending each Xᵢ to bᵢ.
This mirrors existsUnique_continuous_ringHom_weightedRestrictedSubring, the uncompleted
statement under the same uniform hypothesis. Proposition 5.50's own hypothesis is the
coordinatewise one, so the theorem to cite as 5.50 is the _of_isWeightedVarPowerBounded form of
this one, below:
existsUnique_continuous_ringHom_completion_weightedRestrictedSubring_of_isWeightedVarPowerBounded.
As in the uncompleted statement, uniqueness is among continuous homomorphisms, and continuity is
used at both steps of the argument: 5.50 pins ψ down on the image of A⟨X⟩_T from its values on
the constants and the variables, by density of the polynomials, and the density of that image in
the completion carries the agreement the rest of the way. Whether a discontinuous homomorphism
with the same values can exist is not addressed here.
Wedhorn 5.50 for the completed algebra, under the hypothesis Proposition 5.50 itself
carries: each weighted variable φ(Tᵢ) · bᵢ power-bounded as a set, one index at a time.
This is the theorem to cite as 5.50 for the completion. It is the statement above composed with
isWeightBounded_of_isWeightedVarPowerBounded, exactly as
existsUnique_continuous_ringHom_weightedRestrictedSubring_of_isWeightedVarPowerBounded relates
to its own uniform form.