A cyclic quintic certificate

The polynomial X⁵ + X⁴ - 4X³ - 3X² + 3X + 1 is irreducible modulo 2. Together with its second root X² - 2 in the root field, this supplies a cyclic-route certificate and proves that its Galois group has label 5T1. This polynomial defines the LMFDB number field 5.5.14641.1.

The file also computes the discriminant and the resolvent sextic of this quintic. Its roots are 2 cos (2πk/11), and if θ is one of them then so is θ² - 2; iterating, the five roots are polynomials of degree at most four in θ. The discriminant and the six values of Dummit's F₂₀-invariant at these roots are then polynomials in θ. Reduced modulo the quintic, the product of the differences of the roots is -121, and the six values become explicit elements of ℚ(θ). One of them is -16, and they are pairwise distinct because 1, θ, θ², θ³, θ⁴ are linearly independent over ℚ, the quintic being irreducible. So the resolvent sextic splits over ℚ(θ) with distinct roots, one of them -16. Every reduction modulo the quintic is a linear_combination with an explicit quotient.

Main results

• TauCeti.hasSecondRootInRootField_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1: the second-root evidence.
• Polynomial.irreducible_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1_zmod_two: the irreducible reduction at 2.
• Polynomial.factorDegrees_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1_two: the factor degrees at 2.
• TauCeti.QuinticCertificate.check_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1: the certificate checks.
• TauCeti.hasGaloisLabel_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1: the Galois label is 5T1.
• TauCeti.discr_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1: the discriminant is 121² = 11⁴.
• TauCeti.hasSexticRoot_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1: -16 is a root of the resolvent sextic, which is separable.

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.hasSecondRootInRootField_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1 : HasSecondRootInRootField (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1) (Polynomial.X ^ 2 - 2)

The polynomial X² - 2 supplies formal second-root evidence for the cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1. For this monic irreducible quintic, it represents a second root in the field generated by one root.

theorem Polynomial.irreducible_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1_zmod_two : Irreducible (X ^ 5 + X ^ 4 + X ^ 2 + X + 1)

The reduction of the cyclic quintic modulo 2 is irreducible.

@[simp]

theorem Polynomial.factorDegrees_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1_two : (X ^ 5 + X ^ 4 - 4 * X ^ 3 - 3 * X ^ 2 + 3 * X + 1).factorDegrees 2 = {5}

The cyclic quintic has a single irreducible factor of degree five modulo 2.

@[simp]

theorem TauCeti.QuinticCertificate.check_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1 : (cyclic 2 (Polynomial.X ^ 2 - 2)).check (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1) = true

The cyclic-route certificate for the cyclic quintic checks.

theorem TauCeti.hasGaloisLabel_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1 : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1)) ⟨0, hasGaloisLabel_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1._proof_1⟩

The cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1 has Galois label 5T1.

The roots of the cyclic quintic over ℂ

The discriminant

theorem TauCeti.discr_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1 : (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1).discr = 121 ^ 2

The discriminant of the cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1 is 121² = 11⁴, a square: the Galois group C₅ consists of even permutations.

The resolvent sextic

theorem TauCeti.hasSexticRoot_X5_add_X4_sub_4X3_sub_3X2_add_3X_add_1 : HasSexticRoot (Polynomial.X ^ 5 + Polynomial.X ^ 4 - 4 * Polynomial.X ^ 3 - 3 * Polynomial.X ^ 2 + 3 * Polynomial.X + 1) (-16)

The integer -16 is a root of the resolvent sextic of the cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1, and that sextic has nonzero discriminant: over ℚ(θ), for a root θ of the quintic, it splits into six distinct linear factors.