A dihedral quintic certificate

The polynomial X⁵ - 5X - 12 has Galois group the dihedral group D₅ of order 10, the label 5T2; it defines the LMFDB number field 5.1.1000000.1. This module certifies that label by the dihedral route of TauCeti.QuinticCertificate:

• X⁵ - 5X - 12 is irreducible modulo 7, which makes the Galois action transitive;
• its discriminant is 8000² = 2¹² · 5⁶, a square, so the Galois group is even;
• its resolvent sextic X⁶ - 40X⁵ + 1000X⁴ - 20000X³ + 250000X² - 66400000X + 976000000 has the integral root 40 and is separable, since it is already separable modulo 7; so the Galois group lies in a conjugate of F₂₀;
• modulo 3 it factors as X (X² + X + 2) (X² + 2X + 2), of type (1,2,2), which exhibits an element of order two in the Galois group, and so rules out the cyclic label 5T1.

The discriminant and the sextic alone do not separate 5T1 from 5T2: the cyclic quintic X⁵ + X⁴ - 4X³ - 3X² + 3X + 1 also has a square discriminant and a separable resolvent sextic with an integral root. The factorization of type (1,2,2) is the datum that does. Conversely, every factorization type of X⁵ - 5X - 12 at a good prime is a cycle type of D₅ ≤ A₅, so no factorization excludes A₅; that upper bound comes from the sextic (TauCeti.factorDegrees_do_not_distinguish_D5_A5).

Main results

• TauCeti.discr_X_pow_five_sub_five_mul_X_sub_twelve: the discriminant is 8000².
• TauCeti.hasSexticRoot_X_pow_five_sub_five_mul_X_sub_twelve: 40 is a root of the separable resolvent sextic.
• Polynomial.factorDegrees_X_pow_five_sub_five_mul_X_sub_twelve_seven: the reduction modulo 7 is irreducible.
• Polynomial.factorDegrees_X_pow_five_sub_five_mul_X_sub_twelve_three: the reduction modulo 3 has factor degrees (1,2,2).
• TauCeti.QuinticCertificate.check_X_pow_five_sub_five_mul_X_sub_twelve: the dihedral-route certificate checks.
• TauCeti.hasGaloisLabel_X_pow_five_sub_five_mul_X_sub_twelve: X⁵ - 5X - 12 has label 5T2, and TauCeti.natCard_gal_X_pow_five_sub_five_mul_X_sub_twelve: its Galois group has order 10.
• TauCeti.factorDegrees_do_not_distinguish_D5_A5: every factorization type of X⁵ - 5X - 12 at a good prime is the full cycle type of an even permutation, although the Galois image does not contain A₅.

References

• D. S. Dummit, Solving solvable quintics, Mathematics of Computation 57 (1991), 387–401.

theorem TauCeti.discr_X_pow_five_sub_five_mul_X_sub_twelve : (Polynomial.X ^ 5 - 5 * Polynomial.X - 12).discr = 8000 ^ 2

The discriminant of X⁵ - 5X - 12 is 8000² = 2¹² · 5⁶.

theorem TauCeti.hasSexticRoot_X_pow_five_sub_five_mul_X_sub_twelve : HasSexticRoot (Polynomial.X ^ 5 - 5 * Polynomial.X - 12) 40

The integer 40 is a root of the resolvent sextic of X⁵ - 5X - 12, and that sextic has nonzero discriminant: its reduction modulo 7 is already separable.

theorem Polynomial.fact_prime_seven_dihedral : Fact (Nat.Prime 7)

theorem Polynomial.irreducible_X_pow_five_sub_five_mul_X_sub_twelve_zmod_seven : Irreducible (X ^ 5 - 5 * X - 12)

The reduction of X⁵ - 5X - 12 modulo 7 is irreducible: it has no root and no monic quadratic factor in 𝔽₇.

@[simp]

theorem Polynomial.factorDegrees_X_pow_five_sub_five_mul_X_sub_twelve_seven : (X ^ 5 - 5 * X - 12).factorDegrees 7 = {5}

X⁵ - 5X - 12 has a single irreducible factor of degree five modulo 7.

@[simp]

theorem Polynomial.factorDegrees_X_pow_five_sub_five_mul_X_sub_twelve_three : (X ^ 5 - 5 * X - 12).factorDegrees 3 = {1, 2, 2}

The reduction of X⁵ - 5X - 12 modulo 3 is X (X² + X + 2) (X² + 2X + 2), with factor degrees {1, 2, 2}.

@[simp]

theorem TauCeti.QuinticCertificate.check_X_pow_five_sub_five_mul_X_sub_twelve : (dihedral 7 3 8000 40).check (Polynomial.X ^ 5 - 5 * Polynomial.X - 12) = true

The dihedral-route certificate for X⁵ - 5X - 12 checks: it is irreducible modulo 7, its discriminant is 8000², 40 is a root of its separable resolvent sextic, and it has factor degrees (1,2,2) modulo 3. Neither 7 nor 3 divides the discriminant.

theorem TauCeti.hasGaloisLabel_X_pow_five_sub_five_mul_X_sub_twelve : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)) ⟨1, hasGaloisLabel_X_pow_five_sub_five_mul_X_sub_twelve._proof_1⟩

X⁵ - 5X - 12 has Galois label 5T2: its Galois group over ℚ is the dihedral group D₅ of order 10.

theorem TauCeti.natCard_gal_X_pow_five_sub_five_mul_X_sub_twelve : Nat.card (Polynomial.X ^ 5 - 5 * Polynomial.X - 12).Gal = 10

The Galois group of X⁵ - 5X - 12 over ℚ has order 10.

theorem TauCeti.factSplitsSplittingField_dihedral (f : Polynomial ℚ) : Fact (Polynomial.map (algebraMap ℚ f.SplittingField) f).Splits

theorem TauCeti.factorDegrees_do_not_distinguish_D5_A5 : (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ¬↑p ∣ (Polynomial.X ^ 5 - 5 * Polynomial.X - 12).discr → ∃ σ ∈ alternatingGroup ↑((Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)).rootSet ℂ), σ.fullCycleType = (Polynomial.X ^ 5 - 5 * Polynomial.X - 12).factorDegrees p) ∧ ¬alternatingGroup ↑((Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)).rootSet ℂ) ≤ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)) ℂ).range

Factorization types do not separate D₅ from A₅. At every prime p not dividing the discriminant, the degrees of the irreducible factors of X⁵ - 5X - 12 modulo p are the full cycle type of an even permutation of its complex roots; yet its Galois image, the dihedral group of order 10, does not contain the alternating group. So no factorization type of this polynomial, at any good prime, rules out the label 5T4: factorization types only exhibit elements of the Galois image, and every element of D₅ lies in A₅. The upper bound that excludes A₅ comes from the root 40 of the resolvent sextic instead.