Documentation

Mathlib.RingTheory.PowerSeries.Evaluation

Evaluation of power series #

Power series in one indeterminate are the particular case of multivariate power series, for the Unit type of indeterminates. This file provides a simpler syntax.

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, PowerSeries.eval₂ f φ a is the evaluation of the 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 is topologically nilpotent (a ^ n tends to 0 when n tends to infinity).

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

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

We refer to the documentation of MvPowerSeries.eval₂ for more details.

@[reducible, inline]

abbrev PowerSeries.HasEval {S : Type u_2} [CommRing S] [TopologicalSpace S] (a : S) :

Points at which evaluation of power series is well behaved

Equations

PowerSeries.HasEval a = IsTopologicallyNilpotent a

Instances For

theorem PowerSeries.hasEval_def {S : Type u_2} [CommRing S] [TopologicalSpace S] (a : S) :

HasEval a ↔ IsTopologicallyNilpotent a

theorem PowerSeries.hasEval_iff {S : Type u_2} [CommRing S] [TopologicalSpace S] {a : S} :

HasEval a ↔ MvPowerSeries.HasEval fun (x : Unit) => a

theorem PowerSeries.hasEval {S : Type u_2} [CommRing S] [TopologicalSpace S] {a : S} (ha : HasEval a) :

MvPowerSeries.HasEval fun (x : Unit) => a

theorem PowerSeries.HasEval.mono {S : Type u_3} [CommRing S] {a : S} {t u : TopologicalSpace S} (h : t ≤ u) (ha : HasEval a) :

theorem PowerSeries.HasEval.zero {S : Type u_2} [CommRing S] [TopologicalSpace S] :

theorem PowerSeries.HasEval.add {S : Type u_2} [CommRing S] [TopologicalSpace S] [ContinuousAdd S] [IsLinearTopology S S] {a b : S} (ha : HasEval a) (hb : HasEval b) :

HasEval (a + b)

theorem PowerSeries.HasEval.mul_left {S : Type u_2} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] (c : S) {x : S} (hx : HasEval x) :

HasEval (c * x)

theorem PowerSeries.HasEval.mul_right {S : Type u_2} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] (c : S) {x : S} (hx : HasEval x) :

HasEval (x * c)

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

HasEval (φ a)

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

theorem PowerSeries.HasEval.X {R : Type u_1} [CommRing R] [TopologicalSpace R] :

def PowerSeries.hasEvalIdeal {S : Type u_2} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] :

The domain of evaluation of MvPowerSeries, as an ideal

Equations

PowerSeries.hasEvalIdeal = { carrier := {a : S | PowerSeries.HasEval a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

@[simp]

theorem PowerSeries.coe_hasEvalIdeal {S : Type u_2} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] :

↑hasEvalIdeal = {a : S | HasEval a}

theorem PowerSeries.mem_hasEvalIdeal_iff {S : Type u_2} [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [IsLinearTopology S S] {a : S} :

a ∈ hasEvalIdeal ↔ HasEval a

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

PowerSeries R → S

Evaluation of a power series f at a point a.

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 a is topologically nilpotent.

Equations

PowerSeries.eval₂ φ a = MvPowerSeries.eval₂ φ fun (x : Unit) => a

Instances For

@[simp]

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

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

@[simp]

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

eval₂ φ a ((C R) r) = φ r

@[simp]

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

eval₂ φ a X = a

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

PowerSeries R →+* S

The evaluation homomorphism at a on PowerSeries, as a RingHom.

Equations

PowerSeries.eval₂Hom hφ ha = MvPowerSeries.eval₂Hom hφ ⋯

Instances For

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

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

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

UniformContinuous (eval₂ φ a)

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

Continuous (eval₂ φ a)

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

HasSum (fun (d : ℕ) => φ ((coeff R d) f) * a ^ d) (eval₂ φ a f)

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

eval₂ φ a f = ∑' (d : ℕ), φ ((coeff R d) f) * a ^ d

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

ε = eval₂ φ a

theorem PowerSeries.comp_eval₂ {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {φ : R →+* S} {a : S} [UniformSpace R] [UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R] [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : IsTopologicallyNilpotent a) {T : Type u_3} [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 PowerSeries.aeval {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {a : S} [UniformSpace R] [UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R] [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : IsTopologicallyNilpotent a) :

PowerSeries R →ₐ[R] S

For IsTopologicallyNilpotent a, the evaluation homomorphism at a on PowerSeries, as an AlgHom.

Equations

PowerSeries.aeval ha = MvPowerSeries.aeval ⋯

Instances For

theorem PowerSeries.coe_aeval {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {a : S} [UniformSpace R] [UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R] [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : IsTopologicallyNilpotent a) :

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

theorem PowerSeries.continuous_aeval {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {a : S} [UniformSpace R] [UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R] [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : IsTopologicallyNilpotent a) :

Continuous ⇑(aeval ha)

@[simp]

theorem PowerSeries.aeval_coe {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {a : S} [UniformSpace R] [UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R] [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : IsTopologicallyNilpotent a) (p : Polynomial R) :

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

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

aeval ⋯ = ε

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

HasSum (fun (d : ℕ) => (coeff R d) f • a ^ d) ((aeval ha) f)

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

(aeval ha) f = ∑' (d : ℕ), (coeff R d) f • a ^ d

theorem PowerSeries.comp_aeval {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {a : S} [UniformSpace R] [UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R] [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S] [Algebra R S] [ContinuousSMul R S] (ha : IsTopologicallyNilpotent a) {T : Type u_3} [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 ⋯