The discriminant of a polynomial as a product over pairs of roots

Mathlib defines Polynomial.discr f as the determinant of f.sylvesterDeriv, corrected by the sign (-1) ^ (n * (n - 1) / 2) with n = f.natDegree. The division-free relation is that the resultant of f and f.derivative equals this sign times f.leadingCoeff * f.discr (Polynomial.resultant_deriv). What that definition does not say is what the discriminant measures. This file proves the classical root-product formula

(∏ i, (X - C (r i))).discr = ∏ i, ∏ j ∈ Ioi i, (r i - r j) ^ 2

for a family of roots r : Fin n → R over an arbitrary commutative ring, together with the consequences that read the formula: base change, and the criterion for a monic polynomial to be separable. It also gives the coefficient formula for the discriminant of a monic quartic. The depressed specialization of that formula is used to compare a quartic with its cubic resolvent.

Main results

• Polynomial.discr_prod_X_sub_C, Polynomial.discr_prod_X_sub_C_eq_sq: the root-product formula, in its squared-product form and in the form discr = δ ^ 2 for the Vandermonde-like product δ = ∏_{i < j} (rᵢ - rⱼ). The second is the shape the discriminant test for containment in the alternating group is stated with, since a Galois automorphism permutes the roots and multiplies δ by the sign of that permutation.
• Polynomial.Monic.discr_eq_prod_roots_sub_sq: the same formula for a monic polynomial, written against a numbering r : Fin f.natDegree → L of its root multiset over an extension.
• TauCeti.discrSqrt, TauCeti.discrSqrt_ne_zero, Polynomial.Monic.discrSqrt_sq: the product of the differences of a numbering of the distinct roots, its nonvanishing, and the fact that its square is the discriminant for a monic separable polynomial.
• Polynomial.Monic.prod_roots_eval_derivative: the product of the derivative over the root multiset, which is the discriminant up to the same sign. This is the shape in which the discriminant of a minimal polynomial is a norm.
• Polynomial.Monic.discr_mul: the product formula for discriminants, with the square of the resultant as its cross term.
• Polynomial.discr_X_pow_sub_C: the discriminant of a binomial X ^ n - C a.
• TauCeti.not_isSquare_discr_X_pow_five_sub_C: the discriminant 3125a⁴ of a pure quintic X ^ 5 - C a over ℚ with a ≠ 0 is not a square.
• TauCeti.discr_C_mul, TauCeti.isSquare_discr_iff_mem_range: the scaling law and square-root criterion for a not-necessarily-monic polynomial. Scaling holds over an integral domain; the square-root criterion uses a base field and a domain containing the roots.
• Polynomial.discr_map_of_natDegree_eq, Polynomial.Monic.discr_map: base change whenever the degree is preserved, with monicity as a convenient sufficient condition.
• Polynomial.Monic.isUnit_discr_iff, Polynomial.Monic.discr_ne_zero_iff, Polynomial.Monic.discr_ne_zero_iff_separable_map: a monic polynomial is separable exactly when its discriminant is a unit; over a field that reads discr f ≠ 0, and over a domain the correct statement passes to the fraction field.
• Polynomial.discr_ne_zero_iff: over a field, a nonzero polynomial that need not be monic is separable exactly when its discriminant is nonzero.
• Polynomial.Monic.separable_map_iff_map_discr_ne_zero, Polynomial.Monic.separable_map_zmod_iff_not_dvd_discr: the same criterion read along a ring homomorphism into a field, and its specialization to reduction of an integral polynomial modulo a prime.
• Cubic.toPoly_discr: the two discriminants of a cubic with nonzero leading coefficient agree, so that Cubic.discr and Polynomial.discr may be used interchangeably in degree three.
• Polynomial.Monic.discr_of_natDegree_eq_four, TauCeti.discr_depressedQuartic: the coefficient formula for a monic quartic and its depressed specialization, used to compare quartic and resolvent discriminants.
• Algebra.discr_powerBasis_eq_minpoly_discr: the algebra discriminant of a power basis agrees with the polynomial discriminant of the minimal polynomial of its generator.

