The quartic resolvent specification and the resolvent cubic

The D₄-invariant of four formal roots is x₀x₂ + x₁x₃. A permutation of the roots fixes it exactly when it preserves the pairing {{0, 2}, {1, 3}}, that is, exactly when it lies in the dihedral group of order 8 generated by the rotation (0 1 2 3) and the diagonal swap (0 2), which is the reference subgroup of the transitive-group label 4T3. Its orbit under all permutations consists of the three pairing sums

x₀x₂ + x₁x₃, x₀x₁ + x₂x₃, x₀x₃ + x₁x₂,

so the orbit resolvent is a cubic. Written in the elementary symmetric polynomials e₁, …, e₄ of the roots, it is

X³ - e₂ X² + (e₁e₃ - 4e₄) X - (e₁²e₄ + e₃² - 4e₂e₄).

Specializing at a quartic X⁴ + aX³ + bX² + cX + d gives the classical resolvent cubic X³ - bX² + (ac - 4d)X - (a²d + c² - 4bd), and at a depressed quartic X⁴ + pX² + qX + r it gives TauCeti.resolventCubic p q r = X³ - pX² - 4rX + (4pr - q²). Both are theorems about the universal object TauCeti.quarticD4Spec, not definitions of the resolvent: the closed form is identified with the orbit product through the uniqueness of the symmetric expression.

The invariant is x₀x₂ + x₁x₃ rather than one of the other two orbit elements because its stabilizer is the reference subgroup of 4T3 on the nose; the other two have conjugate stabilizers and the same resolvent.

Main definitions

• TauCeti.quarticD4Invariant: the invariant x₀x₂ + x₁x₃.
• TauCeti.quarticD4Spec: the resolvent specification of the invariant, for the subgroup 4T3.
• TauCeti.resolventCubic: the resolvent cubic of the depressed quartic X⁴ + pX² + qX + r.

Main results

• TauCeti.rename_quarticD4Invariant_eq_self_iff: the stabilizer of the invariant is exactly the reference subgroup of 4T3.
• TauCeti.renameOrbit_quarticD4Invariant: its orbit is the three pairing sums, and TauCeti.card_renameOrbit_quarticD4Invariant: it has three elements.
• TauCeti.quarticD4Spec_orbitProduct: the orbit product in the elementary symmetric polynomials.
• TauCeti.quarticD4Spec_specialize: the resolvent of an arbitrary polynomial, read off its coefficients of degree at most three.
• TauCeti.quarticD4Spec_specialize_depressed: the resolvent of a depressed quartic is resolventCubic p q r.
• TauCeti.natDegree_quarticD4Spec_specialize: the resolvent of a quartic is a cubic.

References

• K. Conrad, Galois groups of cubics and quartics (not in characteristic 2), Definition 3.1 and (3.7).

noncomputable def TauCeti.quarticD4Invariant : MvPolynomial (Fin 4) ℤ

The D₄-invariant x₀x₂ + x₁x₃ of four formal roots: the sum over the pairing {{0, 2}, {1, 3}} of the products of paired roots.

Equations

• TauCeti.quarticD4Invariant = MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.X 1 * MvPolynomial.X 3

theorem TauCeti.quarticD4Invariant_def : quarticD4Invariant = MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.X 1 * MvPolynomial.X 3

The defining formula of the quartic D₄-invariant.

theorem TauCeti.rename_quarticD4Invariant (σ : Equiv.Perm (Fin 4)) : (MvPolynomial.rename ⇑σ) quarticD4Invariant = MvPolynomial.X (σ 0) * MvPolynomial.X (σ 2) + MvPolynomial.X (σ 1) * MvPolynomial.X (σ 3)

Renaming the variables of the D₄-invariant along σ.

theorem TauCeti.rename_quarticD4Invariant_eq_self_iff (σ : Equiv.Perm (Fin 4)) : (MvPolynomial.rename ⇑σ) quarticD4Invariant = quarticD4Invariant ↔ σ ∈ referenceSubgroup 4 ⟨2, rename_quarticD4Invariant_eq_self_iff._proof_1⟩

The exact stabilizer. A permutation fixes the D₄-invariant if and only if it lies in the reference subgroup of 4T3, the dihedral group preserving the pairing {{0, 2}, {1, 3}}.

theorem TauCeti.renameOrbit_quarticD4Invariant : quarticD4Invariant.renameOrbit = {MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 0 * MvPolynomial.X 3 + MvPolynomial.X 1 * MvPolynomial.X 2}

The orbit of the D₄-invariant consists of the three pairing sums.

theorem TauCeti.card_renameOrbit_quarticD4Invariant : quarticD4Invariant.renameOrbit.card = 3

The orbit of the D₄-invariant has three elements, so its resolvent is a cubic.

