The evaluation of A⟨X⟩_T as a ring homomorphism

The additive and multiplicative laws of Wedhorn's evaluation are proved in WeightedEval/Map.lean and WeightedEval/Mul.lean as statements about individual T-restricted series. On A⟨X⟩_T itself — where restrictedness is carried by membership rather than by a hypothesis — they assemble into a ring homomorphism, which is the shape Proposition 5.50 needs.

Its continuity is TauCeti.Huber.continuous_weightedEvalHom in WeightedEval/Continuous.lean. The uniqueness that makes 5.50 a universal property is TauCeti.Huber.weightedRestrictedSubring_ringHom_ext_of_continuous in WeightedRestrictedSeries/Basic.lean; WeightedEval/UniversalProperty.lean puts the two together, and its ∃! statement identifies this homomorphism as the only continuous one with these values on the generators.

Main definitions

• TauCeti.Huber.weightedEvalHom: evaluation as a ring homomorphism A⟨X⟩_T →+* B.

Main results

• TauCeti.Huber.coe_weightedEvalHom: it is TauCeti.Huber.weightedEval on the underlying series, which is how every computation about it is done.
• TauCeti.Huber.weightedEvalHom_weightedC and TauCeti.Huber.weightedEvalHom_weightedX: it sends weightedC a to φ a and weightedX i to bᵢ.

References

• Wedhorn, Adic Spaces, Proposition 5.50.

noncomputable def TauCeti.Huber.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) : ↥(weightedRestrictedSubring T hT) →+* B

Wedhorn's evaluation as a ring homomorphism A⟨X⟩_T →+* B, sending a series to the sum of its terms at b along φ.

It is a homomorphism on A⟨X⟩_T rather than on all of A[[X]]: the ring laws below hold for T-restricted series, and membership in TauCeti.Huber.weightedRestrictedSubring is what carries that restrictedness. The hypotheses are those of the summability theorem — φ continuous at zero and the weighted monomials bounded — together with IsWeightFamily T for the domain to be a ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Huber.coe_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) (f : ↥(weightedRestrictedSubring T hT)) : (weightedEvalHom hT hφ hb) f = weightedEval φ b ↑f

The homomorphism is TauCeti.Huber.weightedEval on the underlying series. The body is not exported, so this is how a consumer computes with it.

theorem TauCeti.Huber.weightedEvalHom_weightedC {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) (a : A) : (weightedEvalHom hT hφ hb) ((weightedC T hT) a) = φ a

The homomorphism sends the constant series weightedC a to φ a.

theorem TauCeti.Huber.weightedEvalHom_weightedX {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) (i : Fin k) : (weightedEvalHom hT hφ hb) (weightedX T hT i) = b i

The homomorphism sends the i-th variable weightedX i to bᵢ.