# mathlibdocumentation

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.

@[protected, instance]
noncomputable def polynomial.algebra_of_algebra {R : Type u} {A : Type z} [semiring A] [ A] :

Note that this instance also provides algebra R R[X].

Equations
theorem polynomial.algebra_map_apply {R : Type u} {A : Type z} [semiring A] [ A] (r : R) :
@[simp]
theorem polynomial.to_finsupp_algebra_map {R : Type u} {A : Type z} [semiring A] [ A] (r : R) :
theorem polynomial.of_finsupp_algebra_map {R : Type u} {A : Type z} [semiring A] [ A] (r : R) :
{to_finsupp := )) r} = (polynomial A)) r
theorem polynomial.C_eq_algebra_map {R : Type u} (r : R) :
= (polynomial R)) r

When we have [comm_semiring R], the function C is the same as algebra_map R R[X].

(But note that C is defined when R is not necessarily commutative, in which case algebra_map is not available.)

@[ext]
theorem polynomial.alg_hom_ext' {R : Type u} {A' : Type u_1} {B' : Type u_2} [comm_semiring A'] [semiring B'] [ A'] [ B'] {f g : →ₐ[R] B'} (h₁ : f.comp (polynomial A')) = g.comp (polynomial A'))) (h₂ : = ) :
f = g

Extensionality lemma for algebra maps out of polynomial A' over a smaller base ring than A'

@[simp]
theorem polynomial.to_finsupp_iso_alg_symm_apply (R : Type u) (ᾰ : ) :
@[simp]
theorem polynomial.to_finsupp_iso_alg_apply (R : Type u) (ᾰ : polynomial R) :
noncomputable def polynomial.to_finsupp_iso_alg (R : Type u)  :

Algebra isomorphism between polynomial R and add_monoid_algebra R ℕ. This is just an implementation detail, but it can be useful to transfer results from finsupp to polynomials.

