Scalar-multiple polynomial evaluation

This file defines polynomial evaluation via scalar multiplication. Our polynomials have coefficients in a semiring R, and we evaluate at a weak form of R-algebra, namely an additive commutative monoid with an action of R and a notion of natural number power. This is a generalization of Algebra.Polynomial.Eval.

Main definitions

• Polynomial.smeval: function for evaluating a polynomial with coefficients in a Semiring R at an element x of an AddCommMonoid S that has natural number powers and an R-action.
• smeval.linearMap: the smeval function as an R-linear map, when S is an R-module.
• smeval.algebraMap: the smeval function as an R-algebra map, when S is an R-algebra.

Main results

• smeval_monomial: monomials evaluate as we expect.
• smeval_add, smeval_smul: linearity of evaluation, given an R-module.
• smeval_mul, smeval_comp: multiplicativity of evaluation, given power-associativity.
• eval₂_smulOneHom_eq_smeval, leval_eq_smeval.linearMap, aeval_eq_smeval, etc.: comparisons

TODO

• smeval_neg and smeval_intCast for R a ring and S an AddCommGroup.
• Nonunital evaluation for polynomials with vanishing constant term for Pow S ℕ+ (different file?)

def Polynomial.smul_pow {R : Type u_1} [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : ℕ → R → S

Scalar multiplication together with taking a natural number power.

Equations

• Polynomial.smul_pow x n r = r • x ^ n

@[irreducible]

def Polynomial.smeval {R : Type u_3} [Semiring R] (p : Polynomial R) {S : Type u_4} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : S

Evaluate a polynomial p in the scalar semiring R at an element x in the target S using scalar multiple R-action.

Equations

• p.smeval x = p.sum (Polynomial.smul_pow x)

theorem Polynomial.smeval_def {R : Type u_3} [Semiring R] (p : Polynomial R) {S : Type u_4} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : p.smeval x = p.sum (smul_pow x)

theorem Polynomial.smeval_eq_sum {R : Type u_1} [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : p.smeval x = p.sum (smul_pow x)

@[simp]

theorem Polynomial.smeval_C {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : (C r).smeval x = r • x ^ 0

@[simp]

theorem Polynomial.smeval_monomial {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) (n : ℕ) : ((monomial n) r).smeval x = r • x ^ n

theorem Polynomial.eval_eq_smeval {R : Type u_1} [Semiring R] (r : R) (p : Polynomial R) : eval r p = p.smeval r

theorem Polynomial.eval₂_smulOneHom_eq_smeval (R : Type u_3) [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [IsScalarTower R S S] (p : Polynomial R) (x : S) : eval₂ RingHom.smulOneHom x p = p.smeval x

@[simp]

theorem Polynomial.smeval_zero (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : smeval 0 x = 0

@[simp]

theorem Polynomial.smeval_one (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : smeval 1 x = 1 • x ^ 0

@[simp]

theorem Polynomial.smeval_X (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) : X.smeval x = x ^ 1

@[simp]

theorem Polynomial.smeval_X_pow (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) {n : ℕ} : (X ^ n).smeval x = x ^ n

@[simp]

theorem Polynomial.smeval_add (R : Type u_1) [Semiring R] (p q : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : (p + q).smeval x = p.smeval x + q.smeval x

theorem Polynomial.smeval_natCast (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (n : ℕ) : (↑n).smeval x = n • x ^ 0

@[simp]

theorem Polynomial.smeval_smul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (r : R) : (r • p).smeval x = r • p.smeval x

def Polynomial.smeval.linearMap (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : Polynomial R →ₗ[R] S

Polynomial.smeval as a linear map.

Equations

• Polynomial.smeval.linearMap R x = { toFun := fun (f : Polynomial R) => f.smeval x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.smeval.linearMap_apply (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : (linearMap R x) p = p.smeval x

theorem Polynomial.leval_coe_eq_smeval {R : Type u_3} [Semiring R] (r : R) : ⇑(leval r) = fun (p : Polynomial R) => p.smeval r

theorem Polynomial.leval_eq_smeval.linearMap {R : Type u_3} [Semiring R] (r : R) : leval r = smeval.linearMap R r

@[simp]

theorem Polynomial.smeval_neg (R : Type u_1) [Ring R] {S : Type u_2} [AddCommGroup S] [Pow S ℕ] [Module R S] (p : Polynomial R) (x : S) : (-p).smeval x = -p.smeval x

@[simp]

theorem Polynomial.smeval_sub (R : Type u_1) [Ring R] {S : Type u_2} [AddCommGroup S] [Pow S ℕ] [Module R S] (p q : Polynomial R) (x : S) : (p - q).smeval x = p.smeval x - q.smeval x

theorem Polynomial.smeval_neg_nat (S : Type u_3) [NonAssocRing S] [Pow S ℕ] [NatPowAssoc S] (q : Polynomial ℕ) (n : ℕ) : q.smeval (-↑n) = ↑(q.smeval (-↑n))

In the module docstring for algebras at Mathlib/Algebra/Algebra/Basic.lean, we see that [CommSemiring R] [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] is an equivalent way to express [CommSemiring R] [Semiring S] [Algebra R S] that allows one to relax the defining structures independently. For non-associative power-associative algebras (e.g., octonions), we replace the [Semiring S] with [NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S].

theorem Polynomial.smeval_C_mul (R : Type u_1) [Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) : (C r * p).smeval x = r • p.smeval x

theorem Polynomial.smeval_at_natCast {S : Type u_2} [NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S] (q : Polynomial ℕ) (n : ℕ) : q.smeval ↑n = ↑(q.smeval n)

theorem Polynomial.smeval_at_zero (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] [NatPowAssoc S] : p.smeval 0 = p.coeff 0 • 1

theorem Polynomial.smeval_X_mul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] : (X * p).smeval x = x * p.smeval x

theorem Polynomial.smeval_X_pow_assoc (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (m n : ℕ) : x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)

theorem Polynomial.smeval_X_pow_mul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ℕ) : (X ^ n * p).smeval x = x ^ n * p.smeval x

theorem Polynomial.smeval_monomial_mul (R : Type u_1) [Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ℕ) : ((monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)

theorem Polynomial.smeval_mul_X (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] : (p * X).smeval x = p.smeval x * x

theorem Polynomial.smeval_assoc_X_pow (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] (m n : ℕ) : p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)

theorem Polynomial.smeval_mul_X_pow (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] (n : ℕ) : (p * X ^ n).smeval x = p.smeval x * x ^ n

theorem Polynomial.smeval_mul (R : Type u_1) [Semiring R] (p q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] : (p * q).smeval x = p.smeval x * q.smeval x

theorem Polynomial.smeval_pow (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] (n : ℕ) : (p ^ n).smeval x = p.smeval x ^ n

theorem Polynomial.smeval_comp (R : Type u_1) [Semiring R] (p q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] : (p.comp q).smeval x = p.smeval (q.smeval x)

theorem Polynomial.smeval_commute_left (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] {x y : S} (hc : Commute x y) : Commute (p.smeval x) y

theorem Polynomial.smeval_commute (R : Type u_1) [Semiring R] (p q : Polynomial R) {S : Type u_2} [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] {x y : S} (hc : Commute x y) : Commute (p.smeval x) (q.smeval y)

theorem Polynomial.aeval_eq_smeval {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) : (aeval x) p = p.smeval x

theorem Polynomial.aeval_coe_eq_smeval {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Algebra R S] (x : S) : ⇑(aeval x) = fun (p : Polynomial R) => p.smeval x