The six conjugates of the quintic Frobenius invariant

The orbit of Dummit's quintic invariant has six elements. Here they are represented by the permutations of the last three variables that fix the first two. This explicit orbit makes the universal resolvent a product of six named factors, useful for calculating its coefficients and checking specializations.

Main results

• TauCeti.renameOrbit_quinticF20Invariant: the six representatives give the entire orbit.
• TauCeti.universalResolvent_quinticF20Invariant: the resulting six-factor product.

References

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

def TauCeti.quinticF20OrbitRepresentatives : Finset (Equiv.Perm (Fin 5))

Representatives of the six cosets of the stabilizer of Dummit's quintic invariant. They permute the last three indices and fix the first two.

Equations

• TauCeti.quinticF20OrbitRepresentatives = {1, Equiv.swap 2 3, Equiv.swap 3 4, Equiv.swap 2 4, Equiv.swap 2 3 * Equiv.swap 3 4, Equiv.swap 3 4 * Equiv.swap 2 3}

@[simp]

theorem TauCeti.mem_quinticF20OrbitRepresentatives {σ : Equiv.Perm (Fin 5)} : σ ∈ quinticF20OrbitRepresentatives ↔ σ = 1 ∨ σ = Equiv.swap 2 3 ∨ σ = Equiv.swap 3 4 ∨ σ = Equiv.swap 2 4 ∨ σ = Equiv.swap 2 3 * Equiv.swap 3 4 ∨ σ = Equiv.swap 3 4 * Equiv.swap 2 3

The orbit representatives are the identity and the five nontrivial permutations of the last three indices.

theorem TauCeti.card_quinticF20OrbitRepresentatives : quinticF20OrbitRepresentatives.card = 6

There are six orbit representatives, one for each conjugate of the invariant.

theorem TauCeti.prod_quinticF20OrbitRepresentatives {M : Type u_1} [CommMonoid M] (f : Equiv.Perm (Fin 5) → M) : ∏ σ ∈ quinticF20OrbitRepresentatives, f σ = f 1 * f (Equiv.swap 2 3) * f (Equiv.swap 3 4) * f (Equiv.swap 2 4) * f (Equiv.swap 2 3 * Equiv.swap 3 4) * f (Equiv.swap 3 4 * Equiv.swap 2 3)

A product over the orbit representatives, expanded into its six factors.

theorem TauCeti.renameOrbit_quinticF20Invariant : quinticF20Invariant.renameOrbit = Finset.image (fun (σ : Equiv.Perm (Fin 5)) => (MvPolynomial.rename ⇑σ) quinticF20Invariant) quinticF20OrbitRepresentatives

The six permutations of the last three indices give all conjugates of Dummit's quintic invariant. In particular, none of their renamings coincide as integral polynomials.

theorem TauCeti.universalResolvent_quinticF20Invariant : quinticF20Invariant.universalResolvent = ∏ σ ∈ quinticF20OrbitRepresentatives, (Polynomial.X - Polynomial.C ((MvPolynomial.rename ⇑σ) quinticF20Invariant))

The universal quintic Frobenius resolvent is the product of the six linear factors indexed by the explicit orbit representatives.