Documentation

Mathlib.RingTheory.MvPowerSeries.Evaluation

Evaluation of multivariate power series #

Let σ, R, S be types, with CommRing R, CommRing S. One assumes that IsTopologicalRing R and IsUniformAddGroup R, and that S is a complete and separated topological R-algebra, with IsLinearTopology S S, which means there is a basis of neighborhoods of 0 consisting of ideals.

Given φ : R →+* S, a : σ → S, and f : MvPowerSeries σ R, MvPowerSeries.eval₂ f φ a is the evaluation of the multivariate power series f at a. It f is (the coercion of) a polynomial, it coincides with the evaluation of that polynomial. Otherwise, it is defined by density from polynomials; its values are irrelevant unless φ is continuous and a satisfies two conditions bundled in MvPowerSeries.HasEval a :

for all s : σ, a s is topologically nilpotent, meaning that (a s) ^ n tends to 0 when n tends to infinity
when a s tends to zero for the filter of cofinite subsets of σ.

Under Continuous φ and HasEval a, the following lemmas furnish the properties of evaluation:

MvPowerSeries.eval₂Hom: the evaluation of multivariate power series, as a ring morphism,
MvPowerSeries.aeval: the evaluation map as an algebra morphism
MvPowerSeries.uniformContinuous_eval₂: uniform continuity of the evaluation
MvPowerSeries.continuous_eval₂: continuity of the evaluation
MvPowerSeries.eval₂_eq_tsum: the evaluation is given by the sum of its monomials, evaluated.

structure MvPowerSeries.HasEval {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] (a : σ → S) :

Families at which power series can be consistently evaluated

hpow (s : σ) : IsTopologicallyNilpotent (a s)
tendsto_zero : Filter.Tendsto a Filter.cofinite (nhds 0)

Instances For

theorem MvPowerSeries.hasEval_def {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] (a : σ → S) :

HasEval a ↔ (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧ Filter.Tendsto a Filter.cofinite (nhds 0)

theorem MvPowerSeries.HasEval.mono {σ : Type u_1} {S : Type u_4} [CommRing S] {a : σ → S} {t u : TopologicalSpace S} (h : t ≤ u) (ha : HasEval a) :

theorem MvPowerSeries.HasEval.zero {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] :

theorem MvPowerSeries.HasEval.add {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [ContinuousAdd S] [IsLinearTopology S S] {a b : σ → S} (ha : HasEval a) (hb : HasEval b) :

HasEval (a + b)

theorem MvPowerSeries.HasEval.mul_left {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] (c : σ → S) {x : σ → S} (hx : HasEval x) :

HasEval (c * x)

theorem MvPowerSeries.HasEval.mul_right {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] (c : σ → S) {x : σ → S} (hx : HasEval x) :

HasEval (x * c)

theorem MvPowerSeries.HasEval.map {σ : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] {S : Type u_3} [CommRing S] [TopologicalSpace S] {φ : R →+* S} (hφ : Continuous ⇑φ) {a : σ → R} (ha : HasEval a) :

HasEval fun (s : σ) => φ (a s)

[Bourbaki, Algebra, chap. 4, §4, n°3, Prop. 4 (i) (a & b)][bourbaki1981].

theorem MvPowerSeries.HasEval.X {σ : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] :

HasEval fun (s : σ) => X s

def MvPowerSeries.hasEvalIdeal {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] :

Ideal (σ → S)

The domain of evaluation of MvPowerSeries, as an ideal

Instances For

@[simp]

theorem MvPowerSeries.coe_hasEvalIdeal {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] :

↑hasEvalIdeal = {a : σ → S | HasEval a}

theorem MvPowerSeries.mem_hasEvalIdeal_iff {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] {a : σ → S} :

a ∈ hasEvalIdeal ↔ HasEval a

theorem MvPowerSeries.HasEval.pow {σ : Type u_1} {S : Type u_3} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] (x : σ → S) (ha : HasEval x) {p : ℕ} (hp : 0 < p) :

HasEval (x ^ p)

theorem MvPolynomial.toMvPowerSeries_isUniformInducing {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] :

IsUniformInducing toMvPowerSeries

theorem MvPolynomial.toMvPowerSeries_isDenseInducing {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] :

IsDenseInducing toMvPowerSeries

theorem MvPolynomial.toMvPowerSeries_uniformContinuous {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsUniformAddGroup R] [IsUniformAddGroup S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : MvPowerSeries.HasEval a) :

UniformContinuous ⇑(eval₂Hom φ a)

The evaluation map on multivariate polynomials is uniformly continuous for the uniform structure induced by that on multivariate power series.

noncomputable def MvPowerSeries.eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (f : MvPowerSeries σ R) :

S

Evaluation of a multivariate power series at f at a point a : σ → S.

It coincides with the evaluation of f as a polynomial if f is the coercion of a polynomial. Otherwise, it is only relevant if φ is continuous and HasEval a.

Instances For

@[simp]

theorem MvPowerSeries.eval₂_coe {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (f : MvPolynomial σ R) :

eval₂ φ a ↑f = MvPolynomial.eval₂ φ a f

@[simp]

theorem MvPowerSeries.eval₂_C {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (r : R) :

eval₂ φ a (C r) = φ r

@[simp]

theorem MvPowerSeries.eval₂_X {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] (φ : R →+* S) (a : σ → S) (s : σ) :

eval₂ φ a (X s) = a s

noncomputable def MvPowerSeries.eval₂Hom {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) :

MvPowerSeries σ R →+* S

Evaluation of power series at adequate elements, as a RingHom

Instances For

theorem MvPowerSeries.eval₂Hom_eq_extend {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) (f : MvPowerSeries σ R) :

(eval₂Hom hφ ha) f = ⋯.extend (MvPolynomial.eval₂ φ a) f

theorem MvPowerSeries.coe_eval₂Hom {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) :

⇑(eval₂Hom hφ ha) = eval₂ φ a

theorem MvPowerSeries.uniformContinuous_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) :

UniformContinuous (eval₂ φ a)

theorem MvPowerSeries.continuous_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) :

Continuous (eval₂ φ a)

theorem MvPowerSeries.hasSum_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) (f : MvPowerSeries σ R) :

