Good and bad reductions of quintic resolvents

The prime 3 is good for both X⁵ - 2 and its sextic resolvent. In contrast, it is good for X⁵ - 5X - 12 but bad for that polynomial's sextic resolvent: the latter reduces to (X - 1)⁴ (X² + 1). The sextic is separable over ℚ, so the collision is introduced by reduction, rather than being inherited from characteristic zero.

These examples show why avoiding the discriminant of the original polynomial does not suffice to apply a resolvent subgroup test over the residue field.

References

• D. S. Dummit, Solving solvable quintics, Mathematics of Computation 57 (1991), equations (2) and (2′), for the sextics used here.

theorem TauCeti.isGoodPrime_quinticF20Spec_X_pow_five_sub_two_three : quinticF20Spec.IsGoodPrime (Polynomial.X ^ 5 - 2) 3

The prime 3 preserves separability of the pure quintic X⁵ - 2 and its sextic resolvent.

theorem TauCeti.map_resolventSextic_X_pow_five_sub_five_mul_X_sub_twelve_three : Polynomial.map (Int.castRingHom (ZMod 3)) (resolventSextic (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)) = (Polynomial.X - 1) ^ 4 * (Polynomial.X ^ 2 + 1)

Modulo 3, the sextic of X⁵ - 5X - 12 develops a quadruple root at 1.

theorem TauCeti.isGoodPrime_and_not_isGoodPrime_quinticF20Spec_X_pow_five_sub_five_mul_X_sub_twelve : IsGoodPrime (Polynomial.X ^ 5 - 5 * Polynomial.X - 12) 3 ∧ ¬quinticF20Spec.IsGoodPrime (Polynomial.X ^ 5 - 5 * Polynomial.X - 12) 3

Although 3 avoids the quintic discriminant, it does not avoid the sextic discriminant. The resolvent over ℚ is separable, but its reduction is not.