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)
Equations
@[simp]
def
polynomial.aeval
{R : Type u}
{A : Type z}
[comm_semiring R]
[comm_semiring A]
[algebra R A] :
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) 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]
[comm_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_X
{R : Type u}
{A : Type z}
[comm_semiring R]
[comm_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]
[comm_semiring A]
[algebra R A]
(x : A)
(r : R) :
⇑(polynomial.aeval x) (⇑polynomial.C r) = ⇑(algebra_map R A) r
theorem
polynomial.eval_unique
{R : Type u}
{A : Type z}
[comm_semiring R]
[comm_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]
[comm_semiring A]
[algebra R A]
{B : Type u_1}
[comm_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]
[comm_semiring A]
[algebra R A]
{B : Type u_1}
[comm_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} :
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} :
⇑(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.