# Theory of univariate polynomials #

We show that A[X] is an R-algebra when A is an R-algebra. We promote eval₂ to an algebra hom in aeval.

instance Polynomial.algebraOfAlgebra {R : Type u} {A : Type z} [] [] [Algebra R A] :
Algebra R ()

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

Equations
• Polynomial.algebraOfAlgebra = Algebra.mk (Polynomial.C.comp ())
@[simp]
theorem Polynomial.algebraMap_apply {R : Type u} {A : Type z} [] [] [Algebra R A] (r : R) :
(algebraMap R ()) r = Polynomial.C (() r)
@[simp]
theorem Polynomial.toFinsupp_algebraMap {R : Type u} {A : Type z} [] [] [Algebra R A] (r : R) :
((algebraMap R ()) r).toFinsupp = () r
theorem Polynomial.ofFinsupp_algebraMap {R : Type u} {A : Type z} [] [] [Algebra R A] (r : R) :
{ toFinsupp := () r } = (algebraMap R ()) r
theorem Polynomial.C_eq_algebraMap {R : Type u} [] (r : R) :
Polynomial.C r = (algebraMap R ()) r

When we have [CommSemiring R], the function C is the same as algebraMap R R[X].

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

@[simp]
theorem Polynomial.algebraMap_eq {R : Type u} [] :
algebraMap R () = Polynomial.C
@[simp]
theorem Polynomial.CAlgHom_apply {R : Type u} {A : Type z} [] [] [Algebra R A] :
∀ (a : A), Polynomial.CAlgHom a = Polynomial.C a
def Polynomial.CAlgHom {R : Type u} {A : Type z} [] [] [Algebra R A] :

Polynomial.C as an AlgHom.

Equations
• Polynomial.CAlgHom = { toRingHom := Polynomial.C, commutes' := }
Instances For
theorem Polynomial.algHom_ext' {R : Type u} {A : Type z} {B : Type u_2} [] [] [] [Algebra R A] [Algebra R B] {f : →ₐ[R] B} {g : →ₐ[R] B} (hC : f.comp Polynomial.CAlgHom = g.comp Polynomial.CAlgHom) (hX : f Polynomial.X = g Polynomial.X) :
f = g

Extensionality lemma for algebra maps out of A'[X] over a smaller base ring than A'

@[simp]
theorem Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp (R : Type u) [] (toFinsupp : ) :
(.symm toFinsupp).toFinsupp = toFinsupp
@[simp]
theorem Polynomial.toFinsuppIsoAlg_apply (R : Type u) [] (self : ) :
self = self.toFinsupp

Algebra isomorphism between R[X] and R[ℕ]. This is just an implementation detail, but it can be useful to transfer results from Finsupp to polynomials.

Equations
• = let __src := ; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
instance Polynomial.subalgebraNontrivial {R : Type u} {A : Type z} [] [] [Algebra R A] [] :
Equations
• =
@[simp]
theorem Polynomial.algHom_eval₂_algebraMap {R : Type u_3} {A : Type u_4} {B : Type u_5} [] [] [] [Algebra R A] [Algebra R B] (p : ) (f : A →ₐ[R] B) (a : A) :
@[simp]
theorem Polynomial.eval₂_algebraMap_X {R : Type u_3} {A : Type u_4} [] [] [Algebra R A] (p : ) (f : →ₐ[R] A) :
Polynomial.eval₂ () (f Polynomial.X) p = f p
@[simp]
theorem Polynomial.ringHom_eval₂_cast_int_ringHom {R : Type u_3} {S : Type u_4} [Ring R] [Ring S] (p : ) (f : R →+* S) (r : R) :
f () = Polynomial.eval₂ () (f r) p
@[simp]
theorem Polynomial.eval₂_intCastRingHom_X {R : Type u_3} [Ring R] (p : ) (f : ) :
Polynomial.eval₂ () (f Polynomial.X) p = f p
@[simp]
theorem Polynomial.eval₂AlgHom'_apply {R : Type u} {A : Type z} {B : Type u_2} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b) (p : ) :
() p = Polynomial.eval₂ (f) b p
def Polynomial.eval₂AlgHom' {R : Type u} {A : Type z} {B : Type u_2} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b) :

Polynomial.eval₂ as an AlgHom for noncommutative algebras.

This is Polynomial.eval₂RingHom' for AlgHoms.

Equations
Instances For
def Polynomial.aeval {R : Type u} {A : Type z} [] [] [Algebra R 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
Instances For
@[simp]
theorem Polynomial.adjoin_X {R : Type u} [] :
theorem Polynomial.algHom_ext {R : Type u} {B : Type u_2} [] [] [Algebra R B] {f : →ₐ[R] B} {g : →ₐ[R] B} (hX : f Polynomial.X = g Polynomial.X) :
f = g
theorem Polynomial.aeval_def {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) (p : ) :
() p = Polynomial.eval₂ () x p
theorem Polynomial.aeval_zero {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) :
() 0 = 0
@[simp]
theorem Polynomial.aeval_X {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) :
() Polynomial.X = x
@[simp]
theorem Polynomial.aeval_C {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) (r : R) :
() (Polynomial.C r) = () r
@[simp]
theorem Polynomial.aeval_monomial {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) {n : } {r : R} :
() ( r) = () r * x ^ n
theorem Polynomial.aeval_X_pow {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) {n : } :
() (Polynomial.X ^ n) = x ^ n
theorem Polynomial.aeval_add {R : Type u} {A : Type z} [] [] [Algebra R A] {p : } {q : } (x : A) :
() (p + q) = () p + () q
theorem Polynomial.aeval_one {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) :
() 1 = 1
@[deprecated]
theorem Polynomial.aeval_bit0 {R : Type u} {A : Type z} [] [] [Algebra R A] {p : } (x : A) :
() (bit0 p) = bit0 (() p)
@[deprecated]
theorem Polynomial.aeval_bit1 {R : Type u} {A : Type z} [] [] [Algebra R A] {p : } (x : A) :
() (bit1 p) = bit1 (() p)
theorem Polynomial.aeval_natCast {R : Type u} {A : Type z} [] [] [Algebra R A] (x : A) (n : ) :
() n = n
theorem Polynomial.aeval_mul {R : Type u} {A : Type z} [] [] [Algebra R A] {p : } {q : } (x : A) :
() (p * q) = () p * () q
theorem Polynomial.comp_eq_aeval {R : Type u} [] {p : } {q : } :
p.comp q = () p
theorem Polynomial.aeval_comp {R : Type u} [] {p : } {q : } {A : Type u_3} [] [Algebra R A] (x : A) :
() (p.comp q) = (Polynomial.aeval (() q)) p
@[simp]
theorem Polynomial.algEquivOfCompEqX_apply {R : Type u} [] (p : ) (q : ) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) (a : ) :
(p.algEquivOfCompEqX q hpq hqp) a = () a
@[simp]
theorem Polynomial.algEquivOfCompEqX_symm_apply {R : Type u} [] (p : ) (q : ) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) (a : ) :
(p.algEquivOfCompEqX q hpq hqp).symm a = () a
def Polynomial.algEquivOfCompEqX {R : Type u} [] (p : ) (q : ) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) :

