The content ideal of a polynomial

In this file we introduce the content ideal of a polynomial p : R[X] as the ideal generated by its coefficients, and we prove some basic properties about it.

Main Definitions

Let p : R[X].

• p.contentIdeal is the Ideal R generated by the coefficients of p.

Main Results

• Polynomial.contentIdeal_mul_le_mul_contentIdeal: the content ideal of the product of two polynomials is contained in the product of their content ideals.
• Polynomial.isPrimitive_of_contentIdeal_eq_top: if the content ideal of p is the whole ring, then p is primitive.
• Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top: in case the content ideal of p is principal, p is primitive if and only if its content ideal is the whole ring.
• Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul: the product of the content ideals of two polynomials is contained in the radical of the content ideal of their product.
• Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal: if the content ideal of p is principal, then it is equal to the ideal generated by the content of p.
• contentIdeal_mul_eq_top_of_contentIdeal_eq_top: if the content ideals of two polynomials are the whole ring, then the content ideal of their product is the whole ring. This is also often called Gauss' Lemma.

TODO

• Prove the Dedekind-Mertens lemma, see https://www.cse.chalmers.se/~coquand/mertens.pdf

noncomputable def Polynomial.contentIdeal {R : Type u_1} [Semiring R] (p : Polynomial R) : Ideal R

The content ideal of a polynomial p is the ideal generated by its coefficients.

Equations

• p.contentIdeal = Ideal.span ↑p.coeffs

theorem Polynomial.contentIdeal_def {R : Type u_1} [Semiring R] (p : Polynomial R) : p.contentIdeal = Ideal.span ↑p.coeffs

@[simp]

theorem Polynomial.contentIdeal_zero {R : Type u_1} [Semiring R] : contentIdeal 0 = ⊥

@[simp]

theorem Polynomial.contentIdeal_eq_bot_iff {R : Type u_1} [Semiring R] (p : Polynomial R) : p.contentIdeal = ⊥ ↔ p = 0

theorem Polynomial.coeff_mem_contentIdeal {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) : p.coeff n ∈ p.contentIdeal

@[simp]

theorem Polynomial.contentIdeal_monomial {R : Type u_1} [Semiring R] (n : ℕ) (r : R) : ((monomial n) r).contentIdeal = Ideal.span {r}

@[simp]

theorem Polynomial.contentIdeal_C {R : Type u_1} [Semiring R] (r : R) : (C r).contentIdeal = Ideal.span {r}

@[simp]

theorem Polynomial.contentIdeal_one {R : Type u_1} [Semiring R] : contentIdeal 1 = ⊤

theorem Polynomial.contentIdeal_FG {R : Type u_1} [Semiring R] (p : Polynomial R) : p.contentIdeal.FG

theorem Polynomial.contentIdeal_map_eq_map_contentIdeal {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : (map f p).contentIdeal = Ideal.map f p.contentIdeal

theorem Polynomial.contentIdeal_mul_le_mul_contentIdeal {R : Type u_1} [Semiring R] (p q : Polynomial R) : (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal

theorem Polynomial.contentIdeal_le_contentIdeal_of_dvd {R : Type u_3} [CommSemiring R] {p q : Polynomial R} (hpq : p ∣ q) : q.contentIdeal ≤ p.contentIdeal

theorem Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff {R : Type u_3} [CommSemiring R] {p : Polynomial R} (h_prin : IsPrincipal p.contentIdeal) (n : ℕ) : generator p.contentIdeal ∣ p.coeff n

theorem Submodule.IsPrincipal.contentIdeal_generator_dvd {R : Type u_3} [CommSemiring R] {p : Polynomial R} (h_prin : IsPrincipal p.contentIdeal) : Polynomial.C (generator p.contentIdeal) ∣ p

theorem Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd {R : Type u_3} [CommSemiring R] {p : Polynomial R} (h_prin : IsPrincipal p.contentIdeal) (r : R) : p.contentIdeal ≤ Ideal.span {r} ↔ Polynomial.C r ∣ p

theorem Polynomial.isPrimitive_of_contentIdeal_eq_top {R : Type u_3} [CommSemiring R] {p : Polynomial R} (h : p.contentIdeal = ⊤) : p.IsPrimitive

If the coefficients of p generate the whole ring, then p is primitive.

theorem Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top {R : Type u_3} [CommSemiring R] {p : Polynomial R} (h_prin : IsPrincipal p.contentIdeal) : p.IsPrimitive ↔ p.contentIdeal = ⊤

theorem Polynomial.contentIdeal_eq_top_of_contentIdeal_mul_eq_top {R : Type u_3} [CommSemiring R] {p q : Polynomial R} (h : (p * q).contentIdeal = ⊤) : p.contentIdeal = ⊤

theorem Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul {R : Type u_3} [CommRing R] {p q : Polynomial R} : p.contentIdeal * q.contentIdeal ≤ (p * q).contentIdeal.radical

theorem Polynomial.contentIdeal_mul_eq_top_of_contentIdeal_eq_top {R : Type u_3} [CommRing R] {p q : Polynomial R} (hp : p.contentIdeal = ⊤) (hq : q.contentIdeal = ⊤) : (p * q).contentIdeal = ⊤

theorem Polynomial.contentIdeal_le_span_content {R : Type u_3} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} : p.contentIdeal ≤ Ideal.span {p.content}

theorem Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal {R : Type u_3} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} (h_prin : IsPrincipal p.contentIdeal) : p.contentIdeal = Ideal.span {p.content}

theorem Polynomial.isPrimitive_iff_contentIdeal_eq_top {R : Type u_3} [CommSemiring R] [IsBezout R] (p : Polynomial R) : p.IsPrimitive ↔ p.contentIdeal = ⊤

The polynomial p is primitive if and only if the coefficients of p generate the whole ring.