Implementation notes

The root-product formula is a universal polynomial identity, so it is stated over an arbitrary commutative ring and proved by base change from MvPolynomial (Fin n) ℤ, which is a domain and over which the roots are the variables themselves.

The separability criterion is not a universal identity, and the failure is recorded here: Polynomial.not_separable_X_pow_two_sub_one shows that X ^ 2 - 1 over ℤ has nonzero discriminant 4 and is not Polynomial.Separable. Over a domain the criterion is therefore formulated after passage to a fraction field.

The sign bookkeeping — folding the off-diagonal product over ordered pairs into a product over unordered pairs, and evaluating ∑ i, #(Ioi i) as n * (n - 1) / 2 — follows the corresponding step of Algebra.discr_powerBasis_eq_prod'' in Mathlib/RingTheory/Discriminant.lean, and reuses the same lemma Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag. No Mathlib code is vendored.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §3.3.2 and §6.3.
• S. Lang, Algebra, third edition, Chapter IV, §8.

theorem Polynomial.Monic.resultant_deriv {R : Type u_3} [CommRing R] {f : Polynomial R} (hf : f.Monic) : f.resultant (derivative f) f.natDegree (f.natDegree - 1) = (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.discr

For a monic polynomial, the resultant of f and f.derivative, taken at the degree bounds f.natDegree and f.natDegree - 1 that the Sylvester matrix of the discriminant uses, is the discriminant up to the sign (-1) ^ (n * (n - 1) / 2).

This is the monic case of Polynomial.resultant_deriv: the leading coefficient of that lemma is 1, and its positive-degree hypothesis is unnecessary, the constant polynomial 1 being covered.

@[simp]

theorem Polynomial.discr_X_pow_sub_C {R : Type u_1} [CommRing R] (a : R) (n : ℕ) : (X ^ n - C a).discr = (-1) ^ (n * (n - 1) / 2) * ↑n ^ n * (-a) ^ (n - 1)

The discriminant of a binomial. Over any commutative ring, discr (X ^ n - C a) = (-1) ^ (n (n - 1) / 2) · nⁿ · (-a) ^ (n - 1); for n = 0 both sides are 1.

theorem TauCeti.not_isSquare_discr_X_pow_five_sub_C {a : ℚ} (ha : a ≠ 0) : ¬IsSquare (Polynomial.X ^ 5 - Polynomial.C a).discr

The discriminant 3125a⁴ of a pure quintic X⁵ - a over ℚ, with a ≠ 0, is not a square in ℚ.

theorem Polynomial.sylvesterDeriv_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : Polynomial R} (φ : R →+* S) (hdeg : (map φ f).natDegree = f.natDegree) : (Matrix.reindex (finCongr ⋯) (finCongr ⋯)) (map φ f).sylvesterDeriv = φ.mapMatrix f.sylvesterDeriv

Mapping coefficients preserves sylvesterDeriv after transporting its degree-dependent indices.

theorem Polynomial.discr_map_of_natDegree_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : Polynomial R} (φ : R →+* S) (hdeg : (map φ f).natDegree = f.natDegree) : (map φ f).discr = φ f.discr

Base change of the discriminant along a ring morphism that preserves the degree.

@[simp]

theorem Polynomial.Monic.discr_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : Polynomial R} (hf : f.Monic) (φ : R →+* S) : (Polynomial.map φ f).discr = φ f.discr

Base change of the discriminant along a ring morphism, for a monic polynomial. Monicity ensures that the degree is preserved.

theorem Polynomial.Monic.discr_mul {R : Type u_1} [CommRing R] {f g : Polynomial R} (hf : f.Monic) (hg : g.Monic) : (f * g).discr = f.discr * g.discr * f.resultant g ^ 2

The discriminant of a product of monic polynomials is the product of their discriminants and the square of their resultant.

