A collision in the quintic resolvent

The quintic X⁵ - X is separable (with discriminant -256), while Dummit's sextic resolvent is (X - 2)⁴ (X² + 16) and is inseparable with rational root 2. Its Galois image nevertheless lies in no conjugate of the Frobenius group F₂₀: complex conjugation fixes the roots 0, ±1 and exchanges ±i, so it acts as a transposition, and F₂₀ contains no transposition.

So X⁵ - X satisfies every hypothesis of TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize for the F₂₀ specification, except separability of the specialized resolvent, and the conclusion fails. A rational root of the resolvent confines the Galois image to a conjugate of F₂₀ only when the six orbit values are distinct, and separability of f does not ensure that: here the six values at the roots 0, 1, -1, i, -i are 2, four times, and ±4i.

Main results

• TauCeti.discr_X_pow_five_sub_X: the discriminant is -256.
• TauCeti.separable_X_pow_five_sub_X: the quintic is separable over ℚ.
• TauCeti.resolventSextic_X_pow_five_sub_X: the sextic is (X - 2)⁴ (X² + 16).
• TauCeti.isRoot_resolventSextic_X_pow_five_sub_X: 2 is an integral root.
• TauCeti.discr_resolventSextic_X_pow_five_sub_X: the sextic has discriminant zero.
• TauCeti.not_separable_map_resolventSextic_X_pow_five_sub_X: the sextic is inseparable over ℚ.
• TauCeti.isRoot_specialize_quinticF20Spec_X_pow_five_sub_X: the F₂₀ resolvent specialized over ℚ has the root 2.
• TauCeti.not_exists_le_map_conj_quinticF20Spec_X_pow_five_sub_X: the Galois image of X⁵ - X lies in no conjugate of F₂₀, for any splitting extension and any numbering of the roots.
• TauCeti.not_forall_exists_le_map_conj_of_isRoot_specialize_quinticF20Spec: hence the resolvent criterion fails without its separability hypothesis on the specialized resolvent.

theorem TauCeti.monic_X_pow_five_sub_X : (Polynomial.X ^ 5 - Polynomial.X).Monic

The polynomial X⁵ - X is monic over ℤ.

@[simp]

theorem TauCeti.discr_X_pow_five_sub_X : (Polynomial.X ^ 5 - Polynomial.X).discr = -256

The discriminant of X⁵ - X is -256. Its nonzero value proves separability over ℚ.

theorem TauCeti.separable_X_pow_five_sub_X : (Polynomial.X ^ 5 - Polynomial.X).Separable

The quintic X⁵ - X is separable over ℚ.

@[simp]

theorem TauCeti.resolventSextic_X_pow_five_sub_X : resolventSextic (Polynomial.X ^ 5 - Polynomial.X) = (Polynomial.X - 2) ^ 4 * (Polynomial.X ^ 2 + 16)

Dummit's sextic of X⁵ - X has a quadruple root at 2 and two nonreal roots.

theorem TauCeti.isRoot_resolventSextic_X_pow_five_sub_X : (resolventSextic (Polynomial.X ^ 5 - Polynomial.X)).IsRoot 2

The quintic X⁵ - X has 2 as an integral root of its sextic resolvent.

theorem TauCeti.discr_resolventSextic_X_pow_five_sub_X : (resolventSextic (Polynomial.X ^ 5 - Polynomial.X)).discr = 0

The sextic resolvent of X⁵ - X has discriminant zero.

theorem TauCeti.not_separable_map_resolventSextic_X_pow_five_sub_X : ¬(Polynomial.map (Int.castRingHom ℚ) (resolventSextic (Polynomial.X ^ 5 - Polynomial.X))).Separable

The specialized sextic of X⁵ - X over ℚ is inseparable, despite the quintic having distinct roots.

theorem TauCeti.isRoot_specialize_quinticF20Spec_X_pow_five_sub_X : (quinticF20Spec.specialize ℚ (Polynomial.X ^ 5 - Polynomial.X)).IsRoot 2

The F₂₀ resolvent of X⁵ - X, specialized over ℚ, has the root 2.

theorem TauCeti.not_exists_le_map_conj_quinticF20Spec_X_pow_five_sub_X {E : Type u_1} [Field E] [Algebra ℚ E] [Fact (Polynomial.map (algebraMap ℚ E) (Polynomial.X ^ 5 - Polynomial.X)).Splits] (e : ↑((Polynomial.X ^ 5 - Polynomial.X).rootSet E) ≃ Fin 5) : ¬∃ (τ : Equiv.Perm (Fin 5)), Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom (Polynomial.X ^ 5 - Polynomial.X) E).range ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) quinticF20Spec.H

The collision is not a containment. The Galois image of X⁵ - X over ℚ, in any splitting extension and through any numbering of its roots, lies in no conjugate of the Frobenius group F₂₀.

By TauCeti.isRoot_specialize_quinticF20Spec_X_pow_five_sub_X, the specialized F₂₀ resolvent nevertheless has the root 2 in ℚ. As X⁵ - X is monic and separable of degree five, this shows that TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize fails without its hypothesis that the specialized resolvent is separable.

theorem TauCeti.not_forall_exists_le_map_conj_of_isRoot_specialize_quinticF20Spec : ¬∀ (f : Polynomial ℚ), f.Monic → f.Separable → f.natDegree = 5 → ∀ (e : ↑(f.rootSet ℂ) ≃ Fin 5) (a : ℚ), (quinticF20Spec.specialize ℚ f).IsRoot a → ∃ (τ : Equiv.Perm (Fin 5)), Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom f ℂ).range ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) quinticF20Spec.H

The separability hypothesis on the resolvent cannot be dropped. For the F₂₀ specification, a rational root of the specialized resolvent of a monic separable quintic over ℚ does not in general confine the Galois image to a conjugate of F₂₀: X⁵ - X is a counterexample. This is TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize with its separability hypothesis on the specialized resolvent removed.