The evaluation of a weighted restricted series is multiplicative

TauCeti/RingTheory/Huber/WeightedEval/Map.lean gives Wedhorn's evaluation its additive API and its values on constants and variables. This file adds multiplicativity, weightedEval (f * g) = weightedEval f * weightedEval g.

That is the remaining algebraic ingredient of Proposition 5.50, but not by itself the universal property, since it speaks about individual series. The packaging as a ring homomorphism out of A⟨X⟩_T is TauCeti.Huber.weightedEvalHom in WeightedEval/Hom.lean, which consumes weightedEval_mul below, and its continuity is TauCeti.Huber.continuous_weightedEvalHom in WeightedEval/Continuous.lean. The uniqueness of the extension, which is what makes 5.50 universal, is TauCeti.Huber.weightedRestrictedSubring_ringHom_ext_of_continuous in WeightedRestrictedSeries/Basic.lean, and WeightedEval/UniversalProperty.lean states 5.50 itself.

The argument is the Cauchy product, and Mathlib supplies it: Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal turns a product of sums into a sum over antidiagonals, and MvPowerSeries.coeff_mul says the antidiagonal sum at ν is the ν-th coefficient of f * g.

Main results

• TauCeti.Huber.weightedEval_mul_of_summable: multiplicativity from summability alone, which is all the proof uses.
• TauCeti.Huber.weightedEval_mul, with TauCeti.Huber.weightedEval_mul_of_isWeightedVarPowerBounded and TauCeti.Huber.weightedEval_mul_of_forall_isPowerBounded: the same for T-restricted series, under each of the three hypotheses that produce summability.

References

• Wedhorn, Adic Spaces, Proposition 5.50.

theorem TauCeti.Huber.weightedEval_mul_of_summable {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] [T3Space B] [IsTopologicalRing B] {φ : A →+* B} {b : Fin k → B} {f g : MvPowerSeries (Fin k) A} (hf : Summable (weightedEvalTerm φ b f)) (hg : Summable (weightedEvalTerm φ b g)) (hfg : Summable fun (p : (Fin k →₀ ℕ) × (Fin k →₀ ℕ)) => weightedEvalTerm φ b f p.1 * weightedEvalTerm φ b g p.2) : weightedEval φ b (f * g) = weightedEval φ b f * weightedEval φ b g

The evaluation is multiplicative, at the level where that is true: three summable families. Nothing topological about A, no weights and no restrictedness — those exist only to produce summability, and the results below are this one composed with ways of producing it.

The third hypothesis, summability over pairs, is what the Cauchy product needs and does not follow from the other two in general; in a nonarchimedean target it does, which is how TauCeti.Huber.weightedEval_mul discharges it.

theorem TauCeti.Huber.weightedEval_mul {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [CompleteSpace B] [T3Space B] {φ : A →+* B} {T : Fin k → Set A} {b : Fin k → B} (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightBounded φ T b) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (hg : IsWeightedRestricted T g) : weightedEval φ b (f * g) = weightedEval φ b f * weightedEval φ b g

The evaluation is multiplicative on T-restricted series. This is TauCeti.Huber.weightedEval_mul_of_summable with all three summabilities supplied: the factors by TauCeti.Huber.summable_weightedEvalTerm, the pairs by HasSum.mul_of_nonarchimedean.

Only f and g need be T-restricted. Restrictedness of f * g is not a hypothesis and no weight-family condition appears: the Cauchy product produces the terms of the product and their sum whether or not the product is separately known to be restricted.

theorem TauCeti.Huber.weightedEval_mul_of_isWeightedVarPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [CompleteSpace B] [T3Space B] {φ : A →+* B} {T : Fin k → Set A} {b : Fin k → B} (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightedVarPowerBounded φ T b) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (hg : IsWeightedRestricted T g) : weightedEval φ b (f * g) = weightedEval φ b f * weightedEval φ b g

TauCeti.Huber.weightedEval_mul under Wedhorn's coordinatewise hypothesis.

theorem TauCeti.Huber.weightedEval_mul_of_forall_isPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanRing B] [CompleteSpace B] [T3Space B] {φ : A →+* B} {b : Fin k → B} (hφ : ContinuousAt (⇑φ) 0) (hb : ∀ (i : Fin k), IsPowerBounded (b i)) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted (fun (x : Fin k) => {1}) f) (hg : IsWeightedRestricted (fun (x : Fin k) => {1}) g) : weightedEval φ b (f * g) = weightedEval φ b f * weightedEval φ b g

TauCeti.Huber.weightedEval_mul at the one-weight family, where the hypothesis is that each variable is power-bounded.