The universal property of A⟨X⟩_T

Wedhorn's Proposition 5.50 is the universal property of A⟨X₁, …, Xₖ⟩_T: a ring homomorphism φ : A →+* B into a complete Hausdorff nonarchimedean ring, continuous at zero, together with values bᵢ ∈ B making each weighted variable φ(Tᵢ) · bᵢ power-bounded, extends to A⟨X⟩_T in exactly one continuous way.

The two halves are already in place and this file is their assembly. Existence is the evaluation homomorphism: weightedEvalHom is a ring map, weightedEvalHom_weightedC and weightedEvalHom_weightedX give its values on the generators, and continuous_weightedEvalHom makes it continuous. Uniqueness is weightedRestrictedSubring_ringHom_ext_of_continuous, where the density of the polynomials (Wedhorn 5.49) is what propagates agreement on the generators to the whole ring.

Both hypotheses on the variables appear, as they do throughout this cluster: the statement is given under IsWeightBounded, and Wedhorn's coordinatewise IsWeightedVarPowerBounded — which implies it, by isWeightBounded_of_isWeightedVarPowerBounded — is derived from it.

Mathlib proves the corresponding statement for the whole power-series ring: MvPowerSeries.eval₂_unique identifies a continuous map out of MvPowerSeries σ R that agrees with MvPolynomial.eval₂ on the polynomials. Neither result implies the other. That one puts the product topology on all of MvPowerSeries σ R and asks [IsLinearTopology S S] of the target — a basis of neighbourhoods of zero by ideals — with each variable topologically nilpotent. This one is about the subring A⟨X⟩_T under the topology generated by the U⟨X⟩, which is not the subspace topology of any topology Mathlib puts on MvPowerSeries; and where that one asks IsLinearTopology of the target, this asks of B's zero-neighbourhood basis only that it consist of open subgroups. (B carries completeness and T3Space besides, as it must for the sums to exist and be determined; the contrast is in the basis condition alone.) That weaker basis condition on the target is the one that matters here: a nonzero Tate ring has no proper open ideal, so IsLinearTopology would exclude the rings this construction exists to serve.

Main results

• existsUnique_continuous_ringHom_weightedRestrictedSubring: the ∃! that the phrase "universal property" names, under IsWeightBounded.
• existsUnique_continuous_ringHom_weightedRestrictedSubring_of_isWeightedVarPowerBounded: the same under IsWeightedVarPowerBounded, the coordinatewise condition Proposition 5.50 states. This is the one to cite as 5.50.

References

• Wedhorn, Adic Spaces, Proposition 5.50.

theorem TauCeti.Huber.existsUnique_continuous_ringHom_weightedRestrictedSubring {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [CompleteSpace B] [T3Space B] {φ : A →+* B} {T : Fin k → Set A} {b : Fin k → B} (hT : IsWeightFamily T) (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightBounded φ T b) : ∃! ψ : ↥(weightedRestrictedSubring T hT) →+* B, Continuous ⇑ψ ∧ (∀ (a : A), ψ ((weightedC T hT) a) = φ a) ∧ ∀ (i : Fin k), ψ (weightedX T hT i) = b i

The universal property of A⟨X⟩_T. Given φ : A →+* B continuous at zero and values b making the weighted monomials bounded, there is exactly one continuous ring homomorphism A⟨X⟩_T →+* B restricting to φ on the constants and sending each Xᵢ to bᵢ.

The witness is weightedEvalHom, so a consumer who needs to identify a homomorphism already in hand as the evaluation gets that from the uniqueness clause.

The uniqueness is among continuous homomorphisms, and that restriction is what the proof uses: agreement is forced on the polynomials, and only continuity carries it across their closure. Whether a discontinuous extension with the same values on the generators can exist is not addressed here, in keeping with weightedRestrictedSubring_ringHom_ext_of_continuous.

theorem TauCeti.Huber.existsUnique_continuous_ringHom_weightedRestrictedSubring_of_isWeightedVarPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [CompleteSpace B] [T3Space B] {φ : A →+* B} {T : Fin k → Set A} {b : Fin k → B} (hT : IsWeightFamily T) (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightedVarPowerBounded φ T b) : ∃! ψ : ↥(weightedRestrictedSubring T hT) →+* B, Continuous ⇑ψ ∧ (∀ (a : A), ψ ((weightedC T hT) a) = φ a) ∧ ∀ (i : Fin k), ψ (weightedX T hT i) = b i

Wedhorn 5.50, the universal property of A⟨X⟩_T, 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. It is the statement above composed with isWeightBounded_of_isWeightedVarPowerBounded, which is how the rest of the cluster relates its two hypotheses — compare weightedEval_mul with weightedEval_mul_of_isWeightedVarPowerBounded.