Repeated roots of monic cubics over perfect fields

A monic cubic over a perfect field has zero discriminant exactly when it factors as (X - ρ)² (X - σ) with both roots in the ground field. This gives the three branches of the residue-cubic test in Tate's algorithm: nonzero discriminant, a double root and a distinct simple root, or a triple root.

The covariant b² - 3c distinguishes the last two branches for X³ + b X² + c X + d: in the repeated-root factorization it is (ρ - σ)². The characteristic 2 and 3 cases are included. Perfectness supplies square roots in characteristic 2 and cube roots in characteristic 3.

References

• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9, the residue cubic in Steps 6–8 of Tate's algorithm.

theorem TauCeti.Polynomial.cubic_eq_X_sub_C_sq_mul_X_sub_C_iff {R : Type u_1} [CommRing R] {b c d ρ σ : R} : Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d = (Polynomial.X - Polynomial.C ρ) ^ 2 * (Polynomial.X - Polynomial.C σ) ↔ b = -(ρ + ρ + σ) ∧ c = ρ * ρ + ρ * σ + ρ * σ ∧ d = -(ρ * ρ * σ)

The coefficients of a monic cubic with a specified repeated root and remaining root.

theorem TauCeti.Polynomial.exists_cubic_eq_X_sub_C_pow_three_iff_discr_eq_zero_and_b_sq_eq_three_c {k : Type u_1} [Field k] [PerfectField k] {b c d : k} : (∃ (ρ : k), Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d = (Polynomial.X - Polynomial.C ρ) ^ 3) ↔ { a := 1, b := b, c := c, d := d }.discr = 0 ∧ b ^ 2 = 3 * c

A monic cubic over a perfect field is a cube of a monic linear polynomial exactly when its discriminant and quadratic covariant both vanish. These are the triple-root branch tests of the residue-cubic classification.

theorem TauCeti.Polynomial.cubic_discr_eq_zero_iff {k : Type u_1} [Field k] [PerfectField k] {b c d : k} : { a := 1, b := b, c := c, d := d }.discr = 0 ↔ ∃ (ρ : k) (σ : k), Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d = (Polynomial.X - Polynomial.C ρ) ^ 2 * (Polynomial.X - Polynomial.C σ)

A monic cubic over a perfect field has zero discriminant exactly when it has a repeated root in that field. In this case the remaining root is rational as well.

theorem TauCeti.Polynomial.exists_cubic_eq_X_sub_C_sq_mul_X_sub_C_iff {k : Type u_1} [Field k] [PerfectField k] {b c d : k} : (∃ (ρ : k) (σ : k), ρ ≠ σ ∧ Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d = (Polynomial.X - Polynomial.C ρ) ^ 2 * (Polynomial.X - Polynomial.C σ)) ↔ { a := 1, b := b, c := c, d := d }.discr = 0 ∧ b ^ 2 ≠ 3 * c

A monic cubic over a perfect field has a double root distinct from its simple root exactly when its discriminant vanishes and b² - 3c does not vanish.

theorem TauCeti.Polynomial.cubic_root_trichotomy {k : Type u_1} [Field k] [PerfectField k] {b c d : k} : { a := 1, b := b, c := c, d := d }.discr ≠ 0 ∨ (∃ (ρ : k) (σ : k), ρ ≠ σ ∧ Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d = (Polynomial.X - Polynomial.C ρ) ^ 2 * (Polynomial.X - Polynomial.C σ)) ∨ ∃ (ρ : k), Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d = (Polynomial.X - Polynomial.C ρ) ^ 3

The residue-cubic trichotomy: a monic cubic over a perfect field has nonzero discriminant, one double and one distinct simple root, or a triple root. The first case does not assert that the cubic splits over the ground field.