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.

source

instance Polynomial.algebraOfAlgebra {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] :

Algebra R (Polynomial A)

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

source

theorem Polynomial.algebraMap_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :

↑(algebraMap R (Polynomial A)) r = ↑Polynomial.C (↑(algebraMap R A) r)

source

@[simp]

theorem Polynomial.toFinsupp_algebraMap {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :

(↑(algebraMap R (Polynomial A)) r).toFinsupp = ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r

source

theorem Polynomial.ofFinsupp_algebraMap {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :

{ toFinsupp := ↑(algebraMap R (AddMonoidAlgebra A ℕ)) r } = ↑(algebraMap R (Polynomial A)) r

source

theorem Polynomial.C_eq_algebraMap {R : Type u} [CommSemiring R] (r : R) :

↑Polynomial.C r = ↑(algebraMap R (Polynomial 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.)

source

theorem Polynomial.algHom_ext' {R : Type u} {A' : Type u_1} {B' : Type u_2} [CommSemiring A'] [Semiring B'] [CommSemiring R] [Algebra R A'] [Algebra R B'] {f : Polynomial A' →ₐ[R] B'} {g : Polynomial A' →ₐ[R] B'} (h₁ : AlgHom.comp f (IsScalarTower.toAlgHom R A' (Polynomial A')) = AlgHom.comp g (IsScalarTower.toAlgHom R A' (Polynomial A'))) (h₂ : ↑f Polynomial.X = ↑g Polynomial.X) :

f = g

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

source

@[simp]

theorem Polynomial.toFinsuppIsoAlg_apply (R : Type u) [CommSemiring R] (self : Polynomial R) :

↑(Polynomial.toFinsuppIsoAlg R) self = self.toFinsupp

source

@[simp]

theorem Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp (R : Type u) [CommSemiring R] (toFinsupp : AddMonoidAlgebra R ℕ) :

(↑(AlgEquiv.symm (Polynomial.toFinsuppIsoAlg R)) toFinsupp).toFinsupp = toFinsupp

source

def Polynomial.toFinsuppIsoAlg (R : Type u) [CommSemiring R] :

Polynomial R ≃ₐ[R] AddMonoidAlgebra R ℕ

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.

Instances For

source

instance Polynomial.subalgebraNontrivial {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] [Nontrivial A] :

Nontrivial (Subalgebra R (Polynomial A))

source

@[simp]

theorem Polynomial.algHom_eval₂_algebraMap {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (p : Polynomial R) (f : A →ₐ[R] B) (a : A) :

↑f (Polynomial.eval₂ (algebraMap R A) a p) = Polynomial.eval₂ (algebraMap R B) (↑f a) p

source

@[simp]

theorem Polynomial.eval₂_algebraMap_X {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (f : Polynomial R →ₐ[R] A) :

Polynomial.eval₂ (algebraMap R A) (↑f Polynomial.X) p = ↑f p

source

@[simp]

theorem Polynomial.ringHom_eval₂_cast_int_ringHom {R : Type u_3} {S : Type u_4} [Ring R] [Ring S] (p : Polynomial ℤ) (f : R →+* S) (r : R) :

↑f (Polynomial.eval₂ (Int.castRingHom R) r p) = Polynomial.eval₂ (Int.castRingHom S) (↑f r) p

source

@[simp]

theorem Polynomial.eval₂_int_castRingHom_X {R : Type u_3} [Ring R] (p : Polynomial ℤ) (f : Polynomial ℤ →+* R) :

Polynomial.eval₂ (Int.castRingHom R) (↑f Polynomial.X) p = ↑f p

source

def Polynomial.aeval {R : Type u} {A : Type z} [CommSemiring 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.

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

Instances For

source

@[simp]

theorem Polynomial.adjoin_X {R : Type u} [CommSemiring R] :

Algebra.adjoin R {Polynomial.X} = ⊤

source

theorem Polynomial.algHom_ext {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {f : Polynomial R →ₐ[R] A} {g : Polynomial R →ₐ[R] A} (h : ↑f Polynomial.X = ↑g Polynomial.X) :

f = g

source

theorem Polynomial.aeval_def {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (p : Polynomial R) :

↑(Polynomial.aeval x) p = Polynomial.eval₂ (algebraMap R A) x p

source

theorem Polynomial.aeval_zero {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) 0 = 0

source

@[simp]

theorem Polynomial.aeval_X {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) Polynomial.X = x

source

@[simp]

theorem Polynomial.aeval_C {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) :

↑(Polynomial.aeval x) (↑Polynomial.C r) = ↑(algebraMap R A) r

source

@[simp]

theorem Polynomial.aeval_monomial {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} {r : R} :

↑(Polynomial.aeval x) (↑(Polynomial.monomial n) r) = ↑(algebraMap R A) r * x ^ n

source

theorem Polynomial.aeval_X_pow {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} :

↑(Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n

source

theorem Polynomial.aeval_add {R : Type u} {A : Type z} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) (p + q) = ↑(Polynomial.aeval x) p + ↑(Polynomial.aeval x) q

source

theorem Polynomial.aeval_one {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) 1 = 1

source

@[deprecated]

theorem Polynomial.aeval_bit0 {R : Type u} {A : Type z} [CommSemiring R] {p : Polynomial R} [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) (bit0 p) = bit0 (↑(Polynomial.aeval x) p)

source

@[deprecated]

theorem Polynomial.aeval_bit1 {R : Type u} {A : Type z} [CommSemiring R] {p : Polynomial R} [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) (bit1 p) = bit1 (↑(Polynomial.aeval x) p)

source

theorem Polynomial.aeval_nat_cast {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (n : ℕ) :

↑(Polynomial.aeval x) ↑n = ↑n

source

theorem Polynomial.aeval_mul {R : Type u} {A : Type z} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} [Semiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) (p * q) = ↑(Polynomial.aeval x) p * ↑(Polynomial.aeval x) q

source

theorem Polynomial.aeval_comp {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} {A : Type u_4} [CommSemiring A] [Algebra R A] (x : A) :

↑(Polynomial.aeval x) (Polynomial.comp p q) = ↑(Polynomial.aeval (↑(Polynomial.aeval x) q)) p

source

theorem Polynomial.aeval_algHom {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {B : Type u_3} [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (x : A) :

Polynomial.aeval (↑f x) = AlgHom.comp f (Polynomial.aeval x)

source

@[simp]

theorem Polynomial.aeval_X_left {R : Type u} [CommSemiring R] :

Polynomial.aeval Polynomial.X = AlgHom.id R (Polynomial R)

source

theorem Polynomial.aeval_X_left_apply {R : Type u} [CommSemiring R] (p : Polynomial R) :

↑(Polynomial.aeval Polynomial.X) p = p

source

theorem Polynomial.eval_unique {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (φ : Polynomial R →ₐ[R] A) (p : Polynomial R) :

↑φ p = Polynomial.eval₂ (algebraMap R A) (↑φ Polynomial.X) p

source

theorem Polynomial.aeval_algHom_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {B : Type u_3} [Semiring B] [Algebra R B] {F : Type u_4} [AlgHomClass F R A B] (f : F) (x : A) (p : Polynomial R) :

↑(Polynomial.aeval (↑f x)) p = ↑f (↑(Polynomial.aeval x) p)

source

theorem Polynomial.aeval_algEquiv {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {B : Type u_3} [Semiring B] [Algebra R B] (f : A ≃ₐ[R] B) (x : A) :

Polynomial.aeval (↑f x) = AlgHom.comp (↑f) (Polynomial.aeval x)

source

theorem Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : R) (p : Polynomial R) :

↑(Polynomial.aeval (↑(algebraMap R A) x)) p = ↑(algebraMap R A) (Polynomial.eval x p)

source

@[simp]

theorem Polynomial.coe_aeval_eq_eval {R : Type u} [CommSemiring R] (r : R) :

↑(Polynomial.aeval r) = Polynomial.eval r

source

@[simp]

theorem Polynomial.coe_aeval_eq_evalRingHom {R : Type u} [CommSemiring R] (x : R) :

↑(Polynomial.aeval x) = Polynomial.evalRingHom x

source

@[simp]

theorem Polynomial.aeval_fn_apply {R : Type u} [CommSemiring R] {X : Type u_4} (g : Polynomial R) (f : X → R) (x : X) :

↑(Polynomial.aeval f) g x = ↑(Polynomial.aeval (f x)) g

source

theorem Polynomial.aeval_subalgebra_coe {R : Type u} [CommSemiring R] (g : Polynomial R) {A : Type u_4} [Semiring A] [Algebra R A] (s : Subalgebra R A) (f : { x // x ∈ s }) :

↑(↑(Polynomial.aeval f) g) = ↑(Polynomial.aeval ↑f) g

source

theorem Polynomial.coeff_zero_eq_aeval_zero {R : Type u} [CommSemiring R] (p : Polynomial R) :

Polynomial.coeff p 0 = ↑(Polynomial.aeval 0) p

source

theorem Polynomial.coeff_zero_eq_aeval_zero' {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) :

↑(algebraMap R A) (Polynomial.coeff p 0) = ↑(Polynomial.aeval 0) p

source

theorem Polynomial.map_aeval_eq_aeval_map {R : Type u} [CommSemiring R] {S : Type u_4} {T : Type u_5} {U : Type u_6} [CommSemiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U} (h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)) (p : Polynomial R) (a : S) :

↑ψ (↑(Polynomial.aeval a) p) = ↑(Polynomial.aeval (↑ψ a)) (Polynomial.map φ p)

source

theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero {S : Type v} {T : Type w} [CommSemiring S] [CommSemiring T] [Algebra S T] {p : Polynomial S} {q : Polynomial S} (h₁ : p ∣ q) {a : T} (h₂ : ↑(Polynomial.aeval a) p = 0) :

↑(Polynomial.aeval a) q = 0

source

theorem Algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :

Algebra.adjoin R {x} = AlgHom.range (Polynomial.aeval x)

source

theorem Polynomial.aeval_eq_sum_range {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (x : S) :

↑(Polynomial.aeval x) p = Finset.sum (Finset.range (Polynomial.natDegree p + 1)) fun i => Polynomial.coeff p i • x ^ i

source

theorem Polynomial.aeval_eq_sum_range' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} {n : ℕ} (hn : Polynomial.natDegree p < n) (x : S) :

↑(Polynomial.aeval x) p = Finset.sum (Finset.range n) fun i => Polynomial.coeff p i • x ^ i

source

theorem Polynomial.isRoot_of_eval₂_map_eq_zero {R : Type u} {S : Type v} [CommSemiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ↑f) {r : R} :

Polynomial.eval₂ f (↑f r) p = 0 → Polynomial.IsRoot p r

source

theorem Polynomial.isRoot_of_aeval_algebraMap_eq_zero {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (inj : Function.Injective ↑(algebraMap R S)) {r : R} (hr : ↑(Polynomial.aeval (↑(algebraMap R S) r)) p = 0) :

Polynomial.IsRoot p r

source

def Polynomial.aevalTower {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (f : R →ₐ[S] A') (x : A') :

Polynomial R →ₐ[S] A'

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

Instances For

source

@[simp]

theorem Polynomial.aevalTower_X {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :

↑(Polynomial.aevalTower g y) Polynomial.X = y

source

@[simp]

theorem Polynomial.aevalTower_C {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :

↑(Polynomial.aevalTower g y) (↑Polynomial.C x) = ↑g x

source

@[simp]

theorem Polynomial.aevalTower_comp_C {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :

RingHom.comp (↑(Polynomial.aevalTower g y)) Polynomial.C = ↑g

source

@[simp]

theorem Polynomial.aevalTower_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :

↑(Polynomial.aevalTower g y) (↑(algebraMap R (Polynomial R)) x) = ↑g x

source

@[simp]

theorem Polynomial.aevalTower_comp_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :

RingHom.comp (↑(Polynomial.aevalTower g y)) (algebraMap R (Polynomial R)) = ↑g

source

theorem Polynomial.aevalTower_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :

↑(Polynomial.aevalTower g y) (↑(IsScalarTower.toAlgHom S R (Polynomial R)) x) = ↑g x

source

@[simp]

theorem Polynomial.aevalTower_comp_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring R] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :

AlgHom.comp (Polynomial.aevalTower g y) (IsScalarTower.toAlgHom S R (Polynomial R)) = g

source

@[simp]

theorem Polynomial.aevalTower_id {S : Type v} [CommSemiring S] :

Polynomial.aevalTower (AlgHom.id S S) = Polynomial.aeval

source

@[simp]

theorem Polynomial.aevalTower_ofId {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring S] [Algebra S A'] :

Polynomial.aevalTower (Algebra.ofId S A') = Polynomial.aeval

source

theorem Polynomial.dvd_term_of_dvd_eval_of_dvd_terms {S : Type v} [CommRing S] {z : S} {p : S} {f : Polynomial S} (i : ℕ) (dvd_eval : p ∣ Polynomial.eval z f) (dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ Polynomial.coeff f j * z ^ j) :

p ∣ Polynomial.coeff f i * z ^ i

source

theorem Polynomial.dvd_term_of_isRoot_of_dvd_terms {S : Type v} [CommRing S] {r : S} {p : S} {f : Polynomial S} (i : ℕ) (hr : Polynomial.IsRoot f r) (h : ∀ (j : ℕ), j ≠ i → p ∣ Polynomial.coeff f j * r ^ j) :

p ∣ Polynomial.coeff f i * r ^ i

source

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.

source

theorem Polynomial.not_isUnit_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (r : R) :

¬IsUnit (Polynomial.X - ↑Polynomial.C r)

source

theorem Polynomial.aeval_endomorphism {R : Type u} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) (p : Polynomial R) :

↑(↑(Polynomial.aeval f) p) v = Polynomial.sum p fun n b => b • ↑(f ^ n) v