Soundness of the quintic certificate routes

A monic integral quintic f that is irreducible over ℚ carries exactly one of the transitive-group labels 5T1, …, 5T5. This file shows how finite evidence about f determines that label. Each theorem is one sound route from evidence to a label:

route	evidence besides irreducibility over ℚ	label
cyclic	a second root of f in ℚ[X]/(f)	5T1
dihedral	disc f a square, a root of the separable sextic, factor degrees (1,2,2)	5T2
Frobenius	disc f not a square, a root of the separable sextic	5T3
alternating	disc f a square, factor degrees (1,1,3)	5T4
symmetric	factor degrees (2,3)	5T5

Here "the separable sextic" is the integral resolvent sextic TauCeti.resolventSextic f with nonzero discriminant, as packaged by TauCeti.HasSexticRoot, and factor degrees are taken modulo a prime not dividing disc f, as packaged by TauCeti.HasFactorDegrees. Irreducibility over ℚ is what makes the Galois action transitive; finite evidence for it is an irreducible reduction modulo some prime, through TauCeti.HasFactorDegrees.irreducible_map_rat, and the degree is then read off by TauCeti.HasFactorDegrees.sum_eq_natDegree.

A second root in the field generated by one root gives that field a nonidentity automorphism, so the root field is Galois of degree five and the Galois group is cyclic of order five. The discriminant and the sextic bound the Galois group from above, while a factorization modulo a good prime exhibits an element of the Galois group and so bounds it from below. The discriminant and the sextic alone do not separate 5T1 from 5T2; in the dihedral route, factor degrees (1,2,2) exhibit an element of order two, which the cyclic group of order five does not have. In the alternating route, factor degrees (1,1,3) exhibit an element of order three, which leaves only 5T4 and 5T5, and the square discriminant excludes 5T5. In the symmetric route, factor degrees (2,3) exhibit an element whose cube is a transposition, and a transitive group of prime degree containing a transposition is the full symmetric group.

Main results

• TauCeti.hasGaloisLabel_five_zero_of_hasSecondRootInRootField: the cyclic route.
• TauCeti.hasGaloisLabel_five_one_of_isSquare_discr_of_hasSexticRoot_of_hasFactorDegrees: the dihedral route.
• TauCeti.hasGaloisLabel_five_two_of_not_isSquare_discr_of_hasSexticRoot: the Frobenius route.
• TauCeti.hasGaloisLabel_five_three_of_isSquare_discr_of_hasFactorDegrees: the alternating route.
• TauCeti.hasGaloisLabel_five_four_of_hasFactorDegrees: the symmetric route.

References

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

theorem TauCeti.hasGaloisLabel_five_zero_of_hasSecondRootInRootField {f : Polynomial ℤ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (hdeg : f.natDegree = 5) {b : Polynomial ℚ} (hb : HasSecondRootInRootField f b) : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) ⟨0, hasGaloisLabel_five_zero_of_hasSecondRootInRootField._proof_1⟩

The cyclic route: 5T1. A monic integral quintic, irreducible over ℚ, with formal evidence for a second root in ℚ[X]/(f), the field generated by one of its roots, has the cyclic group of order five on its five roots.

theorem TauCeti.hasGaloisLabel_five_one_of_isSquare_discr_of_hasSexticRoot_of_hasFactorDegrees {f : Polynomial ℤ} {q : ℕ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (hdisc : IsSquare f.discr) {a : ℤ} (ha : HasSexticRoot f a) (hq : HasFactorDegrees f q {1, 2, 2}) : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) ⟨1, hasGaloisLabel_five_one_of_isSquare_discr_of_hasSexticRoot_of_hasFactorDegrees._proof_1⟩

The dihedral route: 5T2. A monic integral quintic, irreducible over ℚ, whose discriminant is a square, whose resolvent sextic is separable with an integral root, and whose factor degrees modulo a prime not dividing its discriminant are (1,2,2), has the dihedral group of order ten on its five roots.

theorem TauCeti.hasGaloisLabel_five_two_of_not_isSquare_discr_of_hasSexticRoot {f : Polynomial ℤ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (hdeg : f.natDegree = 5) (hdisc : ¬IsSquare f.discr) {a : ℤ} (ha : HasSexticRoot f a) : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) ⟨2, hasGaloisLabel_five_two_of_not_isSquare_discr_of_hasSexticRoot._proof_1⟩

The Frobenius route: 5T3. A monic integral quintic, irreducible over ℚ, whose discriminant is not a square, and whose resolvent sextic is separable with an integral root, has the Frobenius group of order twenty on its five roots.

theorem TauCeti.hasGaloisLabel_five_three_of_isSquare_discr_of_hasFactorDegrees {f : Polynomial ℤ} {q : ℕ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (hdisc : IsSquare f.discr) (hq : HasFactorDegrees f q {1, 1, 3}) : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) ⟨3, hasGaloisLabel_five_three_of_isSquare_discr_of_hasFactorDegrees._proof_1⟩

The alternating route: 5T4. A monic integral quintic, irreducible over ℚ, whose discriminant is a square, and whose factor degrees modulo a prime not dividing its discriminant are (1,1,3), has the alternating group on its five roots.

theorem TauCeti.hasGaloisLabel_five_four_of_hasFactorDegrees {f : Polynomial ℤ} {q : ℕ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (hq : HasFactorDegrees f q {2, 3}) : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) ⟨4, hasGaloisLabel_five_four_of_hasFactorDegrees._proof_1⟩

The symmetric route: 5T5. A monic integral quintic, irreducible over ℚ, whose factor degrees modulo a prime not dividing its discriminant are (2,3), has the full symmetric group on its five roots.