Monic cubics with a triple root

A monic cubic X³ + b X² + c X + d is the cube (X - ρ)³ exactly when b = -3ρ, c = 3ρ² and d = -ρ³. Over a perfect field the existence of such a ρ can be read off the coefficients without naming it: it holds exactly when

b² = 3 c, c² = 3 b d, b c = 9 d,

that is, when the quadratic covariant (b² - 3c) x² + (bc - 9d) x y + (c² - 3bd) y² of the binary cubic form x³ + b x² y + c x y² + d y³ vanishes; away from characteristic 2 this covariant is -1/4 times the Hessian of the form. The criterion holds in every characteristic. Away from characteristic 3 the root is ρ = -b / 3. In characteristic 3 the conditions say b = c = 0, and the root is a cube root of -d, which exists because the field is perfect. Over the imperfect field 𝔽₃(s) the cubic X³ - s satisfies the conditions but is not the cube of a linear polynomial.

This is the triple-root test of Tate's algorithm (Steps 6 to 8), applied to the residue cubic of a Weierstrass equation over a discrete valuation ring.

Main results

• TauCeti.Polynomial.cubic_eq_X_sub_C_pow_three_iff: over a commutative ring, X³ + b X² + c X + d = (X - ρ)³ exactly when b = -3ρ, c = 3ρ² and d = -ρ³.
• TauCeti.Polynomial.exists_cubic_eq_X_sub_C_pow_three_iff: over a perfect field, X³ + b X² + c X + d is the cube of a monic linear polynomial exactly when b² = 3c, c² = 3bd and bc = 9d.

theorem TauCeti.Polynomial.cubic_eq_X_sub_C_pow_three_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 ρ) ^ 3 ↔ b = -3 * ρ ∧ c = 3 * ρ ^ 2 ∧ d = -ρ ^ 3

A monic cubic X³ + b X² + c X + d over a commutative ring is the cube (X - ρ)³ exactly when b = -3ρ, c = 3ρ² and d = -ρ³.

theorem TauCeti.Polynomial.exists_cubic_eq_X_sub_C_pow_three_iff {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) ↔ b ^ 2 = 3 * c ∧ c ^ 2 = 3 * b * d ∧ b * c = 9 * d

The triple-root test for a monic cubic. Over a perfect field k, the cubic X³ + b X² + c X + d is (X - ρ)³ for some ρ ∈ k exactly when b² = 3c, c² = 3bd and bc = 9d. Perfectness is needed only in characteristic 3, where the conditions reduce to b = c = 0 and ρ is a cube root of -d.