Square discriminant and a sextic root do not separate 5T1 from 5T2

For an irreducible quintic, a square discriminant together with a rational root of a separable resolvent sextic confines the Galois group to a conjugate of F₂₀ ∩ A₅ = D₅, so the label is 5T1 or 5T2. This file shows that these two yes/no tests, "the discriminant is a square" and "the resolvent sextic is separable and has a rational root", do not determine which of the two labels holds. The cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1, which defines the maximal real subfield of ℚ(ζ₁₁) and has label 5T1, and the dihedral quintic X⁵ - 5X - 12, which has label 5T2, both pass both tests: their discriminants are the squares 121² and 8000², and their resolvent sextics are separable with the integral roots -16 and 40. Separating the two labels takes a further datum, such as a factorization of type (1,2,2) modulo a good prime or a second root in the field generated by one root, which is what the dihedral and cyclic quintic certificates carry.

Main results

• TauCeti.discriminant_and_sextic_do_not_distinguish_C5_D5: the two quintics both pass the square-discriminant test and the separable-sextic-root test, and have the different labels 5T1 and 5T2.

References

• D. S. Dummit, Solving solvable quintics, Mathematics of Computation 57 (1991), 387–401.
• H. Cohen, A Course in Computational Algebraic Number Theory, Springer 1993, §6.3.

theorem TauCeti.discriminant_and_sextic_do_not_distinguish_C5_D5 : (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1).discr = 121 ^ 2 ∧ (Polynomial.X ^ 5 - 5 * Polynomial.X - 12).discr = 8000 ^ 2 ∧ Polynomial.eval (-16) (resolventSextic (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1)) = 0 ∧ Polynomial.eval 40 (resolventSextic (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)) = 0 ∧ (resolventSextic (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1)).discr ≠ 0 ∧ (resolventSextic (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)).discr ≠ 0 ∧ HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1)) ⟨0, discriminant_and_sextic_do_not_distinguish_C5_D5._proof_1⟩ ∧ HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)) ⟨1, discriminant_and_sextic_do_not_distinguish_C5_D5._proof_2⟩

Square discriminant and a sextic root do not separate 5T1 from 5T2. The cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1 and the dihedral quintic X⁵ - 5X - 12 both have square discriminant, 121² and 8000², and both have a resolvent sextic with nonzero discriminant and an integral root, -16 and 40. Yet the first has label 5T1 and the second label 5T2, and a quintic carries at most one label (TauCeti.HasGaloisLabel.eq_of, with the classification of the transitive subgroups of S₅). So the yes/no properties "the discriminant is a square" and "the resolvent sextic is separable and has a rational root" do not determine whether the label of a quintic is 5T1 or 5T2.