HasSum (fun (d : σ →₀ ℕ) => φ ((coeff d) f) * d.prod fun (s : σ) (e : ℕ) => a s ^ e) (eval₂ φ a f)

theorem MvPowerSeries.eval₂_eq_tsum {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) (f : MvPowerSeries σ R) :

eval₂ φ a f = ∑' (d : σ →₀ ℕ), φ ((coeff d) f) * d.prod fun (s : σ) (e : ℕ) => a s ^ e

theorem MvPowerSeries.eval₂_unique {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) {ε : MvPowerSeries σ R → S} (hε : Continuous ε) (h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p) :

ε = eval₂ φ a

theorem MvPowerSeries.comp_eval₂ {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : HasEval a) {T : Type u_4} [UniformSpace T] [CompleteSpace T] [T2Space T] [CommRing T] [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T] {ε : S →+* T} (hε : Continuous ⇑ε) :

⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)

noncomputable def MvPowerSeries.aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) :

MvPowerSeries σ R →ₐ[R] S

Evaluation of power series at adequate elements, as an AlgHom

Instances For

theorem MvPowerSeries.coe_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) :

⇑(aeval ha) = eval₂ (algebraMap R S) a

theorem MvPowerSeries.continuous_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) :

Continuous ⇑(aeval ha)

@[simp]

theorem MvPowerSeries.aeval_coe {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) (p : MvPolynomial σ R) :

(aeval ha) ↑p = (MvPolynomial.aeval a) p

theorem MvPowerSeries.aeval_unique {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] {ε : MvPowerSeries σ R →ₐ[R] S} (hε : Continuous ⇑ε) :

aeval ⋯ = ε

theorem MvPowerSeries.hasSum_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) (f : MvPowerSeries σ R) :

HasSum (fun (d : σ →₀ ℕ) => (coeff d) f • d.prod fun (s : σ) (e : ℕ) => a s ^ e) ((aeval ha) f)

theorem MvPowerSeries.aeval_eq_sum {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) (f : MvPowerSeries σ R) :

(aeval ha) f = ∑' (d : σ →₀ ℕ), (coeff d) f • d.prod fun (s : σ) (e : ℕ) => a s ^ e

theorem MvPowerSeries.comp_aeval {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] {S : Type u_3} [CommRing S] [UniformSpace S] {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : HasEval a) {T : Type u_4} [CommRing T] [UniformSpace T] [IsUniformAddGroup T] [IsTopologicalRing T] [IsLinearTopology T T] [T2Space T] [Algebra R T] [ContinuousSMul R T] [CompleteSpace T] {ε : S →ₐ[R] T} (hε : Continuous ⇑ε) :

ε.comp (aeval ha) = aeval ⋯