The resolvent sextic of a pure quintic

For every integer a, the resolvent sextic of the pure quintic X⁵ - a is X⁶ - 3125a⁴X. This is Dummit's closed formula for the resolvent sextic of the trinomial X⁵ + aX + b (TauCeti.resolventSextic_X_pow_five_add_C_mul_X_add_C) read at X⁵ + 0·X + (-a), and it exhibits 0 as an integral root.

For a ≠ 0 the sextic is separable over ℚ, being the product of X and the binomial X⁵ - 3125a⁴, and its root 0 is therefore separation evidence for the pure quintic.

Main results

• TauCeti.resolventSextic_X_pow_five_sub_C: the resolvent sextic of X⁵ - a is X⁶ - 3125a⁴X; TauCeti.resolventSextic_X_pow_five_sub_intCast is its simp normal form.
• TauCeti.separable_map_resolventSextic_X_pow_five_sub_C: for a ≠ 0, that sextic is separable over ℚ.

References

• D. S. Dummit, Solving solvable quintics, Mathematics of Computation 57 (1991), §1, formula (2′).

theorem TauCeti.resolventSextic_X_pow_five_sub_C (a : ℤ) : resolventSextic (Polynomial.X ^ 5 - Polynomial.C a) = Polynomial.X ^ 6 - Polynomial.C (3125 * a ^ 4) * Polynomial.X

The resolvent sextic of a pure quintic. For every integer a, resolventSextic (X⁵ - a) = X⁶ - 3125a⁴X. This is Dummit's closed formula for the resolvent sextic of X⁵ + aX + b in the case a = 0, and it exhibits 0 as an integral root.

@[simp]

theorem TauCeti.resolventSextic_X_pow_five_sub_intCast (a : ℤ) : resolventSextic (Polynomial.X ^ 5 - ↑a) = Polynomial.X ^ 6 - 3125 * ↑a ^ 4 * Polynomial.X

The resolvent sextic of a pure quintic in simp normal form: over ℤ, the constant C a is the cast ↑a, and resolventSextic (X⁵ - a) = X⁶ - 3125a⁴X.

theorem TauCeti.separable_map_resolventSextic_X_pow_five_sub_C {a : ℤ} (ha : a ≠ 0) : (Polynomial.map (Int.castRingHom ℚ) (resolventSextic (Polynomial.X ^ 5 - Polynomial.C a))).Separable

Over ℚ, the resolvent sextic X⁶ - 3125a⁴X of a pure quintic X⁵ - a with a ≠ 0 is separable, so its root 0 is separation evidence for the quintic certificate.