The root-product formula

theorem Polynomial.Monic.prod_roots_eval_derivative {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} (hf : f.Monic) (hs : f.Splits) : (Multiset.map (fun (a : R) => eval a (derivative f)) f.roots).prod = (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.discr

For a monic polynomial that splits, the product of the derivative over the root multiset is the discriminant, up to the sign (-1) ^ (n * (n - 1) / 2). After base change and identification of the roots with conjugates, this yields the corresponding norm formula.

theorem Polynomial.discr_prod_X_sub_C {R : Type u_1} [CommRing R] {n : ℕ} (r : Fin n → R) : (∏ i : Fin n, (X - C (r i))).discr = ∏ i : Fin n, ∏ j > i, (r i - r j) ^ 2

The root-product formula for the discriminant. The discriminant of a product of linear factors is the square of the Vandermonde-like product of the differences of the roots. This is a universal polynomial identity, so it holds over any commutative ring, with the roots repeated according to multiplicity.

theorem Polynomial.discr_prod_X_sub_C_eq_sq {R : Type u_1} [CommRing R] {n : ℕ} (r : Fin n → R) : (∏ i : Fin n, (X - C (r i))).discr = (∏ i : Fin n, ∏ j > i, (r i - r j)) ^ 2

The root-product formula, in the form discr f = δ ^ 2 for the product δ of the differences of the roots taken over pairs i < j. This is the form the discriminant test for containment in the alternating group reads: a permutation of the roots multiplies δ by its sign.

theorem Polynomial.Monic.discr_eq_prod_roots_sub_sq {R : Type u_1} [CommRing R] {L : Type u_3} [CommRing L] [IsDomain L] [Algebra R L] {f : Polynomial R} (hf : f.Monic) {r : Fin f.natDegree → L} (hr : (Polynomial.map (algebraMap R L) f).roots = Multiset.map r Finset.univ.val) : (algebraMap R L) f.discr = ∏ i : Fin f.natDegree, ∏ j > i, (r i - r j) ^ 2

The root-product formula for a monic polynomial. Number the roots of a monic f over an extension L, with multiplicity, as r : Fin f.natDegree → L. Then the discriminant of f is the square of the Vandermonde-like product of the differences of the roots. Numbering the whole root multiset by Fin f.natDegree already says that f splits over L, so no splitting hypothesis appears.

The square root of the discriminant

def TauCeti.discrSqrt {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : E

The product ∏_{i < j} (rᵢ - rⱼ) of the differences of the roots of f in E, taken along a numbering e of the root set.

For monic separable f this is a square root of the discriminant, by Polynomial.Monic.discrSqrt_sq. It is only a square root: TauCeti.discrSqrt_trans shows that changing the numbering by an odd permutation changes the sign. The root set carries no order, so the numbering is an explicit argument and is never fixed globally.

Equations

• TauCeti.discrSqrt e = ∏ i : Fin f.natDegree, ∏ j > i, (↑(e i) - ↑(e j))

theorem TauCeti.discrSqrt_def {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : discrSqrt e = ∏ i : Fin f.natDegree, ∏ j > i, (↑(e i) - ↑(e j))

The unfolding equation for the square root of the discriminant.

@[simp]

theorem TauCeti.discrSqrt_trans {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (e : Fin f.natDegree ≃ ↑(f.rootSet E)) (π : Equiv.Perm (Fin f.natDegree)) : discrSqrt (Equiv.trans π e) = Equiv.Perm.sign π • discrSqrt e

Renumbering the roots by a permutation π multiplies the product of the root differences by the sign of π. This is the alternating behaviour that makes the discriminant test work.

theorem TauCeti.discrSqrt_ne_zero {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : discrSqrt e ≠ 0

The product of the differences of a numbering of distinct roots is nonzero.

theorem TauCeti.discr_C_mul {F : Type u_1} [CommRing F] [IsDomain F] {f : Polynomial F} (a : F) (ha : a ≠ 0) : (Polynomial.C a * f).discr = a ^ (2 * f.natDegree - 2) * f.discr

Over an integral domain, scaling a polynomial of degree n by a nonzero constant a scales its discriminant by a ^ (2 * n - 2).

theorem TauCeti.isSquare_discr_iff_mem_range {F : Type u_1} [Field F] {f : Polynomial F} {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] (hsep : f.Separable) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : IsSquare f.discr ↔ discrSqrt e ∈ Set.range ⇑(algebraMap F E)

For a separable polynomial, the discriminant is a square in the base field exactly when the product of the root differences in an extension domain comes from the base field. This is the nonmonic analogue of Polynomial.Monic.isSquare_discr_iff_mem_range.

@[simp]

theorem Polynomial.Monic.discrSqrt_sq {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (hf : f.Monic) (hsep : f.Separable) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : TauCeti.discrSqrt e ^ 2 = (algebraMap F E) f.discr

The defining property: the square of the product of the root differences is the discriminant.

theorem Polynomial.Monic.isSquare_discr_iff_mem_range {F : Type u_1} [Field F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (hf : f.Monic) (hsep : f.Separable) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : IsSquare f.discr ↔ TauCeti.discrSqrt e ∈ Set.range ⇑(algebraMap F E)

The discriminant is a square in the base field exactly when the product of the root differences already comes from the base field. No Galois hypothesis is involved: this is the elementary half of the discriminant test, and it is the reading of Polynomial.Monic.discrSqrt_sq in both directions.

Separability

@[simp]

theorem Polynomial.Monic.isUnit_discr_iff {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) : IsUnit f.discr ↔ f.Separable

A monic polynomial is separable exactly when its discriminant is a unit. This is the ring-level form of the criterion; over a field it reads f.discr ≠ 0.

@[simp]

theorem Polynomial.Monic.discr_ne_zero_iff {K : Type u_2} [Field K] {f : Polynomial K} (hf : f.Monic) : f.discr ≠ 0 ↔ f.Separable

Over a field, a monic polynomial is separable exactly when its discriminant is nonzero.

⚠ The field hypothesis is not decoration: Polynomial.not_separable_X_pow_two_sub_one records a monic polynomial over ℤ with nonzero discriminant that is not separable.

theorem Polynomial.discr_ne_zero_iff {K : Type u_2} [Field K] {f : Polynomial K} (hf : f ≠ 0) : f.discr ≠ 0 ↔ f.Separable

Over a field, a nonzero polynomial is separable exactly when its discriminant is nonzero.

The hypothesis f ≠ 0 cannot be dropped: the zero polynomial has discriminant 1 but is not separable.

@[simp]

theorem Polynomial.Monic.separable_map_iff_map_discr_ne_zero {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] {f : Polynomial R} (hf : f.Monic) (φ : R →+* K) : (Polynomial.map φ f).Separable ↔ φ f.discr ≠ 0

A monic polynomial becomes separable along a ring homomorphism into a field exactly when its discriminant does not become zero. No injectivity is needed: the discriminant commutes with base change because monicity preserves the degree.

@[simp]

theorem Polynomial.Monic.discr_ne_zero_iff_separable_map {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {f : Polynomial R} (hf : f.Monic) : f.discr ≠ 0 ↔ (Polynomial.map (algebraMap R K) f).Separable

Over a domain, the discriminant of a monic polynomial is nonzero exactly when the polynomial becomes separable over the fraction field: over a domain the separability criterion is the one formulated after passage to a fraction field.

@[simp]

theorem Polynomial.Monic.separable_map_zmod_iff_not_dvd_discr {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] : (Polynomial.map (Int.castRingHom (ZMod p)) f).Separable ↔ ¬↑p ∣ f.discr

A monic integral polynomial has separable reduction modulo a prime exactly when that prime does not divide its discriminant.

theorem Polynomial.Monic.isSquare_discr_map_rat_iff {f : Polynomial ℤ} (hf : f.Monic) : IsSquare (Polynomial.map (Int.castRingHom ℚ) f).discr ↔ IsSquare f.discr

The discriminant of a monic integral polynomial is a square in ℚ exactly when it is a square in ℤ.

The discriminant of a power basis

theorem Algebra.discr_powerBasis_eq_minpoly_discr {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) : discr K ⇑pb.basis = (minpoly K pb.gen).discr

For a finite field extension with a power basis, the algebra discriminant of the power basis is the polynomial discriminant of the minimal polynomial of its generator. Separability is not needed: without it both sides vanish, the left because the trace form is identically zero and the right because the minimal polynomial is inseparable.

The failure of the separability criterion over a ring

theorem Polynomial.discr_X_pow_two_sub_one : (X ^ 2 - 1).discr = 4

The discriminant of X ^ 2 - 1 over ℤ is 4.

theorem Polynomial.not_separable_X_pow_two_sub_one : ¬(X ^ 2 - 1).Separable

X ^ 2 - 1 is not separable over ℤ, although its discriminant 4 is nonzero. This is why Polynomial.Monic.discr_ne_zero_iff is stated over a field, and why the version over a domain passes to the fraction field.

Comparison with the discriminant of a cubic

@[simp]

theorem Cubic.toPoly_discr {R : Type u_1} [CommRing R] {P : Cubic R} (ha : P.a ≠ 0) : P.toPoly.discr = P.discr

For a cubic with nonzero leading coefficient, the discriminant in the sense of Cubic.discr is the discriminant of the associated degree-three polynomial. The two conventions agree on the nose, with no normalization to monic and no sign.

The discriminant of a monic quartic

theorem Polynomial.Monic.discr_of_natDegree_eq_four {R : Type u_1} [CommRing R] {f : Polynomial R} (hmonic : f.Monic) (hf : f.natDegree = 4) : f.discr = 256 * f.coeff 0 ^ 3 - 192 * f.coeff 3 * f.coeff 1 * f.coeff 0 ^ 2 - 128 * f.coeff 2 ^ 2 * f.coeff 0 ^ 2 + 144 * f.coeff 2 * f.coeff 1 ^ 2 * f.coeff 0 - 27 * f.coeff 1 ^ 4 + 144 * f.coeff 3 ^ 2 * f.coeff 2 * f.coeff 0 ^ 2 - 6 * f.coeff 3 ^ 2 * f.coeff 1 ^ 2 * f.coeff 0 - 80 * f.coeff 3 * f.coeff 2 ^ 2 * f.coeff 1 * f.coeff 0 + 18 * f.coeff 3 * f.coeff 2 * f.coeff 1 ^ 3 + 16 * f.coeff 2 ^ 4 * f.coeff 0 - 4 * f.coeff 2 ^ 3 * f.coeff 1 ^ 2 - 27 * f.coeff 3 ^ 4 * f.coeff 0 ^ 2 + 18 * f.coeff 3 ^ 3 * f.coeff 2 * f.coeff 1 * f.coeff 0 - 4 * f.coeff 3 ^ 3 * f.coeff 1 ^ 3 - 4 * f.coeff 3 ^ 2 * f.coeff 2 ^ 3 * f.coeff 0 + f.coeff 3 ^ 2 * f.coeff 2 ^ 2 * f.coeff 1 ^ 2

The discriminant of a monic quartic, expressed in terms of its coefficients.

theorem TauCeti.discr_depressedQuartic {R : Type u_1} [CommRing R] (p q r : R) : (Polynomial.X ^ 4 + Polynomial.C p * Polynomial.X ^ 2 + Polynomial.C q * Polynomial.X + Polynomial.C r).discr = 256 * r ^ 3 - 128 * p ^ 2 * r ^ 2 + 144 * p * q ^ 2 * r - 27 * q ^ 4 + 16 * p ^ 4 * r - 4 * p ^ 3 * q ^ 2

The discriminant of the depressed quartic X⁴ + pX² + qX + r.