Separability and splitting criteria for quadratic polynomials #
Mathlib's Mathlib/Algebra/QuadraticDiscriminant.lean works with the equation
a x² + b x + c = 0 and relates its solutions to discrim a b c = b² - 4 a c. This file reads
those facts back as statements about the polynomial C a * X ^ 2 + C b * X + C c. Wherever a
statement mentions the discriminant it uses Mathlib's discrim rather than its expansion, so
that Mathlib's discriminant API applies to it directly; the two criteria phrased by a root or by
an Artin-Schreier condition mention no discriminant at all.
Over an ordered commutative ring, TauCeti.quadratic_pos_iff_of_discrim_neg and
TauCeti.quadratic_neg_iff_of_discrim_neg identify the sign of a quadratic with negative
discriminant from its leading coefficient.
Over a field, with a ≠ 0:
Polynomial.separable_quadratic_iff_discrim_ne_zero: separable exactly whendiscrim a b c ≠ 0;Polynomial.splits_quadratic_iff_exists_root: splits exactly when it has a root — the characteristic-free core the other two are read off from;Polynomial.splits_quadratic_iff_isSquare: away from characteristic two, splits exactly whendiscrim a b cis a square;Polynomial.splits_quadratic_of_discrim_eq_zero: over a perfect field, splits as soon asdiscrim a b c = 0;Polynomial.card_rootSet_quadratic_of_discrim_eq_zero: if it splits anddiscrim a b c = 0, it has exactly one root;Polynomial.splits_quadratic_iff_exists_artinSchreier_of_two_eq_zero: in characteristic two, where the discriminant degenerates tob²(discrim_eq_sq_of_two_eq_zero) and the square-class criterion says nothing, splits exactly when the Artin-Schreier invarianta c / b²lies in the image ofz ↦ z² + z, written division-free. Hereb ≠ 0is also required, which byseparable_quadratic_iff_discrim_ne_zerois separability.
Three statements need neither a field nor a ≠ 0, and are stated over a commutative (semi)ring:
Polynomial.derivative_quadratic, computing the derivative as 2 a X + b; the Bézout-type
Polynomial.sq_derivative_quadratic_sub_mul_eq_C_discrim, (P')² - 4 a P = C (discrim a b c); and
its consequence Polynomial.separable_quadratic_of_isUnit_discrim, that the quadratic is separable
whenever its discriminant is a unit. Over a field that last statement is one direction of
Polynomial.separable_quadratic_iff_discrim_ne_zero, in every characteristic.
The two splitting criteria are consumed by the node-polynomial criteria of
TauCeti/AlgebraicGeometry/EllipticCurve/NodePolynomial.lean, which advance
TauCetiRoadmap/EllipticCurves/README.md §Layer 5 (twists): whether the node polynomial of a
multiplicative reduction splits over the residue field is exactly whether that reduction is split.
Adapted from the FLT project (ImperialCollegeLondon/FLT,
FLT/Mathlib/Algebra/Polynomial/QuadraticDiscriminant.lean at the roadmap's pin bc2fe8ff7396,
FLT PR #1088, Apache 2.0). That file's own header reads Authors: Kevin Buzzard, Claude;
following this repository's convention for adapted material, the upstream authorship is credited
here rather than in the copyright header. Ported with the source's @[expose] dropped, and
without its companion FLT/Mathlib/Algebra/Polynomial/Splits.lean: that file's
Splits.of_natDegree_le_two_of_isRoot is superseded here by Mathlib's own
Polynomial.Splits.of_natDegree_eq_two, which the one consumer can use directly since it knows
the degree is exactly two.
In characteristic two the discriminant degenerates to b², since 4 = 0 kills the a c
term. This is why splits_quadratic_iff_isSquare says nothing there: discrim a b c is
automatically a square.
The Bézout-type identity (P')² - 4 a · P = C (discrim a b c) for the quadratic
P = a X² + b X + c: the discriminant is an explicit R[X]-combination of P and its
derivative, which is what makes it a coprimality witness in
separable_quadratic_of_isUnit_discrim.
A quadratic a X² + b X + c over any commutative ring is separable as soon as discrim a b c
is a unit. No hypothesis on a is needed: once the discriminant is inverted, the Bézout-type
identity sq_derivative_quadratic_sub_mul_eq_C_discrim writes 1 as an R[X]-combination of the
polynomial and its derivative.
A quadratic polynomial a X² + b X + c (with a ≠ 0) over a field is separable exactly when
discrim a b c is nonzero. This holds in every characteristic; contrast
splits_quadratic_iff_isSquare, which asks for the discriminant to be a square rather than
nonzero, and only away from characteristic two. The reverse direction needs neither a field nor
a ≠ 0: it is separable_quadratic_of_isUnit_discrim.
A quadratic a X² + b X + c (a ≠ 0) over a field splits exactly when it has a root. This is
the characteristic-free core of the two split criteria below, which only restate "has a root":
splits_quadratic_iff_isSquare in terms of the discriminant, and
splits_quadratic_iff_exists_artinSchreier_of_two_eq_zero in terms of the Artin-Schreier
invariant a c / b².
Over a field of characteristic ≠ 2, a quadratic a X² + b X + c (with a ≠ 0) splits
exactly when discrim a b c is a square. Compare separable_quadratic_iff_discrim_ne_zero,
which asks for the discriminant to be nonzero rather than square, and holds in every
characteristic.
Over a field of characteristic 2, a quadratic a X² + b X + c with a, b ≠ 0 splits
exactly when its Artin-Schreier invariant a c / b² lies in the image of z ↦ z² + z, written
division-free as ∃ z, b² (z² + z) = a c. Here the square-class criterion
splits_quadratic_iff_isSquare says nothing, since discrim a b c = b² is automatically a
square; the hypothesis b ≠ 0 is
exactly separability, by separable_quadratic_iff_discrim_ne_zero.
Over a perfect field, a quadratic a X² + b X + c (with a ≠ 0) whose discriminant vanishes
splits. Perfectness is needed in characteristic two, where X² - c can have vanishing
discriminant without a root.
A quadratic with negative discriminant is positive at every argument exactly when its leading coefficient is positive.
With negative discriminant, a quadratic is negative everywhere exactly when its leading coefficient is negative.