Resultant of two polynomials

This file contains basic facts about resultant of two polynomials over commutative rings.

Main definitions

• Polynomial.resultant: The resultant of two polynomials p and q is defined as the determinant of the Sylvester matrix of p and q.
• Polynomial.disc: The discriminant of a polynomial f is defined as the resultant of f and f.derivative, modified by factoring out a sign and a power of the leading term.

TODO

• The eventual goal is to prove the following property: resultant (∏ a ∈ s, (X - C a)) f = ∏ a ∈ s, f.eval a. This allows us to write the resultant f g as the product of terms of the form a - b where a is a root of f and b is a root of g.
• A smaller intermediate goal is to show that the Sylvester matrix corresponds to the linear map that we will call the Sylvester map, which is R[X]_n × R[X]_m →ₗ[R] R[X]_(n + m) given by (p, q) ↦ f * p + g * q, where R[X]_n is Polynomial.degreeLT in Mathlib.RingTheory.Polynomial.Basic.
• Resultant of two binary forms (i.e. homogeneous polynomials in two variables), after binary forms are implemented.

def Polynomial.sylvester {R : Type u_1} [Semiring R] (f g : Polynomial R) (m n : ℕ) : Matrix (Fin (n + m)) (Fin (n + m)) R

The Sylvester matrix of two polynomials f and g of degrees m and n respectively is a (n+m) × (n+m) matrix with the coefficients of f and g arranged in a specific way. Here, m and n are free variables, not necessarily equal to the actual degrees of the polynomials f and g.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.sylvester_C_right {R : Type u_1} [Semiring R] (f : Polynomial R) (m : ℕ) (a : R) : f.sylvester (C a) m 0 = Matrix.diagonal fun (x : Fin (0 + m)) => a

noncomputable def Polynomial.sylvesterDeriv {R : Type u_1} [Semiring R] (f : Polynomial R) : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R

The Sylvester matrix for f and f.derivative, modified by dividing the bottom row by the leading coefficient of f. Important because its determinant is (up to a sign) the discriminant of f.

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.sylvesterDeriv_updateRow {R : Type u_1} [Semiring R] (f : Polynomial R) (hf : 0 < f.natDegree) : f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩) = f.sylvester (derivative f) f.natDegree (f.natDegree - 1)

We can get the usual Sylvester matrix of f and f.derivative back from the modified one by multiplying the last row by the leading coefficient of f.

def Polynomial.resultant {R : Type u_1} [CommRing R] (f g : Polynomial R) (m : ℕ := f.natDegree) (n : ℕ := g.natDegree) : R

The resultant of two polynomials f and g is the determinant of the Sylvester matrix of f and g. The size arguments m and n are implemented as optParam, meaning that the default values are f.natDegree and g.natDegree respectively, but they can also be specified to be other values.

Equations

• f.resultant g m n = (f.sylvester g m n).det

@[simp]

theorem Polynomial.resultant_C_zero_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m : ℕ) (a : R) : f.resultant (C a) m 0 = a ^ m

For polynomial f and constant a, Res(f, a) = a ^ m.

theorem Polynomial.resultant_C_right {R : Type u_1} [CommRing R] (f : Polynomial R) (m : ℕ) (a : R) : f.resultant (C a) m = a ^ m

For polynomial f and constant a, Res(f, a) = a ^ m.

noncomputable def Polynomial.disc {R : Type u_1} [CommRing R] (f : Polynomial R) : R

The discriminant of a polynomial, defined as the determinant of f.sylvesterDeriv modified by a sign. The sign is chosen so polynomials over ℝ with all roots real have non-negative discriminant.

Equations

• f.disc = f.sylvesterDeriv.det * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2)

@[simp]

theorem Polynomial.disc_C {R : Type u_1} [CommRing R] (r : R) : (C r).disc = 1

The discriminant of a constant polynomial is 1.

theorem Polynomial.disc_of_degree_eq_one {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 1) : f.disc = 1

The discriminant of a linear polynomial is 1.

theorem Polynomial.disc_of_degree_eq_two {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 2) : f.disc = f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2

Standard formula for the discriminant of a quadratic polynomial.

theorem Polynomial.resultant_deriv {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : 0 < f.degree) : f.resultant (derivative f) f.natDegree (f.natDegree - 1) = (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.disc

Relation between the resultant and the discriminant.

(Note this is actually false when f is a constant polynomial not equal to 1, so the assumption on the degree is genuinely needed.)

theorem Polynomial.disc_of_degree_eq_three {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.degree = 3) : f.disc = f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 - 27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 + 18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Standard formula for the discriminant of a cubic polynomial.