Solvability of a quintic from its resolvent sextic

Let f be a monic irreducible separable quintic over a field F. The Galois group of f is solvable exactly when its permutation image on the five roots lies in a conjugate of the Frobenius group F₂₀ = 5T3. The resolvent attached to TauCeti.quinticF20Spec detects exactly that containment: provided the specialized resolvent is separable, it has a root in F if and only if the image lies in a conjugate of F₂₀.

Thus a separable specialized resolvent has a root in the base field exactly when the polynomial Galois group is solvable. Separability of f does not imply separability of the resolvent and cannot replace that hypothesis: specialization can make distinct values of the six universal orbit elements collide.

No characteristic restriction is needed for this group-and-resolvent statement. Restrictions on characteristics two and five enter the separate discriminant and depression arguments, not the exact-stabilizer criterion used here.

Main results

• TauCeti.exists_isRoot_specialize_quinticF20Spec_of_isSolvable: a solvable Galois group gives the F₂₀ resolvent a root in the base field, with no hypothesis on the resolvent.
• TauCeti.isSolvable_gal_iff_exists_isRoot_specialize_quinticF20Spec: the Galois group of an irreducible separable quintic is solvable exactly when its separable F₂₀ resolvent has a root in the base field.

References

• D. S. Dummit, Solving solvable quintics, Mathematics of Computation 57 (1991), Theorem 1. The separability hypothesis here makes explicit the distinct-value condition used when a resolvent root is read as containment in an invariant's stabilizer.

theorem TauCeti.exists_isRoot_specialize_quinticF20Spec_of_isSolvable {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (hsol : Group.IsSolvable f.Gal) : ∃ (a : F), (quinticF20Spec.specialize F f).IsRoot a

A solvable quintic Galois group gives the resolvent a root. Let f be a monic irreducible separable quintic over a field. If the polynomial Galois group is solvable, then the specialization of Dummit's F₂₀ resolvent has a root in the base field.

Nothing is assumed about the resolvent here; the converse direction, in TauCeti.isSolvable_gal_iff_exists_isRoot_specialize_quinticF20Spec, does assume its separability.

theorem TauCeti.isSolvable_gal_iff_exists_isRoot_specialize_quinticF20Spec {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (hres : (quinticF20Spec.specialize F f).Separable) : Group.IsSolvable f.Gal ↔ ∃ (a : F), (quinticF20Spec.specialize F f).IsRoot a

The quintic resolvent solvability criterion. Let f be a monic irreducible separable quintic over a field. If the specialization of Dummit's F₂₀ resolvent is separable, then the polynomial Galois group is solvable if and only if that resolvent has a root in the base field.