Polynomials of small degree

Splitting criteria for low-degree polynomials and a separability criterion, all read off the coefficients.

• Away from characteristic two, a cubic that already has one root splits exactly when its discriminant is a square: the root splits off a quadratic factor whose discriminant differs from that of the cubic by a square, and a quadratic splits exactly when its discriminant is a square. Normalization by the leading coefficient reduces the statement to the monic case.
• A cubic with two distinct roots in its coefficient field splits there, and conversely a separable split polynomial of degree at least two has two distinct roots.
• An irreducible polynomial is separable as soon as its degree is nonzero in the coefficient field, which for a quartic is exactly what characteristic ≠ 2 gives.
• A monic quadratic X² + aX + b divides a depressed quartic X⁴ + pX² + qX + r exactly when the two coefficients of the remainder of the division vanish. Over ℤ this reduces the search for a quadratic factor of an explicit quartic to two Diophantine equations, which a reduction modulo a small prime can rule out. The analogous criterion for X⁵ + cX + d supports finite-field irreducibility tests for quintics: in degree at most five a polynomial with no root and no monic quadratic factor is irreducible.

Together these turn the single test "the resolvent cubic of a quartic has a root in the base field" into the classical resolvent conditions — irreducible, splits completely, exactly one root — used by the quartic label table of TauCeti.FieldTheory.GaloisGroups.Quartic.Basic.

Main results

• Polynomial.Irreducible.separable_of_natDegree_cast_ne_zero and Polynomial.separable_of_irreducible_of_natDegree_eq_four
• Polynomial.exists_natDegree_eq_two_of_natDegree_eq_three_of_isRoot
• Polynomial.splits_iff_isSquare_discr_of_natDegree_eq_two and Polynomial.splits_iff_isSquare_discr_of_natDegree_eq_three_of_isRoot
• Polynomial.Splits.of_natDegree_eq_three_of_isRoot_of_isRoot_of_ne and Polynomial.Splits.exists_isRoot_ne
• Polynomial.X_sq_add_C_mul_X_add_C_dvd_X_pow_four_add_iff: when a monic quadratic divides a depressed quartic, by explicit division with remainder
• Polynomial.X_sq_add_C_mul_X_add_C_dvd_X_pow_five_add_iff: when a monic quadratic divides X⁵ + cX + d
• Polynomial.Monic.irreducible_of_degree_le_five_of_not_isRoot_of_not_quadratic_dvd and Polynomial.irreducible_X_pow_five_add_C_mul_X_add_C: irreducibility in degree at most five from the absence of linear and monic quadratic factors

theorem Polynomial.exists_natDegree_eq_two_of_natDegree_eq_three_of_isRoot {R : Type u_1} [CommRing R] {g : Polynomial R} (hdeg : g.natDegree = 3) {a : R} (ha : g.IsRoot a) : ∃ (q : Polynomial R), q.natDegree = 2 ∧ g = (X - C a) * q

A cubic with a root a over a commutative ring is (X - a) times a quadratic.

theorem Polynomial.Irreducible.separable_of_natDegree_cast_ne_zero {F : Type u_1} [Field F] {f : Polynomial F} (hirr : Irreducible f) (hdeg : ↑f.natDegree ≠ 0) : f.Separable

An irreducible polynomial whose degree is nonzero in the coefficient field is separable: the derivative then has the nonzero leading coefficient natDegree • leadingCoeff.

theorem Polynomial.separable_of_irreducible_of_natDegree_eq_four {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hirr : Irreducible f) (hdeg : f.natDegree = 4) : f.Separable

An irreducible quartic is separable away from characteristic two.

theorem Polynomial.splits_iff_isSquare_discr_of_natDegree_eq_two {F : Type u_1} [Field F] {q : Polynomial F} (hchar : ringChar F ≠ 2) (hdeg : q.natDegree = 2) : q.Splits ↔ IsSquare q.discr

Away from characteristic two, a quadratic splits over its coefficient field exactly when its discriminant is a square. This is Polynomial.splits_quadratic_iff_isSquare read on discr rather than on a coefficient triple.

theorem Polynomial.splits_iff_isSquare_discr_of_natDegree_eq_three_of_isRoot {F : Type u_1} [Field F] {g : Polynomial F} (hdeg : g.natDegree = 3) (hchar : ringChar F ≠ 2) {a : F} (ha : g.IsRoot a) : g.Splits ↔ IsSquare g.discr

