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.

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} [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} [Semiring R] (f : Polynomial R) (m : ℕ) (a : R) : f.sylvester (C a) m 0 = Matrix.diagonal fun (x : Fin (0 + m)) => a

def Polynomial.resultant {R : Type u} [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} [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} [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.