Ring-theoretic supplement of Algebra.Polynomial.

Main results

• MvPolynomial.isDomain: If a ring is an integral domain, then so is its polynomial ring over finitely many variables.
• Polynomial.isNoetherianRing: Hilbert basis theorem, that if a ring is Noetherian then so is its polynomial ring.

instance Polynomial.instCharP {R : Type u} [Semiring R] (p : ℕ) [h : CharP R p] : CharP (Polynomial R) p

instance Polynomial.instExpChar {R : Type u} [Semiring R] (p : ℕ) [h : ExpChar R p] : ExpChar (Polynomial R) p

def Polynomial.degreeLE (R : Type u) [Semiring R] (n : WithBot ℕ) : Submodule R (Polynomial R)

The R-submodule of R[X] consisting of polynomials of degree ≤ n.

def Polynomial.degreeLT (R : Type u) [Semiring R] (n : ℕ) : Submodule R (Polynomial R)

The R-submodule of R[X] consisting of polynomials of degree < n.

theorem Polynomial.mem_degreeLE {R : Type u} [Semiring R] {n : WithBot ℕ} {f : Polynomial R} : f ∈ degreeLE R n ↔ f.degree ≤ n

theorem Polynomial.degreeLE_mono {R : Type u} [Semiring R] {m n : WithBot ℕ} (H : m ≤ n) : degreeLE R m ≤ degreeLE R n

theorem Polynomial.degreeLE_eq_span_X_pow {R : Type u} [Semiring R] [DecidableEq R] {n : ℕ} : degreeLE R ↑n = Submodule.span R ↑(Finset.image (fun (n : ℕ) => X ^ n) (Finset.range (n + 1)))

theorem Polynomial.mem_degreeLT {R : Type u} [Semiring R] {n : ℕ} {f : Polynomial R} : f ∈ degreeLT R n ↔ f.degree < ↑n

theorem Polynomial.degreeLT_mono {R : Type u} [Semiring R] {m n : ℕ} (H : m ≤ n) : degreeLT R m ≤ degreeLT R n

theorem Polynomial.degreeLT_eq_span_X_pow {R : Type u} [Semiring R] [DecidableEq R] {n : ℕ} : degreeLT R n = Submodule.span R ↑(Finset.image (fun (n : ℕ) => X ^ n) (Finset.range n))

def Polynomial.degreeLTEquiv (R : Type u_2) [Semiring R] (n : ℕ) : ↥(degreeLT R n) ≃ₗ[R] Fin n → R

The first n coefficients on degreeLT n form a linear equivalence with Fin n → R.

