mathlibdocumentation

ring_theory.polynomial.basic

Ring-theoretic supplement of data.polynomial. #

Main results #

• mv_polynomial.is_domain: If a ring is an integral domain, then so is its polynomial ring over finitely many variables.
• polynomial.is_noetherian_ring: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
• polynomial.wf_dvd_monoid: If an integral domain is a wf_dvd_monoid, then so is its polynomial ring.
• polynomial.unique_factorization_monoid, mv_polynomial.unique_factorization_monoid: If an integral domain is a unique_factorization_monoid, then so is its polynomial ring (of any number of variables).
@[protected, instance]
def polynomial.char_p {R : Type u} [semiring R] (p : ) [h : p] :
noncomputable def polynomial.degree_le (R : Type u) [semiring R] (n : with_bot ) :

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

Equations
noncomputable def polynomial.degree_lt (R : Type u) [semiring R] (n : ) :

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

Equations
theorem polynomial.mem_degree_le {R : Type u} [semiring R] {n : with_bot } {f : polynomial R} :
theorem polynomial.degree_le_mono {R : Type u} [semiring R] {m n : with_bot } (H : m n) :
theorem polynomial.degree_le_eq_span_X_pow {R : Type u} [semiring R] {n : } :
= (finset.image (λ (n : ), (finset.range (n + 1)))
theorem polynomial.mem_degree_lt {R : Type u} [semiring R] {n : } {f : polynomial R} :
theorem polynomial.degree_lt_mono {R : Type u} [semiring R] {m n : } (H : m n) :
theorem polynomial.degree_lt_eq_span_X_pow {R : Type u} [semiring R] {n : } :
= (finset.image (λ (n : ), (finset.range n))
noncomputable def polynomial.degree_lt_equiv (R : Type u_1) [semiring R] (n : ) :
n) ≃ₗ[R] fin n → R

The first n coefficients on degree_lt n form a linear equivalence with fin n → R.

Equations
@[simp]
theorem polynomial.degree_lt_equiv_eq_zero_iff_eq_zero {R : Type u} [semiring R] {n : } {p : polynomial R} (hp : p ) :
p, hp⟩ = 0 p = 0
theorem polynomial.eval_eq_sum_degree_lt_equiv {R : Type u} [semiring R] {n : } {p : polynomial R} (hp : p ) (x : R) :
= finset.univ.sum (λ (i : fin n), p, hp⟩ i * x ^ i)
noncomputable def polynomial.frange {R : Type u} [semiring R] (p : polynomial R) :

The finset of nonzero coefficients of a polynomial.

Equations
theorem polynomial.frange_zero {R : Type u} [semiring R] :
theorem polynomial.mem_frange_iff {R : Type u} [semiring R] {p : polynomial R} {c : R} :
c p.frange ∃ (n : ) (H : n p.support), c = p.coeff n
theorem polynomial.frange_one {R : Type u} [semiring R] :
1.frange {1}
theorem polynomial.coeff_mem_frange {R : Type u} [semiring R] (p : polynomial R) (n : ) (h : p.coeff n 0) :
theorem polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [semiring R] (n : ) :
((finset.range n).sum (λ (i : ), .comp = (finset.range n).sum (λ (i : ), (n.choose (i + 1)) *
theorem polynomial.monic.geom_sum {R : Type u} [semiring R] {P : polynomial R} (hP : P.monic) (hdeg : 0 < P.nat_degree) {n : } (hn : n 0) :
((finset.range n).sum (λ (i : ), 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) :
((finset.range n).sum (λ (i : ), P ^ i)).monic
theorem polynomial.monic_geom_sum_X {R : Type u} [semiring R] {n : } (hn : n 0) :
((finset.range n).sum (λ (i : ), .monic
noncomputable def polynomial.restriction {R : Type u} [ring R] (p : polynomial R) :

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

Equations
@[simp]
theorem polynomial.coeff_restriction {R : Type u} [ring R] {p : polynomial R} {n : } :
@[simp]
theorem polynomial.coeff_restriction' {R : Type u} [ring R] {p : polynomial R} {n : } :
@[simp]
theorem polynomial.support_restriction {R : Type u} [ring R] (p : polynomial R) :
@[simp]
theorem polynomial.map_restriction {R : Type u} [comm_ring R] (p : polynomial R) :
@[simp]
theorem polynomial.degree_restriction {R : Type u} [ring R] {p : polynomial R} :
@[simp]
theorem polynomial.nat_degree_restriction {R : Type u} [ring R] {p : polynomial R} :
@[simp]
theorem polynomial.monic_restriction {R : Type u} [ring R] {p : polynomial R} :
@[simp]
theorem polynomial.restriction_zero {R : Type u} [ring R] :
@[simp]
theorem polynomial.restriction_one {R : Type u} [ring R] :
theorem polynomial.eval₂_restriction {R : Type u} {S : Type u_1} [ring R] [semiring S] {f : R →+* S} {x : S} {p : polynomial R} :
noncomputable def polynomial.to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) :

Given a polynomial p and a subring T that contains the coefficients of p, return the corresponding polynomial whose coefficients are in T.

Equations
@[simp]
theorem polynomial.coeff_to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) {n : } :
((p.to_subring T hp).coeff n) = p.coeff n
@[simp]
theorem polynomial.coeff_to_subring' {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) {n : } :
((p.to_subring T hp).coeff n).val = p.coeff n
@[simp]
theorem polynomial.support_to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) :
@[simp]
theorem polynomial.degree_to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) :
@[simp]
theorem polynomial.nat_degree_to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) :
@[simp]
theorem polynomial.monic_to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) :
@[simp]
theorem polynomial.to_subring_zero {R : Type u} [ring R] (T : subring R) :
0.to_subring T _ = 0
@[simp]
theorem polynomial.to_subring_one {R : Type u} [ring R] (T : subring R) :
1.to_subring T _ = 1
@[simp]
theorem polynomial.map_to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : (p.frange) T) :
(p.to_subring T hp) = p
noncomputable def polynomial.of_subring {R : Type u} [ring R] (T : subring R) (p : polynomial T) :

Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefficients are in the ambient ring.

