mathlib documentation

data.polynomial.algebra_map

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] :

Note that this instance also provides algebra R (polynomial R).

Equations
theorem polynomial.algebra_map_apply {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (r : R) :

theorem polynomial.C_eq_algebra_map {R : Type u_1} [comm_ring R] (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) :

@[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) :

@[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) :

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} :

theorem polynomial.eval_comp {R : Type u} {a : R} [comm_semiring R] {p q : polynomial R} :

@[instance]
def polynomial.is_semiring_hom {R : Type u} [comm_semiring R] {p : polynomial R} :
is_semiring_hom (λ (q : polynomial R), q.comp p)

def polynomial.aeval {R : Type u} {A : Type z} [comm_semiring R] [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
theorem polynomial.aeval_def {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) (p : polynomial R) :

@[simp]
theorem polynomial.aeval_zero {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) :

@[simp]
theorem polynomial.aeval_X {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) :

@[simp]
theorem polynomial.aeval_C {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) (r : R) :

theorem polynomial.aeval_monomial {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) {n : } {r : R} :

@[simp]
theorem polynomial.aeval_X_pow {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) {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) :

@[simp]
theorem polynomial.aeval_one {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) :

@[simp]
theorem polynomial.aeval_bit0 {R : Type u} {A : Type z} [comm_semiring R] {p : polynomial R} [semiring A] [algebra R A] (x : A) :

@[simp]
theorem polynomial.aeval_bit1 {R : Type u} {A : Type z} [comm_semiring R] {p : polynomial R} [semiring A] [algebra R A] (x : A) :

@[simp]
theorem polynomial.aeval_nat_cast {R : Type u} {A : Type z} [comm_semiring R] [semiring A] [algebra R A] (x : A) (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) :

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) :

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) :

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) :

@[simp]

theorem polynomial.pow_comp {R : Type u} [comm_semiring R] (p q : polynomial R) (k : ) :
(p ^ k).comp q = p.comp q ^ k

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 = 0p.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} :

theorem polynomial.dvd_term_of_dvd_eval_of_dvd_terms {S : Type v} [comm_ring S] {z p : S} {f : polynomial S} (i : ) :
p polynomial.eval z f(∀ (j : ), j ip (f.coeff j) * z ^ j)p (f.coeff i) * z ^ i

theorem polynomial.dvd_term_of_is_root_of_dvd_terms {S : Type v} [comm_ring S] {r p : S} {f : polynomial S} (i : ) :
f.is_root r(∀ (j : ), j ip (f.coeff j) * r ^ j)p (f.coeff i) * r ^ i

theorem polynomial.eval_mul_X_sub_C {R : Type u} [ring R] {p : polynomial R} (r : R) :

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)