Two polynomials p and q such that p(q(X))=X and q(p(X))=X induces an automorphism of the polynomial algebra.

Equations
• p.algEquivOfCompEqX q hpq hqp =
Instances For
@[simp]
theorem Polynomial.algEquivAevalXAddC_symm_apply {R : Type u_3} [] (t : R) (a : ) :
.symm a = (Polynomial.aeval (Polynomial.X - Polynomial.C t)) a
@[simp]
theorem Polynomial.algEquivAevalXAddC_apply {R : Type u_3} [] (t : R) (a : ) :
= (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a
def Polynomial.algEquivAevalXAddC {R : Type u_3} [] (t : R) :

The automorphism of the polynomial algebra given by p(X) ↦ p(X+t), with inverse p(X) ↦ p(X-t).

Equations
• = (Polynomial.X + Polynomial.C t).algEquivOfCompEqX (Polynomial.X - Polynomial.C t)
Instances For
theorem Polynomial.aeval_algHom {R : Type u} {A : Type z} {B : Type u_2} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (x : A) :
Polynomial.aeval (f x) = f.comp ()
@[simp]
theorem Polynomial.aeval_X_left {R : Type u} [] :
Polynomial.aeval Polynomial.X = AlgHom.id R ()
theorem Polynomial.aeval_X_left_apply {R : Type u} [] (p : ) :
(Polynomial.aeval Polynomial.X) p = p
theorem Polynomial.eval_unique {R : Type u} {A : Type z} [] [] [Algebra R A] (φ : →ₐ[R] A) (p : ) :
φ p = Polynomial.eval₂ () (φ Polynomial.X) p
theorem Polynomial.aeval_algHom_apply {R : Type u} {A : Type z} {B : Type u_2} [] [] [] [Algebra R A] [Algebra R B] {F : Type u_3} [FunLike F A B] [AlgHomClass F R A B] (f : F) (x : A) (p : ) :
(Polynomial.aeval (f x)) p = f (() p)
@[simp]
theorem Polynomial.coe_aeval_mk_apply {R : Type u} {A : Type z} [] [] [Algebra R A] {p : } (x : A) {S : } (h : x S) :
((Polynomial.aeval x, h) p) = () p
theorem Polynomial.aeval_algEquiv {R : Type u} {A : Type z} {B : Type u_2} [] [] [] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (x : A) :
Polynomial.aeval (f x) = (f).comp ()
theorem Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval {R : Type u} {A : Type z} [] [] [Algebra R A] (x : R) (p : ) :
(Polynomial.aeval (() x)) p = () ()
@[simp]
theorem Polynomial.coe_aeval_eq_eval {R : Type u} [] (r : R) :
@[simp]
theorem Polynomial.coe_aeval_eq_evalRingHom {R : Type u} [] (x : R) :
@[simp]
theorem Polynomial.aeval_fn_apply {R : Type u} [] {X : Type u_3} (g : ) (f : XR) (x : X) :
() g x = (Polynomial.aeval (f x)) g
theorem Polynomial.aeval_subalgebra_coe {R : Type u} [] (g : ) {A : Type u_3} [] [Algebra R A] (s : ) (f : s) :
(() g) = () g
theorem Polynomial.coeff_zero_eq_aeval_zero {R : Type u} [] (p : ) :
p.coeff 0 = () p
theorem Polynomial.coeff_zero_eq_aeval_zero' {R : Type u} {A : Type z} [] [] [Algebra R A] (p : ) :
() (p.coeff 0) = () p
theorem Polynomial.map_aeval_eq_aeval_map {R : Type u} [] {S : Type u_3} {T : Type u_4} {U : Type u_5} [] [] [] [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U} (h : ().comp φ = ψ.comp ()) (p : ) (a : S) :
ψ (() p) = (Polynomial.aeval (ψ a)) ()
theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero {S : Type v} {T : Type w} [] [] [Algebra S T] {p : } {q : } (h₁ : p q) {a : T} (h₂ : () p = 0) :
() q = 0
theorem Algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type z} [] [] [Algebra R A] (x : A) :
@[simp]
theorem Polynomial.aeval_mem_adjoin_singleton (R : Type u) {A : Type z} [] [] [Algebra R A] {p : } (x : A) :
instance Polynomial.instCommSemiringAdjoinSingleton (R : Type u) {A : Type z} [] [] [Algebra R A] (x : A) :
Equations
instance Polynomial.instCommRingAdjoinSingleton {R : Type u_3} {A : Type u_4} [] [Ring A] [Algebra R A] (x : A) :
Equations
theorem Polynomial.aeval_eq_sum_range {R : Type u} {S : Type v} [] [] [Algebra R S] {p : } (x : S) :
() p = (Finset.range (p.natDegree + 1)).sum fun (i : ) => p.coeff i x ^ i
theorem Polynomial.aeval_eq_sum_range' {R : Type u} {S : Type v} [] [] [Algebra R S] {p : } {n : } (hn : p.natDegree < n) (x : S) :
() p = ().sum fun (i : ) => p.coeff i x ^ i
theorem Polynomial.isRoot_of_eval₂_map_eq_zero {R : Type u} {S : Type v} [] {p : } [] {f : R →+* S} (hf : ) {r : R} :
Polynomial.eval₂ f (f r) p = 0p.IsRoot r
theorem Polynomial.isRoot_of_aeval_algebraMap_eq_zero {R : Type u} {S : Type v} [] [] [Algebra R S] {p : } (inj : Function.Injective ()) {r : R} (hr : (Polynomial.aeval (() r)) p = 0) :
p.IsRoot r
def Polynomial.aevalTower {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (f : R →ₐ[S] A') (x : A') :

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

Equations
Instances For
@[simp]
theorem Polynomial.aevalTower_X {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
() Polynomial.X = y
@[simp]
theorem Polynomial.aevalTower_C {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :
() (Polynomial.C x) = g x
@[simp]
theorem Polynomial.aevalTower_comp_C {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
(()).comp Polynomial.C = g
theorem Polynomial.aevalTower_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :
() ((algebraMap R ()) x) = g x
theorem Polynomial.aevalTower_comp_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
(()).comp (algebraMap R ()) = g
theorem Polynomial.aevalTower_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :
() (() x) = g x
@[simp]
theorem Polynomial.aevalTower_comp_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [] [] [] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
().comp () = g
@[simp]
theorem Polynomial.aevalTower_id {S : Type v} [] :
= Polynomial.aeval
@[simp]
theorem Polynomial.aevalTower_ofId {S : Type v} {A' : Type u_1} [] [] [Algebra S A'] :
= Polynomial.aeval
theorem Polynomial.dvd_term_of_dvd_eval_of_dvd_terms {S : Type v} [] {z : S} {p : S} {f : } (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_isRoot_of_dvd_terms {S : Type v} [] {r : S} {p : S} {f : } (i : ) (hr : f.IsRoot 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 : } (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.not_isUnit_X_sub_C {R : Type u} [Ring R] [] (r : R) :
¬IsUnit (Polynomial.X - Polynomial.C r)
theorem Polynomial.aeval_endomorphism {R : Type u} {M : Type u_3} [] [] [Module R M] (f : M →ₗ[R] M) (v : M) (p : ) :
(() p) v = p.sum fun (n : ) (b : R) => b (f ^ n) v
theorem Polynomial.aeval_apply_smul_mem_of_le_comap' {R : Type u} {A : Type z} {M : Type u_3} [] [] [Module R M] {q : } {m : M} (hm : m q) (p : ) [] [Algebra R A] [Module A M] [] (a : A) (hq : q Submodule.comap (() a) q) :
() p m q
theorem Polynomial.aeval_apply_smul_mem_of_le_comap {R : Type u} {M : Type u_3} [] [] [Module R M] {q : } {m : M} (hm : m q) (p : ) (f : ) (hq : q ) :
(() p) m q