Theory of univariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We show that A[X] 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] :
algebra R (polynomial 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 (polynomial A)) 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 (polynomial A)) 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 (polynomial A)) r
theorem
polynomial.C_eq_algebra_map
{R : Type u}
[comm_semiring R]
(r : R) :
⇑polynomial.C r = ⇑(algebra_map 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']
[comm_semiring R]
[algebra R A']
[algebra R B']
{f g : polynomial A' →ₐ[R] B'}
(h₁ : f.comp (is_scalar_tower.to_alg_hom R A' (polynomial A')) = g.comp (is_scalar_tower.to_alg_hom 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'
@[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]
Algebra isomorphism between R[X] 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 (polynomial A))
@[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 : polynomial R)
(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 : polynomial R)
(f : polynomial R →ₐ[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 : polynomial ℤ)
(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 : polynomial ℤ)
(f : polynomial ℤ →+* 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) :
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.
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 : polynomial R →ₐ[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 : polynomial R) :
⇑(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 : polynomial R}
[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 : polynomial R}
[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 : polynomial R}
[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 : polynomial R}
[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 : polynomial R}
{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
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.aeval_X_left_apply
{R : Type u}
[comm_semiring R]
(p : polynomial R) :
⇑(polynomial.aeval polynomial.X) p = p
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) :
⇑φ 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 : Type u_1}
[alg_hom_class F R A B]
(f : F)
(x : A)
(p : polynomial R) :
⇑(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_algebra_map_apply_eq_algebra_map_eval
{R : Type u}
{A : Type z}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : R)
(p : polynomial R) :
⇑(polynomial.aeval (⇑(algebra_map R A) x)) p = ⇑(algebra_map R A) (polynomial.eval x p)
@[simp]
@[simp]
@[simp]
theorem
polynomial.aeval_fn_apply
{R : Type u}
[comm_semiring R]
{X : Type u_1}
(g : polynomial R)
(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 : polynomial R)
{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 : polynomial R) :
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 : polynomial R) :
⇑(algebra_map R A) (p.coeff 0) = ⇑(polynomial.aeval 0) p
theorem
polynomial.map_aeval_eq_aeval_map
{R : Type u}
[comm_semiring R]
{S : Type u_1}
{T : Type u_2}
{U : Type u_3}
[comm_semiring S]
[comm_semiring T]
[semiring U]
[algebra R S]
[algebra T U]
{φ : R →+* T}
{ψ : S →+* U}
(h : (algebra_map T U).comp φ = ψ.comp (algebra_map R S))
(p : polynomial R)
(a : S) :
⇑ψ (⇑(polynomial.aeval a) p) = ⇑(polynomial.aeval (⇑ψ a)) (polynomial.map φ p)
theorem
polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero
{S : Type v}
{T : Type w}
[comm_semiring S]
[comm_semiring T]
[algebra S T]
{p q : polynomial S}
(h₁ : p ∣ q)
{a : T}
(h₂ : ⇑(polynomial.aeval a) p = 0) :
⇑(polynomial.aeval a) q = 0
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]
[semiring S]
[algebra R S]
{p : polynomial R}
(x : S) :
⇑(polynomial.aeval x) 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}
[comm_semiring R]
[semiring S]
[algebra R S]
{p : polynomial R}
{n : ℕ}
(hn : p.nat_degree < n)
(x : S) :
⇑(polynomial.aeval x) 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}
[comm_semiring R]
{p : polynomial R}
[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]
[semiring S]
[algebra R S]
{p : polynomial R}
(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') :
polynomial R →ₐ[S] A'
Version of aeval for defining algebra homs out of R[X] 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 (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']
[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 (polynomial R)) = ↑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 (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']
[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 (polynomial R)) = 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 : 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.
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) :