Documentation

TauCeti.FieldTheory.GaloisGroups.Resolvent.Quintic.Trinomial

The resolvent sextic of a quintic trinomial #

For a quintic X⁵ + aX + b over any commutative ring, the specialization of Dummit's F₂₀ resolvent specification is

X⁶ + 8aX⁵ + 40a²X⁴ + 160a³X³ + 400a⁴X² + (512a⁵ - 3125b⁴)X + (256a⁶ - 9375ab⁴).

This is formula (2′) of Dummit's Solving solvable quintics. Here it is a theorem about the orbit-product definition of TauCeti.resolventSextic, not a definition: it checks the specification, the symmetric descent and the Vieta substitution against the source. Its instances give the resolvent sextics of the trinomials used as worked examples, such as X⁵ - 5X - 12, whose sextic has the integral root 40.

The proof does not expand the orbit product. Dummit's invariant is homogeneous of degree four, so the coefficient of X ^ k in its integral orbit product is weighted homogeneous of weight 4 (6 - k) when the variable standing for eᵢ₊₁ has weight i + 1. At X⁵ + aX + b the elementary symmetric polynomials e₁, e₂, e₃ vanish and e₄ = a, e₅ = -b, so only the monomials e₄ⁱ e₅ʲ with 4i + 5j = 4 (6 - k) survive. This leaves eight integral constants, independent of a and b. They are read off from two quintics whose roots are explicit complex numbers: X⁵ - X, whose sextic is (X - 2)⁴ (X² + 16), fixes the six constants in front of powers of a, and the two real orbit values 190 ± 12√31 at the roots of X⁵ - 41X + 120 = (X + 3)(X² - 4X + 5)(X² + X + 8) fix the two constants in front of b⁴.

Main results #

References #

source
noncomputable def TauCeti.rootsXPowFiveSubX :
Fin 5 → ℂ

The roots 0, 1, -1, i, -i of X⁵ - X, in a fixed order.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.rootsXPowFiveSubX_def :
    rootsXPowFiveSubX = ![0, 1, -1, Complex.I, -Complex.I]

    The explicit entries of rootsXPowFiveSubX.

    source
    theorem TauCeti.X_pow_five_sub_X_eq_prod_X_sub_C_rootsXPowFiveSubX :
    Polynomial.X ^ 5 - Polynomial.X = ∏ i : Fin 5, (Polynomial.X - Polynomial.C (rootsXPowFiveSubX i))

    The factorization of X⁵ - X over ℂ using rootsXPowFiveSubX.

    source
    theorem TauCeti.quinticF20Spec_specialize_X_pow_five_add_C_mul_X_add_C {R : Type u_1} [CommRing R] (a b : R) :
    quinticF20Spec.specialize R (Polynomial.X ^ 5 + Polynomial.C a * Polynomial.X + Polynomial.C b) = Polynomial.X ^ 6 + Polynomial.C (8 * a) * Polynomial.X ^ 5 + Polynomial.C (40 * a ^ 2) * Polynomial.X ^ 4 + Polynomial.C (160 * a ^ 3) * Polynomial.X ^ 3 + Polynomial.C (400 * a ^ 4) * Polynomial.X ^ 2 + Polynomial.C (512 * a ^ 5 - 3125 * b ^ 4) * Polynomial.X + Polynomial.C (256 * a ^ 6 - 9375 * a * b ^ 4)

    Dummit's formula for the resolvent of a quintic trinomial. Over every commutative ring, the specialization of the quintic F₂₀ specification at X⁵ + aX + b is X⁶ + 8aX⁵ + 40a²X⁴ + 160a³X³ + 400a⁴X² + (512a⁵ - 3125b⁴)X + (256a⁶ - 9375ab⁴).

    source
    theorem TauCeti.resolventSextic_X_pow_five_add_C_mul_X_add_C (a b : ℤ) :
    resolventSextic (Polynomial.X ^ 5 + Polynomial.C a * Polynomial.X + Polynomial.C b) = Polynomial.X ^ 6 + Polynomial.C (8 * a) * Polynomial.X ^ 5 + Polynomial.C (40 * a ^ 2) * Polynomial.X ^ 4 + Polynomial.C (160 * a ^ 3) * Polynomial.X ^ 3 + Polynomial.C (400 * a ^ 4) * Polynomial.X ^ 2 + Polynomial.C (512 * a ^ 5 - 3125 * b ^ 4) * Polynomial.X + Polynomial.C (256 * a ^ 6 - 9375 * a * b ^ 4)

    Dummit's formula (2′) for the resolvent sextic of the integral quintic X⁵ + aX + b.

    source
    @[simp]
    theorem TauCeti.resolventSextic_X_pow_five_sub_five_mul_X_sub_twelve :
    resolventSextic (Polynomial.X ^ 5 - 5 * Polynomial.X - 12) = Polynomial.X ^ 6 - 40 * Polynomial.X ^ 5 + 1000 * Polynomial.X ^ 4 - 20000 * Polynomial.X ^ 3 + 250000 * Polynomial.X ^ 2 - 66400000 * Polynomial.X + 976000000

    The resolvent sextic of X⁵ - 5X - 12, from Dummit's formula for a quintic trinomial.

    source
    theorem TauCeti.isRoot_resolventSextic_X_pow_five_sub_five_mul_X_sub_twelve :
    (resolventSextic (Polynomial.X ^ 5 - 5 * Polynomial.X - 12)).IsRoot 40

    The resolvent sextic of X⁵ - 5X - 12 has the integral root 40.