Documentation

TauCeti.FieldTheory.GaloisGroups.Resolvent.Quintic.Basic

The quintic F₂₀ resolvent specification and the resolvent sextic #

Index five formal roots by ℤ/5 and set

Φ = ∑ a, xₐ² (xₐ₊₁ xₐ₋₁ + xₐ₊₂ xₐ₋₂),

the ten monomials x₀²x₁x₄ + x₀²x₂x₃ + x₁²x₂x₀ + x₁²x₃x₄ + ⋯. The stabilizer of Φ under permutation of the variables is exactly the reference subgroup of the transitive-group label 5T3, the Frobenius group F₂₀ = AGL(1, 5) of affine maps of ℤ/5, of order twenty: the affine maps a ↦ a + 1 and a ↦ 2a + 1 that generate it permute the summands of Φ. The orbit of Φ under the whole symmetric group therefore has 120 / 20 = 6 elements, and the orbit resolvent of a quintic is a sextic.

That the stabilizer is exactly F₂₀, and not merely contained in it, identifies the six universal orbit elements with the cosets S₅ / F₂₀. After specialization their values may still collide, so using a rational root to detect containment in a conjugate of F₂₀ requires separation evidence, for example a nonzero discriminant of the specialized sextic.

TauCeti.resolventSextic f is the specialization of this specification at a quintic f over ℤ. Integrality is a theorem about ResolventSpec.specialize and not an extra hypothesis, so the sextic is a monic integral polynomial of degree six; the sextic over ℚ is its image under Polynomial.map, by TauCeti.ResolventSpec.specialize_map. Being monic and integral, any rational root is integral, reducing the rational-root search to integers; concluding containment from such a root separately requires the separation evidence above.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.quinticF20Invariant :
MvPolynomial (Fin 5) ℤ

Dummit's F₂₀-invariant of five formal roots indexed by ℤ/5: ∑ a, xₐ² (xₐ₊₁ xₐ₋₁ + xₐ₊₂ xₐ₋₂), a sum of ten monomials of shape xₐ² x_b x_c.

Equations
Instances For
    source
    theorem TauCeti.quinticF20Invariant_def :
    quinticF20Invariant = ∑ a : Fin 5, MvPolynomial.X a ^ 2 * (MvPolynomial.X (a + 1) * MvPolynomial.X (a - 1) + MvPolynomial.X (a + 2) * MvPolynomial.X (a - 2))

    The defining formula of the quintic F₂₀-invariant.

    source
    theorem TauCeti.isHomogeneous_quinticF20Invariant :
    quinticF20Invariant.IsHomogeneous 4

    Dummit's F₂₀-invariant is homogeneous of degree four.

    source
    theorem TauCeti.rename_quinticF20Invariant (σ : Equiv.Perm (Fin 5)) :
    (MvPolynomial.rename ⇑σ) quinticF20Invariant = ∑ a : Fin 5, MvPolynomial.X (σ a) ^ 2 * (MvPolynomial.X (σ (a + 1)) * MvPolynomial.X (σ (a - 1)) + MvPolynomial.X (σ (a + 2)) * MvPolynomial.X (σ (a - 2)))

    Renaming the variables of the F₂₀-invariant along σ.

    source
    theorem TauCeti.eval₂_rename_quinticF20Invariant {R : Type u_1} [CommRing R] (x : Fin 5 → R) (k : Fin 5 → Fin 5) :
    MvPolynomial.eval₂ (Int.castRingHom R) x ((MvPolynomial.rename k) quinticF20Invariant) = x (k 0) ^ 2 * (x (k 1) * x (k 4) + x (k 2) * x (k 3)) + x (k 1) ^ 2 * (x (k 2) * x (k 0) + x (k 3) * x (k 4)) + x (k 2) ^ 2 * (x (k 3) * x (k 1) + x (k 4) * x (k 0)) + x (k 3) ^ 2 * (x (k 4) * x (k 2) + x (k 0) * x (k 1)) + x (k 4) ^ 2 * (x (k 0) * x (k 3) + x (k 1) * x (k 2))

    The value at x of the renaming of the F₂₀-invariant along any k : Fin 5 → Fin 5, written out as its ten monomials.

    source
    theorem TauCeti.rename_quinticF20Invariant_eq_self_iff (σ : Equiv.Perm (Fin 5)) :
    (MvPolynomial.rename ⇑σ) quinticF20Invariant = quinticF20Invariant ↔ σ ∈ referenceSubgroup 5 ⟨2, rename_quinticF20Invariant_eq_self_iff._proof_1⟩

    The exact stabilizer. A permutation fixes the F₂₀-invariant if and only if it lies in the reference subgroup of 5T3, the Frobenius group of affine maps of ℤ/5.

    source
    noncomputable def TauCeti.quinticF20Spec :
    ResolventSpec 5

    The quintic resolvent specification: Dummit's F₂₀-invariant, whose stabilizer is exactly the reference subgroup of 5T3.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.quinticF20Spec_H :
      quinticF20Spec.H = referenceSubgroup 5 ⟨2, rename_quinticF20Invariant_eq_self_iff._proof_1⟩
      source
      @[simp]
      theorem TauCeti.quinticF20Spec_Φ :
      quinticF20Spec.Φ = quinticF20Invariant
      source
      theorem TauCeti.card_renameOrbit_quinticF20Invariant :
      quinticF20Invariant.renameOrbit.card = 6

      The orbit of the F₂₀-invariant has six elements, so its resolvent is a sextic.

      source
      noncomputable def TauCeti.resolventSextic (f : Polynomial ℤ) :
      Polynomial ℤ

      The resolvent sextic of an integral quintic f: the specialization of the quintic F₂₀ specification at f, over ℤ. It is monic of degree six (TauCeti.natDegree_resolventSextic), and the resolvent sextic over any other coefficient ring is its image under Polynomial.map, by TauCeti.ResolventSpec.specialize_map.

      Equations
      Instances For
        source
        theorem TauCeti.resolventSextic_def (f : Polynomial ℤ) :
        resolventSextic f = quinticF20Spec.specialize ℤ f

        The defining formula of the resolvent sextic.

        source
        theorem TauCeti.monic_resolventSextic (f : Polynomial ℤ) :
        (resolventSextic f).Monic

        The resolvent sextic is monic.

        source
        @[simp]
        theorem TauCeti.natDegree_resolventSextic (f : Polynomial ℤ) :
        (resolventSextic f).natDegree = 6

        The resolvent sextic has degree six, for every f: it is the image of a monic polynomial of degree [S₅ : F₂₀] = 6, so a specialization never lowers its degree.