Pure quintics and the Frobenius certificate for X⁵ - 2

A pure quintic X⁵ - a with a : ℤ that is irreducible over ℚ has the Frobenius group F₂₀ = AGL(1, 5) of order 20 as Galois group, the label 5T3. This module proves that from the resolvent data alone. The discriminant 3125a⁴ = 5(25a²)² is not a square in ℚ, and the resolvent sextic X⁶ - 3125a⁴X is separable with the rational root 0, which is the third row of the quintic decision table.

The Kummer example X⁵ - 2 is then certified by the Frobenius route: it is irreducible modulo 11, which does not divide its discriminant 50000 = 2⁴5⁵, that discriminant is not a square, and 0 is a root of its separable resolvent sextic X⁶ - 50000X.

Main results

• TauCeti.hasSexticRoot_X_pow_five_sub_C: for a ≠ 0, the integer 0 is a root of the separable resolvent sextic of X⁵ - a.
• TauCeti.hasGaloisLabel_X_pow_five_sub_C: for a : ℤ, a pure quintic X⁵ - a that is irreducible over ℚ has the label 5T3.
• Polynomial.factorDegrees_X_pow_five_sub_two_eleven: X⁵ - 2 is irreducible modulo 11.
• TauCeti.QuinticCertificate.check_X_pow_five_sub_two: the Frobenius-route certificate for X⁵ - 2 checks.
• TauCeti.hasGaloisLabel_X_pow_five_sub_two: X⁵ - 2 has Galois label 5T3, and TauCeti.natCard_gal_X_pow_five_sub_two: its Galois group has order 20.

References

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

Pure quintics

theorem TauCeti.hasSexticRoot_X_pow_five_sub_C {a : ℤ} (ha : a ≠ 0) : HasSexticRoot (Polynomial.X ^ 5 - Polynomial.C a) 0

For a ≠ 0, the integer 0 is a root of the resolvent sextic X⁶ - 3125a⁴X of the pure quintic X⁵ - a, and that sextic has nonzero discriminant.

theorem TauCeti.hasGaloisLabel_X_pow_five_sub_C {a : ℤ} (hirr : Irreducible (Polynomial.X ^ 5 - Polynomial.C ↑a)) : HasGaloisLabel (Polynomial.X ^ 5 - Polynomial.C ↑a) ⟨2, hasGaloisLabel_X_pow_five_sub_C._proof_1⟩

An irreducible pure quintic X⁵ - a with a : ℤ has the label 5T3. For an integer a with X⁵ - a irreducible over ℚ, the Galois group of X⁵ - a acting on its five roots is the Frobenius group F₂₀ = AGL(1, 5) of order 20: the discriminant 3125a⁴ is not a square, and the resolvent sextic X⁶ - 3125a⁴X is separable with the rational root 0.

The Kummer quintic X⁵ - 2

theorem TauCeti.discr_X_pow_five_sub_two : (Polynomial.X ^ 5 - 2).discr = 50000

The discriminant of X⁵ - 2 is 50000 = 2⁴ · 5⁵.

theorem Polynomial.factPrimeEleven : Fact (Nat.Prime 11)

theorem Polynomial.irreducible_X_pow_five_sub_two_zmod_eleven : Irreducible (X ^ 5 - 2)

The reduction of X⁵ - 2 modulo 11 is irreducible: 2 is not a fifth power in 𝔽₁₁.

@[simp]

theorem Polynomial.factorDegrees_X_pow_five_sub_two_eleven : (X ^ 5 - 2).factorDegrees 11 = {5}

X⁵ - 2 has a single irreducible factor of degree five modulo 11.

@[simp]

theorem TauCeti.QuinticCertificate.check_X_pow_five_sub_two : (frobeniusF20 11 0).check (Polynomial.X ^ 5 - 2) = true

The Frobenius-route certificate for X⁵ - 2 checks: it is irreducible modulo 11, which does not divide its discriminant 50000, the discriminant is not a square, and 0 is a root of its separable resolvent sextic X⁶ - 50000X.

theorem TauCeti.hasGaloisLabel_X_pow_five_sub_two : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - 2)) ⟨2, hasGaloisLabel_X_pow_five_sub_C._proof_1⟩

X⁵ - 2 has Galois label 5T3: its Galois group over ℚ is the Frobenius group F₂₀. This is the Kummer example.

theorem TauCeti.natCard_gal_X_pow_five_sub_two : Nat.card (Polynomial.X ^ 5 - 2).Gal = 20

The Galois group of X⁵ - 2 over ℚ has order 20.