The pair-sum resolvent of a quintic

The linear invariant x₀ + x₁ of five formal roots is fixed exactly by the permutations that preserve the pair {0, 1}. Its stabilizer is the intransitive subgroup S_{{0,1}} × S_{{2,3,4}}, generated by the three adjacent transpositions (0 1), (2 3) and (3 4). The orbit consists of the ten sums xᵢ + xⱼ indexed by unordered pairs of distinct indices, so the associated resolvent has degree ten.

This is the basic linear-resolvent example: specializing the universal specification at a monic quintic of degree five produces the polynomial whose roots are the pairwise sums of the roots, whenever those roots are enumerated in a splitting extension.

Main definitions

• TauCeti.quinticPairSumStabilizer: the subgroup preserving {0, 1}.
• TauCeti.quinticPairSumInvariant: the invariant x₀ + x₁.
• TauCeti.quinticPairSumSpec: its resolvent specification.

Main results

• TauCeti.quinticPairSumStabilizer_eq_closure: the stabilizer is generated by (0 1), (2 3) and (3 4).
• TauCeti.rename_quinticPairSumInvariant_eq_self_iff: the exact stabilizer theorem.
• TauCeti.card_renameOrbit_quinticPairSumInvariant: the symbolic orbit has ten elements.
• TauCeti.natDegree_specialize_quinticPairSumSpec: every specialization has degree ten.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §6.3.

def TauCeti.quinticPairSumStabilizer : Subgroup (Equiv.Perm (Fin 5))

The intransitive subgroup of S₅ preserving the pair {0, 1} setwise.

Equations

• TauCeti.quinticPairSumStabilizer = TauCeti.fiberSubgroup fun (i : Fin 5) => decide (i < 2)

theorem TauCeti.mem_quinticPairSumStabilizer_iff (σ : Equiv.Perm (Fin 5)) : σ ∈ quinticPairSumStabilizer ↔ σ 0 = 0 ∧ σ 1 = 1 ∨ σ 0 = 1 ∧ σ 1 = 0

Membership in the pair-sum stabilizer means preserving the pair {0, 1}.

theorem TauCeti.quinticPairSumStabilizer_eq_closure : quinticPairSumStabilizer = Subgroup.closure {Equiv.swap 0 1, Equiv.swap 2 3, Equiv.swap 3 4}

The pair stabilizer is generated by the transpositions (0 1), (2 3) and (3 4).

noncomputable def TauCeti.quinticPairSumInvariant : MvPolynomial (Fin 5) ℤ

The linear invariant x₀ + x₁ of five formal roots.

Equations

• TauCeti.quinticPairSumInvariant = MvPolynomial.X 0 + MvPolynomial.X 1

theorem TauCeti.quinticPairSumInvariant_def : quinticPairSumInvariant = MvPolynomial.X 0 + MvPolynomial.X 1

The defining formula of the quintic pair-sum invariant.

theorem TauCeti.rename_quinticPairSumInvariant (σ : Equiv.Perm (Fin 5)) : (MvPolynomial.rename ⇑σ) quinticPairSumInvariant = MvPolynomial.X (σ 0) + MvPolynomial.X (σ 1)

Renaming the variables of the pair-sum invariant along σ.

theorem TauCeti.rename_quinticPairSumInvariant_eq_self_iff (σ : Equiv.Perm (Fin 5)) : (MvPolynomial.rename ⇑σ) quinticPairSumInvariant = quinticPairSumInvariant ↔ σ ∈ quinticPairSumStabilizer

The exact stabilizer. A permutation fixes x₀ + x₁ if and only if it preserves the pair {0, 1}.

noncomputable def TauCeti.quinticPairSumSpec : ResolventSpec 5

The quintic pair-sum resolvent specification: the invariant x₀ + x₁, whose stabilizer is the intransitive subgroup preserving {0, 1}.

Equations

• TauCeti.quinticPairSumSpec = TauCeti.ResolventSpec.mk' TauCeti.quinticPairSumStabilizer TauCeti.quinticPairSumInvariant TauCeti.rename_quinticPairSumInvariant_eq_self_iff

@[simp]

theorem TauCeti.quinticPairSumSpec_H : quinticPairSumSpec.H = quinticPairSumStabilizer

@[simp]

theorem TauCeti.quinticPairSumSpec_Φ : quinticPairSumSpec.Φ = quinticPairSumInvariant

@[simp]

theorem TauCeti.card_quinticPairSumStabilizer : Fintype.card ↥quinticPairSumStabilizer = 12

The pair-sum stabilizer has order twelve: independently permuting the pair and its three-element complement gives 2! · 3! = 12 elements.

@[simp]

theorem TauCeti.index_quinticPairSumStabilizer : quinticPairSumStabilizer.index = 10

The pair-sum stabilizer has index ten in S₅, one coset for each unordered pair.

theorem TauCeti.card_renameOrbit_quinticPairSumInvariant : quinticPairSumInvariant.renameOrbit.card = 10

The orbit of x₀ + x₁ has ten elements, indexed by the unordered pairs of five indices.

theorem TauCeti.natDegree_specialize_quinticPairSumSpec (R : Type u_1) [CommRing R] [Nontrivial R] (f : Polynomial R) : (quinticPairSumSpec.specialize R f).natDegree = 10

Every specialization of the quintic pair-sum specification has degree ten.