Theory of univariate polynomials
We show that polynomial A is an R-algebra when A is an R-algebra.
We promote eval₂ to an algebra hom in aeval.
@[instance]
def
polynomial.algebra_of_algebra
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A] :
algebra R (polynomial A)
Note that this instance also provides algebra R (polynomial R).
theorem
polynomial.algebra_map_apply
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
⇑(algebra_map R (polynomial A)) r = ⇑polynomial.C (⇑(algebra_map R A) r)
theorem
polynomial.C_eq_algebra_map
{R : Type u_1}
[comm_ring R]
(r : R) :
⇑polynomial.C r = ⇑(algebra_map R (polynomial R)) r
When we have [comm_ring R], the function C is the same as algebra_map R (polynomial R).
(But note that C is defined when R is not necessarily commutative, in which case
algebra_map is not available.)
@[simp]
theorem
polynomial.alg_hom_eval₂_algebra_map
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_ring R]
[ring A]
[ring B]
[algebra R A]
[algebra R B]
(p : polynomial R)
(f : A →ₐ[R] B)
(a : A) :
⇑f (polynomial.eval₂ (algebra_map R A) a p) = polynomial.eval₂ (algebra_map R B) (⇑f a) p
@[simp]
theorem
polynomial.eval₂_algebra_map_X
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
(p : polynomial R)
(f : polynomial R →ₐ[R] A) :
polynomial.eval₂ (algebra_map R A) (⇑f polynomial.X) p = ⇑f p
@[simp]
theorem
polynomial.ring_hom_eval₂_algebra_map_int
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
(p : polynomial ℤ)
(f : R →+* S)
(r : R) :
⇑f (polynomial.eval₂ (algebra_map ℤ R) r p) = polynomial.eval₂ (algebra_map ℤ S) (⇑f r) p
@[simp]
theorem
polynomial.eval₂_algebra_map_int_X
{R : Type u_1}
[ring R]
(p : polynomial ℤ)
(f : polynomial ℤ →+* R) :
polynomial.eval₂ (algebra_map ℤ R) (⇑f polynomial.X) p = ⇑f p
theorem
polynomial.eval₂_comp
{R : Type u}
{S : Type v}
[comm_semiring R]
{p q : polynomial R}
[comm_semiring S]
(f : R →+* S)
{x : S} :
polynomial.eval₂ f x (p.comp q) = polynomial.eval₂ f (polynomial.eval₂ f x q) p
theorem
polynomial.eval_comp
{R : Type u}
{a : R}
[comm_semiring R]
{p q : polynomial R} :
polynomial.eval a (p.comp q) = polynomial.eval (polynomial.eval a q) p
@[instance]
def
polynomial.is_semiring_hom
{R : Type u}
[comm_semiring R]
{p : polynomial R} :
is_semiring_hom (λ (q : polynomial R), q.comp p)
@[simp]
def
polynomial.aeval
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
polynomial R →ₐ[R] A
Given a valuation x of the variable in an R-algebra A, aeval R A x is
the unique R-algebra homomorphism from R[X] to A sending X to x.
Equations
- polynomial.aeval x = {to_fun := (polynomial.eval₂_ring_hom' (algebra_map R A) algebra.commutes x).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
polynomial.aeval_def
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
(p : polynomial R) :
⇑(polynomial.aeval x) p = polynomial.eval₂ (algebra_map R A) x p
@[simp]
theorem
polynomial.aeval_zero
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) 0 = 0
@[simp]
theorem
polynomial.aeval_X
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) polynomial.X = x
@[simp]
theorem
polynomial.aeval_C
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
(r : R) :
⇑(polynomial.aeval x) (⇑polynomial.C r) = ⇑(algebra_map R A) r
theorem
polynomial.aeval_monomial
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
{n : ℕ}
{r : R} :
⇑(polynomial.aeval x) (polynomial.monomial n r) = (⇑(algebra_map R A) r) * x ^ n
@[simp]
theorem
polynomial.aeval_X_pow
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
{n : ℕ} :
⇑(polynomial.aeval x) (polynomial.X ^ n) = x ^ n
@[simp]
theorem
polynomial.aeval_add
{R : Type u}
{A : Type z}
[comm_semiring R]
{p q : polynomial R}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (p + q) = ⇑(polynomial.aeval x) p + ⇑(polynomial.aeval x) q
@[simp]
theorem
polynomial.aeval_one
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) 1 = 1
@[simp]
theorem
polynomial.aeval_bit0
{R : Type u}
{A : Type z}
[comm_semiring R]
{p : polynomial R}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (bit0 p) = bit0 (⇑(polynomial.aeval x) p)
@[simp]
theorem
polynomial.aeval_bit1
{R : Type u}
{A : Type z}
[comm_semiring R]
{p : polynomial R}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (bit1 p) = bit1 (⇑(polynomial.aeval x) p)
@[simp]
theorem
polynomial.aeval_nat_cast
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
(n : ℕ) :
⇑(polynomial.aeval x) ↑n = ↑n
theorem
polynomial.aeval_mul
{R : Type u}
{A : Type z}
[comm_semiring R]
{p q : polynomial R}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (p * q) = (⇑(polynomial.aeval x) p) * ⇑(polynomial.aeval x) q
theorem
polynomial.eval_unique
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(φ : polynomial R →ₐ[R] A)
(p : polynomial R) :
⇑φ p = polynomial.eval₂ (algebra_map R A) (⇑φ polynomial.X) p
theorem
polynomial.aeval_alg_hom
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
{B : Type u_1}
[semiring B]
[algebra R B]
(f : A →ₐ[R] B)
(x : A) :
polynomial.aeval (⇑f x) = f.comp (polynomial.aeval x)
theorem
polynomial.aeval_alg_hom_apply
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
{B : Type u_1}
[semiring B]
[algebra R B]
(f : A →ₐ[R] B)
(x : A)
(p : polynomial R) :
⇑(polynomial.aeval (⇑f x)) p = ⇑f (⇑(polynomial.aeval x) p)
@[simp]
theorem
polynomial.coeff_zero_eq_aeval_zero
{R : Type u}
[comm_semiring R]
(p : polynomial R) :
p.coeff 0 = ⇑(polynomial.aeval 0) p
theorem
polynomial.is_root_of_eval₂_map_eq_zero
{R : Type u}
{S : Type v}
[comm_semiring R]
{p : polynomial R}
[comm_ring S]
{f : R →+* S}
(hf : function.injective ⇑f)
{r : R}
(a : polynomial.eval₂ f (⇑f r) p = 0) :
p.is_root r
theorem
polynomial.is_root_of_aeval_algebra_map_eq_zero
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_ring S]
[algebra R S]
{p : polynomial R}
(inj : function.injective ⇑(algebra_map R S))
{r : R}
(hr : ⇑(polynomial.aeval (⇑(algebra_map R S) r)) p = 0) :
p.is_root r
theorem
polynomial.eval_mul_X_sub_C
{R : Type u}
[ring R]
{p : polynomial R}
(r : R) :
polynomial.eval r (p * (polynomial.X - ⇑polynomial.C r)) = 0
The evaluation map is not generally multiplicative when the coefficient ring is noncommutative,
but nevertheless any polynomial of the form p * (X - monomial 0 r) is sent to zero
when evaluated at r.
This is the key step in our proof of the Cayley-Hamilton theorem.
theorem
polynomial.aeval_endomorphism
{R : Type u}
{M : Type u_1}
[comm_ring R]
[add_comm_group M]
[module R M]
(f : M →ₗ[R] M)
(v : M)
(p : polynomial R) :
⇑(⇑(polynomial.aeval f) p) v = finsupp.sum p (λ (n : ℕ) (b : R), b • ⇑(f ^ n) v)