Mathlib.Algebra.Polynomial.Eval.SMul

Module docstring

{"# Evaluating polynomials and scalar multiplication

Main results

eval₂_smul, eval_smul, map_smul, comp_smul: the functions preserve scalar multiplication
Polynomial.leval: Polynomial.eval as linear map

Polynomial.eval₂_smul theorem

(g : R →+* S) (p : R[X]) (x : S) {s : R} : eval₂ g x (s • p) = g s * eval₂ g x p

Full source

@[simp]
theorem eval₂_smul (g : R →+* S) (p : R[X]) (x : S) {s : R} :
    eval₂ g x (s • p) = g s * eval₂ g x p := by
  have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _
  have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A
  rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B] <;>
    simp [mul_sum, mul_assoc]

Evaluation of Scalar Multiple: $\text{eval}_2\, g\, x\, (s \cdot p) = g(s) \cdot \text{eval}_2\, g\, x\, p$

Informal description

Let $R$ and $S$ be semirings, and let $g : R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, any element $x \in S$, and any scalar $s \in R$, the evaluation of the scalar multiple $s \cdot p$ at $x$ via $g$ satisfies: $$ \text{eval}_2\, g\, x\, (s \cdot p) = g(s) \cdot \text{eval}_2\, g\, x\, p. $$

Polynomial.eval_smul theorem

[SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X]) (x : R) : (s • p).eval x = s • p.eval x

Full source

@[simp]
theorem eval_smul [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X])
    (x : R) : (s • p).eval x = s • p.eval x := by
  rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul]

Evaluation Preserves Scalar Multiplication: $(s \cdot p)(x) = s \cdot p(x)$

Informal description

Let $R$ be a semiring and $S$ a type with a scalar multiplication action on $R$ that preserves zero (`SMulZeroClass`). Suppose further that $S$ and $R$ form a scalar tower over $R$ (`IsScalarTower S R R`). Then for any scalar $s \in S$, any polynomial $p \in R[X]$, and any element $x \in R$, the evaluation of the scalar multiple $s \cdot p$ at $x$ satisfies: $$ (s \cdot p)(x) = s \cdot p(x). $$

Polynomial.leval definition

{R : Type*} [Semiring R] (r : R) : R[X] →ₗ[R] R

Full source

/-- `Polynomial.eval` as linear map -/
@[simps]
def leval {R : Type*} [Semiring R] (r : R) : R[X]R[X] →ₗ[R] R where
  toFun f := f.eval r
  map_add' _f _g := eval_add
  map_smul' c f := eval_smul c f r

Linear evaluation map for polynomials

Informal description

For a semiring $R$ and an element $r \in R$, the function $\text{leval}_r \colon R[X] \to R$ is the linear map that evaluates a polynomial $f \in R[X]$ at $r$, i.e., $\text{leval}_r(f) = f(r)$. This map is linear with respect to the $R$-module structures on $R[X]$ and $R$.

Polynomial.smul_comp theorem

[SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p q : R[X]) : (s • p).comp q = s • p.comp q

Full source

@[simp]
theorem smul_comp [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p q : R[X]) :
    (s • p).comp q = s • p.comp q := by
  rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]

Scalar Multiplication Commutes with Polynomial Composition: $(s \cdot p) \circ q = s \cdot (p \circ q)$

Informal description

Let $R$ be a semiring and $S$ a type with a scalar multiplication action on $R$ that preserves zero. Suppose further that $S$ and $R$ form a scalar tower over $R$. Then for any scalar $s \in S$ and any polynomials $p, q \in R[X]$, the composition of the scalar multiple $s \cdot p$ with $q$ satisfies: $$ (s \cdot p) \circ q = s \cdot (p \circ q). $$

Polynomial.map_smul theorem

(r : R) : (r • p).map f = f r • p.map f

Full source

@[simp]
protected theorem map_smul (r : R) : (r • p).map f = f r • p.map f := by
  rw [map, eval₂_smul, RingHom.comp_apply, C_mul']

Polynomial map preserves scalar multiplication: $f_*(r \cdot p) = f(r) \cdot f_*(p)$

Informal description

Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $r \in R$ a scalar. Then the image of the scalar multiple $r \cdot p$ under the polynomial map induced by $f$ equals the scalar multiple $f(r) \cdot (f_* p)$, where $f_* p$ denotes the polynomial in $S[X]$ obtained by applying $f$ to each coefficient of $p$. In symbols: $$ f_*(r \cdot p) = f(r) \cdot f_*(p) $$