Equations
@[protected, instance]
def polynomial.subalgebra.nontrivial {R : Type u} {A : Type z} [semiring A] [ A] [nontrivial A] :
@[simp]
theorem polynomial.alg_hom_eval₂_algebra_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [semiring A] [semiring B] [ A] [ B] (p : polynomial R) (f : A →ₐ[R] B) (a : A) :
f (polynomial.eval₂ A) a p) = (f a) p
@[simp]
theorem polynomial.eval₂_algebra_map_X {R : Type u_1} {A : Type u_2} [semiring A] [ A] (p : polynomial R) (f : →ₐ[R] A) :
p = f p
@[simp]
theorem polynomial.ring_hom_eval₂_cast_int_ring_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] (p : polynomial ) (f : R →+* S) (r : R) :
f p) = (f r) p
@[simp]
theorem polynomial.eval₂_int_cast_ring_hom_X {R : Type u_1} [ring R] (p : polynomial ) (f : →+* R) :
= f p
noncomputable def polynomial.aeval {R : Type u} {A : Type z} [semiring A] [ A] (x : 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.

This is a stronger variant of the linear map polynomial.leval.

Equations
@[simp]
theorem polynomial.adjoin_X {R : Type u}  :
@[ext]
theorem polynomial.alg_hom_ext {R : Type u} {A : Type z} [semiring A] [ A] {f g : →ₐ[R] A} (h : = ) :
f = g
theorem polynomial.aeval_def {R : Type u} {A : Type z} [semiring A] [ A] (x : A) (p : polynomial R) :
p = x p
@[simp]
theorem polynomial.aeval_zero {R : Type u} {A : Type z} [semiring A] [ A] (x : A) :
0 = 0
@[simp]
theorem polynomial.aeval_X {R : Type u} {A : Type z} [semiring A] [ A] (x : A) :
@[simp]
theorem polynomial.aeval_C {R : Type u} {A : Type z} [semiring A] [ A] (x : A) (r : R) :
= A) r
@[simp]
theorem polynomial.aeval_monomial {R : Type u} {A : Type z} [semiring A] [ A] (x : A) {n : } {r : R} :
( r) = A) r * x ^ n
@[simp]
theorem polynomial.aeval_X_pow {R : Type u} {A : Type z} [semiring A] [ A] (x : A) {n : } :
= x ^ n
@[simp]
theorem polynomial.aeval_add {R : Type u} {A : Type z} {p q : polynomial R} [semiring A] [ A] (x : A) :
(p + q) = p + q
@[simp]
theorem polynomial.aeval_one {R : Type u} {A : Type z} [semiring A] [ A] (x : A) :
1 = 1
@[simp]
theorem polynomial.aeval_bit0 {R : Type u} {A : Type z} {p : polynomial R} [semiring A] [ A] (x : A) :
(bit0 p) = bit0 ( p)
@[simp]
theorem polynomial.aeval_bit1 {R : Type u} {A : Type z} {p : polynomial R} [semiring A] [ A] (x : A) :
(bit1 p) = bit1 ( p)
@[simp]
theorem polynomial.aeval_nat_cast {R : Type u} {A : Type z} [semiring A] [ A] (x : A) (n : ) :
n = n
theorem polynomial.aeval_mul {R : Type u} {A : Type z} {p q : polynomial R} [semiring A] [ A] (x : A) :
(p * q) = p * q
theorem polynomial.aeval_comp {R : Type u} {p q : polynomial R} {A : Type u_1} [ A] (x : A) :
(p.comp q) = (polynomial.aeval ( q)) p
@[simp]
theorem polynomial.aeval_map {R : Type u} {B : Type u_3} [semiring B] [ B] {A : Type u_1} [ A] [ B] [ B] (b : B) (p : polynomial R) :
(polynomial.map A) p) = p
theorem polynomial.aeval_alg_hom {R : Type u} {A : Type z} [semiring A] [ A] {B : Type u_3} [semiring B] [ B] (f : A →ₐ[R] B) (x : A) :
@[simp]
theorem polynomial.aeval_X_left {R : Type u}  :
theorem polynomial.eval_unique {R : Type u} {A : Type z} [semiring A] [ A] (φ : →ₐ[R] A) (p : polynomial R) :
φ p = p
theorem polynomial.aeval_alg_hom_apply {R : Type u} {A : Type z} [semiring A] [ A] {B : Type u_3} [semiring B] [ B] (f : A →ₐ[R] B) (x : A) (p : polynomial R) :
theorem polynomial.aeval_alg_equiv {R : Type u} {A : Type z} [semiring A] [ A] {B : Type u_3} [semiring B] [ B] (f : A ≃ₐ[R] B) (x : A) :
theorem polynomial.aeval_alg_equiv_apply {R : Type u} {A : Type z} [semiring A] [ A] {B : Type u_3} [semiring B] [ B] (f : A ≃ₐ[R] B) (x : A) (p : polynomial R) :
theorem polynomial.aeval_algebra_map_apply {R : Type u} {A : Type z} [semiring A] [ A] (x : R) (p : polynomial R) :
(polynomial.aeval ( A) x)) p = A) p)
@[simp]
theorem polynomial.coe_aeval_eq_eval {R : Type u} (r : R) :
@[simp]
theorem polynomial.aeval_fn_apply {R : Type u} {X : Type u_1} (g : polynomial R) (f : X → R) (x : X) :
g x = (polynomial.aeval (f x)) g
@[norm_cast]
theorem polynomial.aeval_subalgebra_coe {R : Type u} (g : polynomial R) {A : Type u_1} [semiring A] [ A] (s : A) (f : s) :
( g) = g
theorem polynomial.coeff_zero_eq_aeval_zero {R : Type u} (p : polynomial R) :
p.coeff 0 = p
theorem polynomial.coeff_zero_eq_aeval_zero' {R : Type u} {A : Type z} [semiring A] [ A] (p : polynomial R) :
A) (p.coeff 0) = p
theorem algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type z} [semiring A] [ A] (x : A) :
{x} =
theorem polynomial.aeval_eq_sum_range {R : Type u} {S : Type v} [ S] {p : polynomial R} (x : S) :
p = (finset.range (p.nat_degree + 1)).sum (λ (i : ), p.coeff i x ^ i)
theorem polynomial.aeval_eq_sum_range' {R : Type u} {S : Type v} [ S] {p : polynomial R} {n : } (hn : p.nat_degree < n) (x : S) :
p = (finset.range n).sum (λ (i : ), p.coeff i x ^ i)
theorem polynomial.is_root_of_eval₂_map_eq_zero {R : Type u} {S : Type v} {p : polynomial R} {f : R →+* S} (hf : function.injective f) {r : R} :
(f r) p = 0p.is_root r
theorem polynomial.is_root_of_aeval_algebra_map_eq_zero {R : Type u} {S : Type v} [ S] {p : polynomial R} (inj : function.injective S)) {r : R} (hr : (polynomial.aeval ( S) r)) p = 0) :
noncomputable def polynomial.aeval_tower {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (f : R →ₐ[S] A') (x : A') :

Version of aeval for defining algebra homs out of polynomial R over a smaller base ring than R.

Equations
@[simp]
theorem polynomial.aeval_tower_X {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') :
@[simp]
theorem polynomial.aeval_tower_C {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') (x : R) :
= g x
@[simp]
theorem polynomial.aeval_tower_comp_C {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') :
@[simp]
theorem polynomial.aeval_tower_algebra_map {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') (x : R) :
( (polynomial R)) x) = g x
@[simp]
theorem polynomial.aeval_tower_comp_algebra_map {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') :
theorem polynomial.aeval_tower_to_alg_hom {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') (x : R) :
( (polynomial R)) x) = g x
@[simp]
theorem polynomial.aeval_tower_comp_to_alg_hom {R : Type u} {S : Type v} {A' : Type u_1} [comm_semiring A'] [ R] [ A'] (g : R →ₐ[S] A') (y : A') :
.comp (polynomial R)) = g
@[simp]
theorem polynomial.aeval_tower_id {S : Type v}  :
@[simp]
theorem polynomial.aeval_tower_of_id {S : Type v} {A' : Type u_1} [comm_semiring A'] [ A'] :
theorem polynomial.dvd_term_of_dvd_eval_of_dvd_terms {S : Type v} [comm_ring S] {z p : S} {f : polynomial S} (i : ) (dvd_eval : p ) (dvd_terms : ∀ (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 : ) (hr : f.is_root r) (h : ∀ (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) :
(p * = 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.not_is_unit_X_sub_C {R : Type u} [ring R] [nontrivial R] (r : R) :
theorem polynomial.aeval_endomorphism {R : Type u} {M : Type u_1} [comm_ring R] [ M] (f : M →ₗ[R] M) (v : M) (p : polynomial R) :
( p) v = p.sum (λ (n : ) (b : R), b (f ^ n) v)