Equations
theorem polynomial.coeff_of_subring {R : Type u} [ring R] (T : subring R) (p : polynomial T) (n : ) :
.coeff n = (p.coeff n)
@[simp]
theorem polynomial.frange_of_subring {R : Type u} [ring R] (T : subring R) {p : polynomial T} :
theorem polynomial.mem_ker_mod_by_monic {R : Type u} [comm_ring R] {q : polynomial R} (hq : q.monic) {p : polynomial R} :
q p
@[simp]
theorem polynomial.ker_mod_by_monic_hom {R : Type u} [comm_ring R] {q : polynomial R} (hq : q.monic) :
def ideal.of_polynomial {R : Type u} [semiring R] (I : ideal (polynomial R)) :

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

Equations
theorem ideal.mem_of_polynomial {R : Type u} [semiring R] {I : ideal (polynomial R)} (x : polynomial R) :
x I
noncomputable def ideal.degree_le {R : Type u} [semiring R] (I : ideal (polynomial R)) (n : with_bot ) :

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

Equations
noncomputable def ideal.leading_coeff_nth {R : Type u} [semiring R] (I : ideal (polynomial R)) (n : ) :

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

Equations
noncomputable def ideal.leading_coeff {R : Type u} [semiring R] (I : ideal (polynomial R)) :

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

Equations
theorem ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} (I : ideal (polynomial R)) (p : polynomial R) (hp : ∀ (n : ), ) :
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} {I : ideal R} {f : polynomial R} :
∀ (n : ), f.coeff n I

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

