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}
[comm_semiring R]
[semiring A]
[algebra R A] :
Note that this instance also provides algebra R R[X].
Equations
theorem
polynomial.algebra_map_apply
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
⇑(algebra_map R A[X]) r = ⇑polynomial.C (⇑(algebra_map R A) r)
@[simp]
theorem
polynomial.to_finsupp_algebra_map
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
(⇑(algebra_map R A[X]) r).to_finsupp = ⇑(algebra_map R (add_monoid_algebra A ℕ)) r
theorem
polynomial.of_finsupp_algebra_map
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(r : R) :
{to_finsupp := ⇑(algebra_map R (add_monoid_algebra A ℕ)) r} = ⇑(algebra_map R A[X]) r
theorem
polynomial.C_eq_algebra_map
{R : Type u}
[comm_semiring R]
(r : R) :
⇑polynomial.C r = ⇑(algebra_map R R[X]) r
When we have [comm_ring 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']
[comm_semiring R]
[algebra R A']
[algebra R B']
{f g : A'[X] →ₐ[R] B'}
(h₁ : f.comp (is_scalar_tower.to_alg_hom R A' A'[X]) = g.comp (is_scalar_tower.to_alg_hom R A' A'[X]))
(h₂ : ⇑f polynomial.X = ⇑g polynomial.X) :
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)
[comm_semiring R]
(ᾰ : add_monoid_algebra R ℕ) :
⇑((polynomial.to_finsupp_iso_alg R).symm) ᾰ = (polynomial.to_finsupp_iso R).inv_fun ᾰ
@[simp]
noncomputable
def
polynomial.to_finsupp_iso_alg
(R : Type u)
[comm_semiring R] :
R[X] ≃ₐ[R] add_monoid_algebra R ℕ
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
- polynomial.to_finsupp_iso_alg R = {to_fun := (polynomial.to_finsupp_iso R).to_fun, inv_fun := (polynomial.to_finsupp_iso R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[protected, instance]
def
polynomial.subalgebra.nontrivial
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
[nontrivial A] :
nontrivial (subalgebra R A[X])
@[simp]
theorem
polynomial.alg_hom_eval₂_algebra_map
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(p : R[X])
(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_semiring R]
[semiring A]
[algebra R A]
(p : R[X])
(f : R[X] →ₐ[R] A) :
polynomial.eval₂ (algebra_map R A) (⇑f polynomial.X) 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 : ℤ[X])
(f : R →+* S)
(r : R) :
⇑f (polynomial.eval₂ (int.cast_ring_hom R) r p) = polynomial.eval₂ (int.cast_ring_hom S) (⇑f r) p
@[simp]
theorem
polynomial.eval₂_int_cast_ring_hom_X
{R : Type u_1}
[ring R]
(p : ℤ[X])
(f : ℤ[X] →+* R) :
polynomial.eval₂ (int.cast_ring_hom R) (⇑f polynomial.X) p = ⇑f p
noncomputable
def
polynomial.aeval
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[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
- 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' := _}
@[simp]
@[ext]
theorem
polynomial.alg_hom_ext
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
{f g : R[X] →ₐ[R] A}
(h : ⇑f polynomial.X = ⇑g polynomial.X) :
f = g
theorem
polynomial.aeval_def
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
(p : R[X]) :
⇑(polynomial.aeval x) p = polynomial.eval₂ (algebra_map R A) x p
@[simp]
theorem
polynomial.aeval_zero
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) 0 = 0
@[simp]
theorem
polynomial.aeval_X
{R : Type u}
{A : Type z}
[comm_semiring R]
[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]
[semiring A]
[algebra R A]
(x : A)
(r : R) :
⇑(polynomial.aeval x) (⇑polynomial.C r) = ⇑(algebra_map R A) r
@[simp]
theorem
polynomial.aeval_monomial
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
{n : ℕ}
{r : R} :
⇑(polynomial.aeval x) (⇑(polynomial.monomial n) r) = (⇑(algebra_map R A) r) * x ^ n
@[simp]
theorem
polynomial.aeval_X_pow
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
{n : ℕ} :
⇑(polynomial.aeval x) (polynomial.X ^ n) = x ^ n
@[simp]
theorem
polynomial.aeval_add
{R : Type u}
{A : Type z}
[comm_semiring R]
{p q : R[X]}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (p + q) = ⇑(polynomial.aeval x) p + ⇑(polynomial.aeval x) q
@[simp]
theorem
polynomial.aeval_one
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) 1 = 1
@[simp]
theorem
polynomial.aeval_bit0
{R : Type u}
{A : Type z}
[comm_semiring R]
{p : R[X]}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (bit0 p) = bit0 (⇑(polynomial.aeval x) p)
@[simp]
theorem
polynomial.aeval_bit1
{R : Type u}
{A : Type z}
[comm_semiring R]
{p : R[X]}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (bit1 p) = bit1 (⇑(polynomial.aeval x) p)
@[simp]
theorem
polynomial.aeval_nat_cast
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A)
(n : ℕ) :
⇑(polynomial.aeval x) ↑n = ↑n
theorem
polynomial.aeval_mul
{R : Type u}
{A : Type z}
[comm_semiring R]
{p q : R[X]}
[semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (p * q) = (⇑(polynomial.aeval x) p) * ⇑(polynomial.aeval x) q
theorem
polynomial.aeval_comp
{R : Type u}
[comm_semiring R]
{p q : R[X]}
{A : Type u_1}
[comm_semiring A]
[algebra R A]
(x : A) :
⇑(polynomial.aeval x) (p.comp q) = ⇑(polynomial.aeval (⇑(polynomial.aeval x) q)) p
@[simp]
theorem
polynomial.aeval_map
{R : Type u}
[comm_semiring R]
{B : Type u_3}
[semiring B]
[algebra R B]
{A : Type u_1}
[comm_semiring A]
[algebra R A]
[algebra A B]
[is_scalar_tower R A B]
(b : B)
(p : R[X]) :
⇑(polynomial.aeval b) (polynomial.map (algebra_map R A) p) = ⇑(polynomial.aeval b) p
theorem
polynomial.aeval_alg_hom
{R : Type u}
{A : Type z}
[comm_semiring 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) = f.comp (polynomial.aeval x)
@[simp]
theorem
polynomial.eval_unique
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(φ : R[X] →ₐ[R] A)
(p : R[X]) :
⇑φ p = polynomial.eval₂ (algebra_map R A) (⇑φ polynomial.X) p
theorem
polynomial.aeval_alg_hom_apply
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
{B : Type u_3}
[semiring B]
[algebra R B]
(f : A →ₐ[R] B)
(x : A)
(p : R[X]) :
⇑(polynomial.aeval (⇑f x)) p = ⇑f (⇑(polynomial.aeval x) p)
theorem
polynomial.aeval_alg_equiv
{R : Type u}
{A : Type z}
[comm_semiring 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) = ↑f.comp (polynomial.aeval x)
theorem
polynomial.aeval_alg_equiv_apply
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
{B : Type u_3}
[semiring B]
[algebra R B]
(f : A ≃ₐ[R] B)
(x : A)
(p : R[X]) :
⇑(polynomial.aeval (⇑f x)) p = ⇑f (⇑(polynomial.aeval x) p)
theorem
polynomial.aeval_algebra_map_apply
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : R)
(p : R[X]) :
⇑(polynomial.aeval (⇑(algebra_map R A) x)) p = ⇑(algebra_map R A) (polynomial.eval x p)
@[simp]
@[simp]
theorem
polynomial.aeval_fn_apply
{R : Type u}
[comm_semiring R]
{X : Type u_1}
(g : R[X])
(f : X → R)
(x : X) :
⇑(polynomial.aeval f) g x = ⇑(polynomial.aeval (f x)) g
@[norm_cast]
theorem
polynomial.aeval_subalgebra_coe
{R : Type u}
[comm_semiring R]
(g : R[X])
{A : Type u_1}
[semiring A]
[algebra R A]
(s : subalgebra R A)
(f : ↥s) :
↑(⇑(polynomial.aeval f) g) = ⇑(polynomial.aeval ↑f) g
theorem
polynomial.coeff_zero_eq_aeval_zero
{R : Type u}
[comm_semiring R]
(p : R[X]) :
p.coeff 0 = ⇑(polynomial.aeval 0) p
theorem
polynomial.coeff_zero_eq_aeval_zero'
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(p : R[X]) :
⇑(algebra_map R A) (p.coeff 0) = ⇑(polynomial.aeval 0) p
theorem
algebra.adjoin_singleton_eq_range_aeval
(R : Type u)
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
algebra.adjoin R {x} = (polynomial.aeval x).range
theorem
polynomial.aeval_eq_sum_range
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
[algebra R S]
{p : R[X]}
(x : S) :
⇑(polynomial.aeval x) p = ∑ (i : ℕ) in finset.range (p.nat_degree + 1), p.coeff i • x ^ i
theorem
polynomial.aeval_eq_sum_range'
{R : Type u}
{S : Type v}
[comm_semiring R]
[comm_semiring S]
[algebra R S]
{p : R[X]}
{n : ℕ}
(hn : p.nat_degree < n)
(x : S) :
⇑(polynomial.aeval x) p = ∑ (i : ℕ) in finset.range n, p.coeff i • x ^ i
theorem
polynomial.is_root_of_eval₂_map_eq_zero
{R : Type u}
{S : Type v}
[comm_semiring R]
{p : R[X]}
[comm_semiring 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_semiring S]
[algebra R S]
{p : R[X]}
(inj : function.injective ⇑(algebra_map R S))
{r : R}
(hr : ⇑(polynomial.aeval (⇑(algebra_map R S) r)) p = 0) :
p.is_root r
noncomputable
def
polynomial.aeval_tower
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S 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.
@[simp]
theorem
polynomial.aeval_tower_X
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A') :
⇑(polynomial.aeval_tower g y) polynomial.X = y
@[simp]
theorem
polynomial.aeval_tower_C
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A')
(x : R) :
⇑(polynomial.aeval_tower g y) (⇑polynomial.C x) = ⇑g x
@[simp]
theorem
polynomial.aeval_tower_comp_C
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A') :
↑(polynomial.aeval_tower g y).comp polynomial.C = ↑g
@[simp]
theorem
polynomial.aeval_tower_algebra_map
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A')
(x : R) :
⇑(polynomial.aeval_tower g y) (⇑(algebra_map R R[X]) x) = ⇑g x
@[simp]
theorem
polynomial.aeval_tower_comp_algebra_map
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A') :
↑(polynomial.aeval_tower g y).comp (algebra_map R R[X]) = ↑g
theorem
polynomial.aeval_tower_to_alg_hom
{R : Type u}
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A')
(x : R) :
⇑(polynomial.aeval_tower g y) (⇑(is_scalar_tower.to_alg_hom S R R[X]) 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']
[comm_semiring R]
[comm_semiring S]
[algebra S R]
[algebra S A']
(g : R →ₐ[S] A')
(y : A') :
(polynomial.aeval_tower g y).comp (is_scalar_tower.to_alg_hom S R R[X]) = g
@[simp]
@[simp]
theorem
polynomial.aeval_tower_of_id
{S : Type v}
{A' : Type u_1}
[comm_semiring A']
[comm_semiring S]
[algebra S A'] :
theorem
polynomial.eval_mul_X_sub_C
{R : Type u}
[ring R]
{p : R[X]}
(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.