theorem Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero {R : Type u} [Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ degreeLT R n) : (degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0

theorem Polynomial.eval_eq_sum_degreeLTEquiv {R : Type u} [Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ degreeLT R n) (x : R) : eval x p = ∑ i : Fin n, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

theorem Polynomial.degreeLT_succ_eq_degreeLE {R : Type u} [Semiring R] {n : ℕ} : degreeLT R (n + 1) = degreeLE R ↑n

def Polynomial.monicEquivDegreeLT {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : { p : Polynomial R // p.Monic ∧ p.natDegree = n } ≃ ↥(degreeLT R n)

The equivalence between monic polynomials of degree n and polynomials of degree less than n, formed by adding a term X ^ n.

theorem Polynomial.exists_degree_le_of_mem_span {R : Type u} [Semiring R] {s : Set (Polynomial R)} {p : Polynomial R} (hs : s.Nonempty) (hp : p ∈ Submodule.span R s) : ∃ p' ∈ s, p.degree ≤ p'.degree

For every polynomial p in the span of a set s : Set R[X], there exists a polynomial of p' ∈ s with higher degree. See also Polynomial.exists_degree_le_of_mem_span_of_finite.

theorem Polynomial.exists_degree_le_of_mem_span_of_finite {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) (hs : s.Nonempty) : ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree

A stronger version of Polynomial.exists_degree_le_of_mem_span under the assumption that the set s : R[X] is finite. There exists a polynomial p' ∈ s whose degree dominates the degree of every element of p ∈ span R s.

theorem Polynomial.span_le_degreeLE_of_finite {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) : ∃ (n : ℕ), Submodule.span R s ≤ degreeLE R ↑n

The span of every finite set of polynomials is contained in a degreeLE n for some n.

theorem Polynomial.span_of_finite_le_degreeLT {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) : ∃ (n : ℕ), Submodule.span R s ≤ degreeLT R n

The span of every finite set of polynomials is contained in a degreeLT n for some n.

theorem Polynomial.not_finite {R : Type u} [Semiring R] [Nontrivial R] : ¬Module.Finite R (Polynomial R)

If R is a nontrivial ring, the polynomials R[X] are not finite as an R-module. When R is a field, this is equivalent to R[X] being an infinite-dimensional vector space over R.

theorem Polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [Semiring R] (n : ℕ) : (∑ i ∈ Finset.range n, X ^ i).comp (X + 1) = ∑ i ∈ Finset.range n, ↑(n.choose (i + 1)) * X ^ i

theorem Polynomial.Monic.geom_sum {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic

theorem Polynomial.Monic.geom_sum' {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic

theorem Polynomial.monic_geom_sum_X {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, X ^ i).Monic

def Polynomial.restriction {R : Type u} [Ring R] (p : Polynomial R) : Polynomial ↥(Subring.closure ↑p.coeffs)

Given a polynomial, return the polynomial whose coefficients are in the ring closure of the original coefficients.

@[simp]

theorem Polynomial.coeff_restriction {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} : ↑(p.restriction.coeff n) = p.coeff n

theorem Polynomial.coeff_restriction' {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} : ↑(p.restriction.coeff n) = p.coeff n

@[simp]

theorem Polynomial.support_restriction {R : Type u} [Ring R] (p : Polynomial R) : p.restriction.support = p.support

@[simp]

theorem Polynomial.map_restriction {R : Type u} [CommRing R] (p : Polynomial R) : map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction = p

@[simp]

theorem Polynomial.degree_restriction {R : Type u} [Ring R] {p : Polynomial R} : p.restriction.degree = p.degree

@[simp]

theorem Polynomial.natDegree_restriction {R : Type u} [Ring R] {p : Polynomial R} : p.restriction.natDegree = p.natDegree

@[simp]

theorem Polynomial.monic_restriction {R : Type u} [Ring R] {p : Polynomial R} : p.restriction.Monic ↔ p.Monic

@[simp]

theorem Polynomial.restriction_zero {R : Type u} [Ring R] : restriction 0 = 0

@[simp]

theorem Polynomial.restriction_one {R : Type u} [Ring R] : restriction 1 = 1

theorem Polynomial.eval₂_restriction {R : Type u} {S : Type u_1} [Ring R] [Semiring S] {f : R →+* S} {x : S} {p : Polynomial R} : eval₂ f x p = eval₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction

def Ideal.ofPolynomial {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) : Submodule R (Polynomial R)

Transport an ideal of R[X] to an R-submodule of R[X].

theorem Ideal.mem_ofPolynomial {R : Type u} [Semiring R] {I : Ideal (Polynomial R)} (x : Polynomial R) : x ∈ I.ofPolynomial ↔ x ∈ I

def Ideal.degreeLE {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) (n : WithBot ℕ) : Submodule R (Polynomial R)

Given an ideal I of R[X], make the R-submodule of I consisting of polynomials of degree ≤ n.

def Ideal.leadingCoeffNth {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) (n : ℕ) : Ideal R

Given an ideal I of R[X], make the ideal in R of leading coefficients of polynomials in I with degree ≤ n.

def Ideal.leadingCoeff {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) : Ideal R

Given an ideal I in R[X], make the ideal in R of the leading coefficients in I.

theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (p : Polynomial R) (hp : ∀ (n : ℕ), p.coeff n ∈ comap Polynomial.C I) : p ∈ I

If every coefficient of a polynomial is in an ideal I, then so is the polynomial itself

theorem Ideal.mem_map_C_iff {R : Type u} [CommSemiring R] {I : Ideal R} {f : Polynomial R} : f ∈ map Polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

The push-forward of an ideal I of R to R[X] via inclusion is exactly the set of polynomials whose coefficients are in I

theorem Polynomial.ker_mapRingHom {R : Type u} {S : Type u_1} [CommSemiring R] [Semiring S] (f : R →+* S) : RingHom.ker (mapRingHom f) = Ideal.map C (RingHom.ker f)

theorem Ideal.mem_leadingCoeffNth {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (n : ℕ) (x : R) : x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

theorem Ideal.mem_leadingCoeffNth_zero {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) : x ∈ I.leadingCoeffNth 0 ↔ Polynomial.C x ∈ I

theorem Ideal.leadingCoeffNth_mono {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ I.leadingCoeffNth n

theorem Ideal.mem_leadingCoeff {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x

theorem Polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial R) (I : Ideal R) (n : ι → ℕ) (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ) : (s.prod f).coeff k ∈ I ^ (s.sum n - k)

If I is an ideal, and pᵢ is a finite family of polynomials each satisfying ∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ for some nᵢ, then p = ∏ pᵢ also satisfies ∀ k, pₖ ∈ Iⁿ⁻ᵏ with n = ∑ nᵢ.

theorem Ideal.polynomial_not_isField {R : Type u} [Ring R] : ¬IsField (Polynomial R)

R[X] is never a field for any ring R.

theorem Ideal.eq_zero_of_constant_mem_of_maximal {R : Type u} [Ring R] (hR : IsField R) (I : Ideal (Polynomial R)) [hI : I.IsMaximal] (x : R) (hx : Polynomial.C x ∈ I) : x = 0

The only constant in a maximal ideal over a field is 0.

theorem Ideal.isPrime_map_C_iff_isPrime {R : Type u} [CommRing R] (P : Ideal R) : (map Polynomial.C P).IsPrime ↔ P.IsPrime

If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].

instance Ideal.isPrime_map_C_of_isPrime {R : Type u} [CommRing R] {P : Ideal R} [P.IsPrime] : (map Polynomial.C P).IsPrime

If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].

theorem Ideal.is_fg_degreeLE {R : Type u} [CommRing R] [IsNoetherianRing R] (I : Ideal (Polynomial R)) (n : ℕ) : (I.degreeLE ↑n).FG

theorem span_le_of_C_coeff_mem {R : Type u} [Semiring R] {f : Polynomial R} {I : Ideal (Polynomial R)} (cf : ∀ (i : ℕ), Polynomial.C (f.coeff i) ∈ I) : Ideal.span {g : Polynomial R | ∃ (i : ℕ), g = Polynomial.C (f.coeff i)} ≤ I

If the coefficients of a polynomial belong to an ideal, then that ideal contains the ideal spanned by the coefficients of the polynomial.

theorem mem_span_C_coeff {R : Type u} [Semiring R] {f : Polynomial R} : f ∈ Ideal.span {g : Polynomial R | ∃ (i : ℕ), g = Polynomial.C (f.coeff i)}

theorem exists_C_coeff_notMem {R : Type u} [Semiring R] {f : Polynomial R} {I : Ideal (Polynomial R)} : f ∉ I → ∃ (i : ℕ), Polynomial.C (f.coeff i) ∉ I

theorem Polynomial.prime_C_iff {R : Type u} [CommRing R] {r : R} : Prime (C r) ↔ Prime r

instance MvPolynomial.instFiniteOfIsEmpty {ι : Type u_2} {R : Type u_3} [CommSemiring R] [IsEmpty ι] : Module.Finite R (MvPolynomial ι R)

theorem MvPolynomial.prime_C_iff {R : Type u} (σ : Type v) [CommRing R] {r : R} : Prime (C r) ↔ Prime r

theorem MvPolynomial.prime_rename_iff {R : Type u} {σ : Type v} [CommRing R] (s : Set σ) {p : MvPolynomial (↑s) R} : Prime ((rename Subtype.val) p) ↔ Prime p

instance Polynomial.isNoetherianRing {R : Type u} [CommRing R] [inst : IsNoetherianRing R] : IsNoetherianRing (Polynomial R)

Hilbert basis theorem: a polynomial ring over a Noetherian ring is a Noetherian ring.

theorem Polynomial.linearIndependent_powers_iff_aeval {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) : (LinearIndependent R fun (n : ℕ) => (f ^ n) v) ↔ ∀ (p : Polynomial R), ((aeval f) p) v = 0 → p = 0

theorem Polynomial.disjoint_ker_aeval_of_isCoprime {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p q : Polynomial R} (hpq : IsCoprime p q) : Disjoint ((aeval f) p).ker ((aeval f) q).ker

theorem Polynomial.sup_aeval_range_eq_top_of_isCoprime {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p q : Polynomial R} (hpq : IsCoprime p q) : ((aeval f) p).range ⊔ ((aeval f) q).range = ⊤

theorem Polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : M →ₗ[R] M} {p q : Polynomial R} : ((aeval f) p).ker ⊔ ((aeval f) q).ker ≤ ((aeval f) (p * q)).ker

theorem Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p q : Polynomial R} (hpq : IsCoprime p q) : ((aeval f) p).ker ⊔ ((aeval f) q).ker = ((aeval f) (p * q)).ker

theorem MvPolynomial.aeval_natDegree_le {σ : Type v} {R : Type u_2} [CommSemiring R] {m n : ℕ} (F : MvPolynomial σ R) (hF : F.totalDegree ≤ m) (f : σ → Polynomial R) (hf : ∀ (i : σ), (f i).natDegree ≤ n) : ((aeval f) F).natDegree ≤ m * n

theorem MvPolynomial.isNoetherianRing_fin_0 {R : Type u} [CommRing R] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial (Fin 0) R)

theorem MvPolynomial.isNoetherianRing_fin {R : Type u} [CommRing R] [IsNoetherianRing R] {n : ℕ} : IsNoetherianRing (MvPolynomial (Fin n) R)

instance MvPolynomial.isNoetherianRing {R : Type u} {σ : Type v} [CommRing R] [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)

The multivariate polynomial ring in finitely many variables over a Noetherian ring is itself a Noetherian ring.

theorem MvPolynomial.map_mvPolynomial_eq_eval₂ {R : Type u} {σ : Type v} [CommRing R] {S : Type u_2} [CommSemiring S] [Finite σ] (ϕ : MvPolynomial σ R →+* S) (p : MvPolynomial σ R) : ϕ p = eval₂ (ϕ.comp C) (fun (s : σ) => ϕ (X s)) p

theorem MvPolynomial.mem_ideal_of_coeff_mem_ideal {R : Type u} {σ : Type v} [CommRing R] (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R) (hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I) : p ∈ I

If every coefficient of a polynomial is in an ideal I, then so is the polynomial itself, multivariate version.

theorem MvPolynomial.mem_map_C_iff {R : Type u} {σ : Type v} [CommRing R] {I : Ideal R} {f : MvPolynomial σ R} : f ∈ Ideal.map C I ↔ ∀ (m : σ →₀ ℕ), coeff m f ∈ I

The push-forward of an ideal I of R to MvPolynomial σ R via inclusion is exactly the set of polynomials whose coefficients are in I

theorem MvPolynomial.ker_map {R : Type u} {S : Type u_1} {σ : Type v} [CommRing R] [CommRing S] (f : R →+* S) : RingHom.ker (map f) = Ideal.map C (RingHom.ker f)

theorem MvPolynomial.ker_mapAlgHom {R : Type u} [CommRing R] {S₁ : Type u_2} {S₂ : Type u_3} {σ : Type u_4} [CommRing S₁] [CommRing S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) : RingHom.ker (mapAlgHom f) = Ideal.map C (RingHom.ker f)