Away from characteristic two, a cubic with a root in its coefficient field splits there exactly when its discriminant is a square. Multiplication by the inverse leading coefficient reduces to the monic criterion, and changes the discriminant by a nonzero fourth power.

theorem Polynomial.Splits.of_natDegree_eq_three_of_isRoot_of_isRoot_of_ne {F : Type u_1} [Field F] {g : Polynomial F} (hdeg : g.natDegree = 3) {a x : F} (ha : g.IsRoot a) (hx : g.IsRoot x) (hxa : x ≠ a) : g.Splits

A cubic with two distinct roots in its coefficient field splits there.

theorem Polynomial.Splits.exists_isRoot_ne {F : Type u_1} [Field F] {g : Polynomial F} (hsplit : g.Splits) (hsep : g.Separable) (hdeg : 2 ≤ g.natDegree) (a : F) : ∃ (x : F), g.IsRoot x ∧ x ≠ a

A separable split polynomial of degree at least two has a root away from any given element. This is the converse of Polynomial.Splits.of_natDegree_eq_three_of_isRoot_of_isRoot_of_ne in the form the uniqueness of a root is used: a split separable polynomial has as many roots as its degree.

theorem Polynomial.X_sq_add_C_mul_X_add_C_dvd_X_pow_four_add_iff {R : Type u_1} [CommRing R] (a b p q r : R) : X ^ 2 + C a * X + C b ∣ X ^ 4 + C p * X ^ 2 + C q * X + C r ↔ q = a ^ 3 - 2 * a * b + a * p ∧ r = a ^ 2 * b - b ^ 2 + b * p

Division of a depressed quartic by a monic quadratic. The monic quadratic X² + aX + b divides the depressed quartic X⁴ + pX² + qX + r exactly when the linear remainder of the division vanishes, that is when q = a³ - 2ab + ap and r = a²b - b² + bp. The quotient is X² - aX + (a² - b + p). Over the zero ring both sides hold trivially.

theorem Polynomial.X_sq_add_C_mul_X_add_C_dvd_X_pow_five_add_iff {R : Type u_1} [CommRing R] (a b c d : R) : X ^ 2 + C a * X + C b ∣ X ^ 5 + C c * X + C d ↔ a ^ 4 - 3 * a ^ 2 * b + b ^ 2 + c = 0 ∧ a ^ 3 * b - 2 * a * b ^ 2 + d = 0

A monic quadratic X² + aX + b divides X⁵ + cX + d exactly when a⁴ - 3a²b + b² + c = 0 and a³b - 2ab² + d = 0. This holds over any commutative ring.

theorem Polynomial.Monic.irreducible_of_degree_le_five_of_not_isRoot_of_not_quadratic_dvd {R : Type u_1} [CommRing R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hdeg : p.natDegree ∈ Finset.Icc 1 5) (hroot : ∀ (x : R), ¬p.IsRoot x) (hquad : ∀ (a b : R), ¬X ^ 2 + C a * X + C b ∣ p) : Irreducible p

A monic polynomial of degree between one and five over a commutative ring without zero divisors is irreducible as soon as it has no root and no monic quadratic factor: a proper monic factor of least degree has degree at most half the degree, so it is linear or quadratic. This extends Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three to degrees four and five.

theorem Polynomial.irreducible_X_pow_five_add_C_mul_X_add_C {R : Type u_1} [CommRing R] [NoZeroDivisors R] {c d : R} (hroot : ∀ (x : R), x ^ 5 + c * x + d ≠ 0) (hquad : ∀ (a b : R), ¬(a ^ 4 - 3 * a ^ 2 * b + b ^ 2 + c = 0 ∧ a ^ 3 * b - 2 * a * b ^ 2 + d = 0)) : Irreducible (X ^ 5 + C c * X + C d)

The quintic X⁵ + cX + d over a commutative ring without zero divisors is irreducible when it has no root and no pair (a, b) solves the two equations of Polynomial.X_sq_add_C_mul_X_add_C_dvd_X_pow_five_add_iff, that is, when it has neither a linear nor a monic quadratic factor. Over a finite field both conditions are finite checks.