The evaluation of A⟨X⟩_T is continuous

WeightedEval/Hom.lean packages Wedhorn's evaluation as a ring homomorphism A⟨X⟩_T →+* B. This file proves it continuous for the topology of A⟨X⟩_T, which is the last property Proposition 5.50 asks of the extension apart from its uniqueness.

The argument is the one that made the terms summable, run at a fixed series rather than along the cofinite filter, and it shares its estimate: a basic neighbourhood U⟨X⟩ of zero bounds every coefficient of f by Tν · U, so TauCeti.Huber.weightedEvalTerm_mem_of_mem_weightMul — applied at every ν rather than at cofinitely many — puts every term of the evaluation in a prescribed open subgroup G of B. The partial sums then lie in G because it is a subgroup, and the sum lies in G because an open subgroup is closed.

Main results

• TauCeti.Huber.continuous_weightedEvalHom: the evaluation homomorphism is continuous.

References

• Wedhorn, Adic Spaces, Proposition 5.50.

theorem TauCeti.Huber.continuous_weightedEvalHom {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) : Continuous ⇑(weightedEvalHom hT hφ hb)

The evaluation homomorphism A⟨X⟩_T →+* B is continuous, under the hypotheses that make it exist: φ continuous at zero and the weighted monomials φ(Tν) · bν bounded.

With weightedEvalHom_weightedC and weightedEvalHom_weightedX, this gives every property Proposition 5.50 asks of the extension except the uniqueness, which is TauCeti.Huber.weightedRestrictedSubring_ringHom_ext_of_continuous; WeightedEval/UniversalProperty.lean assembles the two into 5.50.