theorem polynomial.ker_map_ring_hom {R : Type u} {S : Type u_1} [semiring S] (f : R →+* S) :
theorem ideal.mem_leading_coeff_nth {R : Type u} (I : ideal (polynomial R)) (n : ) (x : R) :
x ∃ (p : (H : p I), p.degree n
theorem ideal.mem_leading_coeff_nth_zero {R : Type u} (I : ideal (polynomial R)) (x : R) :
x
theorem ideal.leading_coeff_nth_mono {R : Type u} (I : ideal (polynomial R)) {m n : } (H : m n) :
theorem ideal.mem_leading_coeff {R : Type u} (I : ideal (polynomial R)) (x : R) :
∃ (p : (H : p I),
theorem polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} {ι : Type u_1} (s : finset ι) (f : ι → ) (I : ideal R) (n : ι → ) (h : ∀ (i : ι), 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_is_field {R : Type u} [ring R] :

polynomial R is never a field for any ring R.

theorem ideal.eq_zero_of_constant_mem_of_maximal {R : Type u} [ring R] (hR : is_field R) (I : ideal (polynomial R)) [hI : I.is_maximal] (x : R) (hx : I) :
x = 0

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

theorem ideal.quotient_map_C_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (a : R) (H : a I) :
= 0
theorem ideal.eval₂_C_mk_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (f : polynomial R) (H : f ) :
noncomputable def ideal.polynomial_quotient_equiv_quotient_polynomial {R : Type u} [comm_ring R] (I : ideal R) :

If I is an ideal of R, then the ring polynomials over the quotient ring I.quotient is isomorphic to the quotient of polynomial R by the ideal map C I, where map C I contains exactly the polynomials whose coefficients all lie in I

Equations
theorem ideal.is_domain_map_C_quotient {R : Type u} [comm_ring R] {P : ideal R} (H : P.is_prime) :

If P is a prime ideal of R, then R[x]/(P) is an integral domain.

theorem ideal.is_prime_map_C_of_is_prime {R : Type u} [comm_ring R] {P : ideal R} (H : P.is_prime) :

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

theorem ideal.eq_zero_of_polynomial_mem_map_range {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (x : .range))  :
x = 0

Given any ring R and an ideal I of polynomial R, we get a map R → R[x] → R[x]/I. If we let R be the image of R in R[x]/I then we also have a map R[x] → R'[x]. In particular we can map I across this map, to get I' and a new map R' → R'[x] → R'[x]/I. This theorem shows I' will not contain any non-zero constant polynomials

theorem ideal.is_fg_degree_le {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (n : ) :
theorem polynomial.prime_C_iff {R : Type u} [comm_ring R] {r : R} :
theorem mv_polynomial.prime_C_iff {R : Type u} (σ : Type v) [comm_ring R] {r : R} :
theorem mv_polynomial.prime_rename_iff {R : Type u} {σ : Type v} [comm_ring R] (s : set σ) {p : R} :
@[protected, instance]
def polynomial.wf_dvd_monoid {R : Type u_1} [comm_ring R] [is_domain R]  :
@[protected, instance]
theorem polynomial.is_noetherian_ring {R : Type u} [comm_ring R]  :

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

theorem polynomial.exists_irreducible_of_degree_pos {R : Type u} [comm_ring R] [is_domain R] {f : polynomial R} (hf : 0 < f.degree) :
∃ (g : , g f
theorem polynomial.exists_irreducible_of_nat_degree_pos {R : Type u} [comm_ring R] [is_domain R] {f : polynomial R} (hf : 0 < f.nat_degree) :
∃ (g : , g f
theorem polynomial.exists_irreducible_of_nat_degree_ne_zero {R : Type u} [comm_ring R] [is_domain R] {f : polynomial R} (hf : f.nat_degree 0) :
∃ (g : , g f
theorem polynomial.linear_independent_powers_iff_aeval {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) (v : M) :
(λ (n : ), (f ^ n) v) ∀ (p : , ( p) v = 0p = 0
theorem polynomial.disjoint_ker_aeval_of_coprime {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) {p q : polynomial R} (hpq : q) :
theorem polynomial.sup_aeval_range_eq_top_of_coprime {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) {p q : polynomial R} (hpq : q) :
theorem polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [comm_ring R] [ M] {f : M →ₗ[R] M} {p q : polynomial R} :
theorem polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) {p q : polynomial R} (hpq : q) :
@[protected, instance]
def mv_polynomial.is_noetherian_ring {R : Type u} {σ : Type v} [comm_ring R] [fintype σ]  :

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

Auxiliary lemma: Multivariate polynomials over an integral domain with variables indexed by fin n form an integral domain. This fact is proven inductively, and then used to prove the general case without any finiteness hypotheses. See mv_polynomial.no_zero_divisors for the general case.

theorem mv_polynomial.no_zero_divisors_of_finite (R : Type u) (σ : Type v) [finite σ]  :

Auxiliary definition: Multivariate polynomials in finitely many variables over an integral domain form an integral domain. This fact is proven by transport of structure from the mv_polynomial.no_zero_divisors_fin, and then used to prove the general case without finiteness hypotheses. See mv_polynomial.no_zero_divisors for the general case.

@[protected, instance]
def mv_polynomial.no_zero_divisors {R : Type u} {σ : Type v} :
@[protected, instance]
def mv_polynomial.is_domain {R : Type u} {σ : Type v} [comm_ring R] [is_domain R] :

The multivariate polynomial ring over an integral domain is an integral domain.

theorem mv_polynomial.map_mv_polynomial_eq_eval₂ {R : Type u} {σ : Type v} [comm_ring R] {S : Type u_1} [comm_ring S] [fintype σ] (ϕ : →+* S) (p : R) :
ϕ p = (λ (s : σ), ϕ (mv_polynomial.X s)) p
theorem mv_polynomial.quotient_map_C_eq_zero {R : Type u} {σ : Type v} [comm_ring R] {I : ideal R} {i : R} (hi : i I) :
theorem mv_polynomial.mem_ideal_of_coeff_mem_ideal {R : Type u} {σ : Type v} [comm_ring R] (I : ideal R)) (p : R) (hcoe : ∀ (m : σ →₀ ), ) :
p I

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

theorem mv_polynomial.mem_map_C_iff {R : Type u} {σ : Type v} [comm_ring R] {I : ideal R} {f : R} :
∀ (m : σ →₀ ), I

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

theorem mv_polynomial.ker_map {R : Type u} {S : Type u_1} {σ : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :
theorem mv_polynomial.eval₂_C_mk_eq_zero {R : Type u} {σ : Type v} [comm_ring R] {I : ideal R} {a : R} (ha : a ) :
noncomputable def mv_polynomial.quotient_equiv_quotient_mv_polynomial {R : Type u} {σ : Type v} [comm_ring R] (I : ideal R) :
(R I) ≃ₐ[R]

If I is an ideal of R, then the ring mv_polynomial σ I.quotient is isomorphic as an R-algebra to the quotient of mv_polynomial σ R by the ideal generated by I.

Equations
@[protected, instance]
@[protected, instance]
def mv_polynomial.unique_factorization_monoid (σ : Type v) {D : Type u} [comm_ring D] [is_domain D]  :