GCD structures on polynomials

Definitions and basic results about polynomials over GCD domains, particularly their contents and primitive polynomials.

Main Definitions

Let p : R[X].

• p.content is the gcd of the coefficients of p.
• p.IsPrimitive indicates that p.content = 1.

Main Results

• Polynomial.content_mul: if p q : R[X], then (p * q).content = p.content * q.content.
• Polynomial.NormalizedGcdMonoid: the polynomial ring of a GCD domain is itself a GCD domain.

Note

This has nothing to do with minimal polynomials of primitive elements in finite fields.

def Polynomial.IsPrimitive {R : Type u_1} [CommSemiring R] (p : Polynomial R) : Prop

A polynomial is primitive when the only constant polynomials dividing it are units. Note: This has nothing to do with minimal polynomials of primitive elements in finite fields.

theorem Polynomial.isPrimitive_iff_isUnit_of_C_dvd {R : Type u_1} [CommSemiring R] {p : Polynomial R} : p.IsPrimitive ↔ ∀ (r : R), C r ∣ p → IsUnit r

@[simp]

theorem Polynomial.isPrimitive_one {R : Type u_1} [CommSemiring R] : IsPrimitive 1

theorem Polynomial.Monic.isPrimitive {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : p.IsPrimitive

theorem Polynomial.IsPrimitive.ne_zero {R : Type u_1} [CommSemiring R] [Nontrivial R] {p : Polynomial R} (hp : p.IsPrimitive) : p ≠ 0

theorem Polynomial.isPrimitive_of_dvd {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q ∣ p) : q.IsPrimitive

theorem Irreducible.isPrimitive {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Irreducible p) (hp' : p.natDegree ≠ 0) : p.IsPrimitive

An irreducible nonconstant polynomial over a domain is primitive.

@[simp]

theorem Polynomial.isPrimitive_iff_ne_zero {F : Type u_2} [Field F] (p : Polynomial F) : p.IsPrimitive ↔ p ≠ 0

In a field, the notion of primitive polynomials is degenerate.

def Polynomial.content {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : R

p.content is the gcd of the coefficients of p.

theorem Polynomial.content_dvd_coeff {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} (n : ℕ) : p.content ∣ p.coeff n

@[simp]

theorem Polynomial.content_C {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {r : R} : (C r).content = normalize r

@[simp]

theorem Polynomial.content_zero {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] : content 0 = 0

@[simp]

theorem Polynomial.content_one {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] : content 1 = 1

theorem Polynomial.content_X_mul {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} : (X * p).content = p.content

@[simp]

theorem Polynomial.content_X_pow {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {k : ℕ} : (X ^ k).content = 1

@[simp]

theorem Polynomial.content_X {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] : X.content = 1

theorem Polynomial.content_C_mul {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (r : R) (p : Polynomial R) : (C r * p).content = normalize r * p.content

@[simp]

theorem Polynomial.content_monomial {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {r : R} {k : ℕ} : ((monomial k) r).content = normalize r

theorem Polynomial.content_eq_zero_iff {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} : p.content = 0 ↔ p = 0

theorem Polynomial.normalize_content {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} : normalize p.content = p.content

@[simp]

theorem Polynomial.normUnit_content {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} : normUnit p.content = 1

theorem Polynomial.content_eq_gcd_range_of_lt {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) (n : ℕ) (h : p.natDegree < n) : p.content = (Finset.range n).gcd p.coeff

theorem Polynomial.content_eq_gcd_range_succ {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.content = (Finset.range p.natDegree.succ).gcd p.coeff

theorem Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.content = gcd p.leadingCoeff p.eraseLead.content

theorem Polynomial.dvd_content_iff_C_dvd {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} {r : R} : r ∣ p.content ↔ C r ∣ p

theorem Polynomial.C_content_dvd {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : C p.content ∣ p

theorem Polynomial.isPrimitive_iff_content_eq_one {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} : p.IsPrimitive ↔ p.content = 1

theorem Polynomial.IsPrimitive.content_eq_one {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p.IsPrimitive) : p.content = 1

noncomputable def Polynomial.primPart {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : Polynomial R

The primitive part of a polynomial p is the primitive polynomial gained by dividing p by p.content. If p = 0, then p.primPart = 1.

theorem Polynomial.eq_C_content_mul_primPart {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p = C p.content * p.primPart

@[simp]

theorem Polynomial.primPart_zero {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] : primPart 0 = 1

theorem Polynomial.isPrimitive_primPart {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart.IsPrimitive

theorem Polynomial.content_primPart {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart.content = 1

theorem Polynomial.primPart_ne_zero {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] [Nontrivial R] (p : Polynomial R) : p.primPart ≠ 0

theorem Polynomial.natDegree_primPart {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart.natDegree = p.natDegree

@[simp]

theorem Polynomial.IsPrimitive.primPart_eq {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p.IsPrimitive) : p.primPart = p

theorem Polynomial.isUnit_primPart_C {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (r : R) : IsUnit (C r).primPart

theorem Polynomial.primPart_dvd {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart ∣ p

theorem Polynomial.aeval_primPart_eq_zero {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {S : Type u_2} [Ring S] [IsDomain S] [Algebra R S] [Module.IsTorsionFree R S] {p : Polynomial R} {s : S} (hpzero : p ≠ 0) (hp : (aeval s) p = 0) : (aeval s) p.primPart = 0

theorem Polynomial.eval₂_primPart_eq_zero {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {S : Type u_2} [CommSemiring S] [IsDomain S] {f : R →+* S} (hinj : Function.Injective ⇑f) {p : Polynomial R} {s : S} (hpzero : p ≠ 0) (hp : eval₂ f s p = 0) : eval₂ f s p.primPart = 0

theorem Polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {a : R} {p q : Polynomial R} (h : C a ∣ p - q) : gcd a p.content = gcd a q.content

theorem Polynomial.content_mul_aux {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} : gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff

@[simp]

theorem Polynomial.content_mul {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} : (p * q).content = p.content * q.content

theorem Polynomial.IsPrimitive.mul {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : (p * q).IsPrimitive

@[simp]

theorem Polynomial.primPart_mul {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} (h0 : p * q ≠ 0) : (p * q).primPart = p.primPart * q.primPart

theorem Polynomial.IsPrimitive.dvd_primPart_iff_dvd {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q ≠ 0) : p ∣ q.primPart ↔ p ∣ q

theorem Polynomial.exists_primitive_lcm_of_isPrimitive {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : ∃ (r : Polynomial R), r.IsPrimitive ∧ ∀ (s : Polynomial R), p ∣ s ∧ q ∣ s ↔ r ∣ s

theorem Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hq : q ≠ 0) : p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

@[implicit_reducible, instance 100]

noncomputable instance Polynomial.normalizedGcdMonoid {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] : NormalizedGCDMonoid (Polynomial R)

theorem Polynomial.degree_gcd_le_left {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p ≠ 0) (q : Polynomial R) : (gcd p q).degree ≤ p.degree

theorem Polynomial.degree_gcd_le_right {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] (p : Polynomial R) {q : Polynomial R} (hq : q ≠ 0) : (gcd p q).degree ≤ q.degree