noncomputable def TauCeti.quarticD4Spec : ResolventSpec 4

The quartic resolvent specification: the D₄-invariant x₀x₂ + x₁x₃, whose stabilizer is exactly the reference subgroup of 4T3, with its orbit product X³ - e₂ X² + (e₁e₃ - 4e₄) X - (e₁²e₄ + e₃² - 4e₂e₄) in the elementary symmetric polynomials, where eₖ₊₁ is the variable xₖ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.quarticD4Spec_H : quarticD4Spec.H = referenceSubgroup 4 ⟨2, rename_quarticD4Invariant_eq_self_iff._proof_1⟩

@[simp]

theorem TauCeti.quarticD4Spec_Φ : quarticD4Spec.Φ = quarticD4Invariant

theorem TauCeti.quarticD4Spec_orbitProduct : quarticD4Spec.orbitProduct = Polynomial.X ^ 3 - Polynomial.C (MvPolynomial.X 1) * Polynomial.X ^ 2 + Polynomial.C (MvPolynomial.X 0 * MvPolynomial.X 2 - 4 * MvPolynomial.X 3) * Polynomial.X - Polynomial.C (MvPolynomial.X 0 ^ 2 * MvPolynomial.X 3 + MvPolynomial.X 2 ^ 2 - 4 * MvPolynomial.X 1 * MvPolynomial.X 3)

The orbit product of the quartic specification, in the elementary symmetric polynomials eₖ₊₁ = xₖ.

theorem TauCeti.quarticD4Spec_specialize (R : Type u_1) [CommRing R] (f : Polynomial R) : quarticD4Spec.specialize R f = Polynomial.X ^ 3 - Polynomial.C (f.coeff 2) * Polynomial.X ^ 2 + Polynomial.C (f.coeff 3 * f.coeff 1 - 4 * f.coeff 0) * Polynomial.X - Polynomial.C (f.coeff 3 ^ 2 * f.coeff 0 + f.coeff 1 ^ 2 - 4 * f.coeff 2 * f.coeff 0)

The resolvent cubic of a polynomial, read off its coefficients: for the quartic X⁴ + aX³ + bX² + cX + d it is X³ - bX² + (ac - 4d)X - (a²d + c² - 4bd). The formula holds for every polynomial f, since the specialization only reads the coefficients of f of degree at most three.

noncomputable def TauCeti.resolventCubic {R : Type u_1} [CommRing R] (p q r : R) : Polynomial R

The resolvent cubic X³ - pX² - 4rX + (4pr - q²) of the depressed quartic X⁴ + pX² + qX + r: the specialization of the quartic resolvent specification at the depressed quartic (TauCeti.quarticD4Spec_specialize_depressed).

Equations

• TauCeti.resolventCubic p q r = Polynomial.X ^ 3 - Polynomial.C p * Polynomial.X ^ 2 - Polynomial.C (4 * r) * Polynomial.X + Polynomial.C (4 * p * r - q ^ 2)

theorem TauCeti.resolventCubic_def {R : Type u_1} [CommRing R] (p q r : R) : resolventCubic p q r = Polynomial.X ^ 3 - Polynomial.C p * Polynomial.X ^ 2 - Polynomial.C (4 * r) * Polynomial.X + Polynomial.C (4 * p * r - q ^ 2)

The defining formula of the resolvent cubic.

theorem TauCeti.quarticD4Spec_specialize_depressed {R : Type u_1} [CommRing R] (p q r : R) : quarticD4Spec.specialize R (Polynomial.X ^ 4 + Polynomial.C p * Polynomial.X ^ 2 + Polynomial.C q * Polynomial.X + Polynomial.C r) = resolventCubic p q r

The closed form of the quartic resolvent: the specialization of the quartic specification at the depressed quartic X⁴ + pX² + qX + r is its resolvent cubic.

theorem TauCeti.monic_resolventCubic {R : Type u_1} [CommRing R] (p q r : R) : (resolventCubic p q r).Monic

The resolvent cubic is monic.

theorem TauCeti.natDegree_quarticD4Spec_specialize {R : Type u_1} [CommRing R] [Nontrivial R] (f : Polynomial R) : (quarticD4Spec.specialize R f).natDegree = 3

The resolvent of the quartic specification is a cubic over every nonzero ring, since the orbit of the D₄-invariant has three elements.

This is not a simp lemma: TauCeti.ResolventSpec.natDegree_specialize already rewrites the left-hand side, to the index of the subgroup of the specification.

@[simp]

theorem TauCeti.natDegree_resolventCubic {R : Type u_1} [CommRing R] [Nontrivial R] (p q r : R) : (resolventCubic p q r).natDegree = 3

The resolvent cubic has degree 3 over every nonzero ring.