Symmetric descent for the universal resolvent

Given an integral multivariable polynomial Φ in n formal roots, its universal resolvent is the product of X - Ψ over the orbit of Φ under permutations of the variables. Permuting the formal roots permutes these factors, so every coefficient of the product is symmetric.

The fundamental theorem of symmetric polynomials then gives a unique polynomial whose coefficients specialize to the universal resolvent after sending the variables to the elementary symmetric polynomials. This is the integral orbit product used by a resolvent specification.

Main definitions

• MvPolynomial.renameStabilizer: the subgroup of permutations fixing an invariant.
• MvPolynomial.universalResolvent: the product over the rename-orbit of an invariant.
• TauCeti.esymmSubst: substitution of the elementary symmetric polynomials for the variables.

Main results

• MvPolynomial.rename_eq_rename_iff: two permutations give the same renaming exactly when their quotient stabilizes the polynomial.
• MvPolynomial.card_renameOrbit: the rename-orbit has size the index of the stabilizer.
• MvPolynomial.renameOrbit_rename and MvPolynomial.universalResolvent_rename: renaming an invariant does not change its orbit or universal resolvent.
• MvPolynomial.universalResolvent_def: the universal resolvent is the product of the linear factors attached to the orbit.
• MvPolynomial.universalResolvent_map_rename: the universal resolvent is invariant under renaming.
• MvPolynomial.isSymmetric_universalResolvent_coeff: all of its coefficients are symmetric.
• TauCeti.esymmSubst_injective: elementary-symmetric substitution is injective.
• MvPolynomial.existsUnique_orbitProduct: the universal resolvent descends uniquely through elementary-symmetric substitution.
• MvPolynomial.monic_universalResolvent and MvPolynomial.natDegree_universalResolvent: the universal resolvent is monic of degree the size of the orbit, and MvPolynomial.monic_of_map_esymmSubst_eq, MvPolynomial.natDegree_of_map_esymmSubst_eq transfer this to its integral expression.

def MvPolynomial.renameStabilizer {σ : Type u_1} {R : Type u_2} [CommSemiring R] (Φ : MvPolynomial σ R) : Subgroup (Equiv.Perm σ)

The stabilizer of a multivariable polynomial under permutation of its variables.

Equations

• Φ.renameStabilizer = { carrier := {e : Equiv.Perm σ | (MvPolynomial.rename ⇑e) Φ = Φ}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem MvPolynomial.mem_renameStabilizer {σ : Type u_1} {R : Type u_2} [CommSemiring R] {Φ : MvPolynomial σ R} {e : Equiv.Perm σ} : e ∈ Φ.renameStabilizer ↔ (rename ⇑e) Φ = Φ

theorem MvPolynomial.rename_eq_rename_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] (Φ : MvPolynomial σ R) (a b : Equiv.Perm σ) : (rename ⇑a) Φ = (rename ⇑b) Φ ↔ a⁻¹ * b ∈ Φ.renameStabilizer

Two permutations rename a polynomial identically exactly when their quotient stabilizes it.

@[simp]

theorem MvPolynomial.renameStabilizer_eq_top_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {Φ : MvPolynomial σ R} : Φ.renameStabilizer = ⊤ ↔ Φ.IsSymmetric

A polynomial is symmetric exactly when its stabilizer is the whole symmetric group.

@[simp]

theorem MvPolynomial.renameStabilizer_rename {σ : Type u_1} {R : Type u_2} [CommSemiring R] (e : Equiv.Perm σ) (Φ : MvPolynomial σ R) : ((rename ⇑e) Φ).renameStabilizer = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj e)) Φ.renameStabilizer

The stabilizer of a renamed polynomial is the conjugate stabilizer.

noncomputable def MvPolynomial.renameOrbit {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : Finset (MvPolynomial (Fin n) ℤ)

The finite set of distinct polynomials obtained by permuting the variables of Φ.

Equations

• Φ.renameOrbit = Finset.image (fun (σ : Equiv.Perm (Fin n)) => (MvPolynomial.rename ⇑σ) Φ) Finset.univ

@[simp]

theorem MvPolynomial.mem_renameOrbit {n : ℕ} (Φ Ψ : MvPolynomial (Fin n) ℤ) : Ψ ∈ Φ.renameOrbit ↔ ∃ (σ : Equiv.Perm (Fin n)), (rename ⇑σ) Φ = Ψ

Membership in the rename-orbit is witnessed by a permutation of the variables.

theorem MvPolynomial.card_renameOrbit {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : Φ.renameOrbit.card = Φ.renameStabilizer.index

Orbit–stabilizer for invariants. The rename-orbit of Φ has as many elements as the index of its stabilizer.

@[simp]

theorem MvPolynomial.renameOrbit_rename {n : ℕ} (e : Equiv.Perm (Fin n)) (Φ : MvPolynomial (Fin n) ℤ) : ((rename ⇑e) Φ).renameOrbit = Φ.renameOrbit

A renamed invariant has the same rename-orbit.

noncomputable def MvPolynomial.universalResolvent {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : Polynomial (MvPolynomial (Fin n) ℤ)

The universal resolvent of Φ, formed over the orbit obtained by permuting its variables.

Equations

• Φ.universalResolvent = ∏ Ψ ∈ Φ.renameOrbit, (Polynomial.X - Polynomial.C Ψ)

theorem MvPolynomial.universalResolvent_def {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : Φ.universalResolvent = ∏ Ψ ∈ Φ.renameOrbit, (Polynomial.X - Polynomial.C Ψ)

The universal resolvent is the product of the monic linear factors X - Ψ attached to the elements of the rename-orbit.

@[simp]

theorem MvPolynomial.universalResolvent_rename {n : ℕ} (e : Equiv.Perm (Fin n)) (Φ : MvPolynomial (Fin n) ℤ) : ((rename ⇑e) Φ).universalResolvent = Φ.universalResolvent

A renamed invariant has the same universal resolvent.

theorem MvPolynomial.monic_universalResolvent {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : Φ.universalResolvent.Monic

The universal resolvent is monic, being a product of monic linear factors.

@[simp]

theorem MvPolynomial.natDegree_universalResolvent {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : Φ.universalResolvent.natDegree = Φ.renameOrbit.card

The universal resolvent has degree the number of elements of the rename-orbit.

noncomputable def TauCeti.esymmSubst (n : ℕ) : MvPolynomial (Fin n) ℤ →+* MvPolynomial (Fin n) ℤ

The substitution sending variable i to the elementary symmetric polynomial e_(i+1).

Equations

• TauCeti.esymmSubst n = (MvPolynomial.aeval fun (i : Fin n) => MvPolynomial.esymm (Fin n) ℤ (↑i + 1)).toRingHom

@[simp]

theorem TauCeti.esymmSubst_X (n : ℕ) (i : Fin n) : (esymmSubst n) (MvPolynomial.X i) = MvPolynomial.esymm (Fin n) ℤ (↑i + 1)

Elementary-symmetric substitution sends X i to e_(i+1).

theorem TauCeti.esymmSubst_apply (n : ℕ) (p : MvPolynomial (Fin n) ℤ) : (esymmSubst n) p = ↑((MvPolynomial.esymmAlgHom (Fin n) ℤ n) p)

Elementary-symmetric substitution agrees with Mathlib's fundamental-theorem map.

@[simp]

theorem MvPolynomial.universalResolvent_map_rename {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (σ : Equiv.Perm (Fin n)) : Polynomial.map (↑(rename ⇑σ)) Φ.universalResolvent = Φ.universalResolvent

Permuting the formal roots leaves the universal resolvent unchanged.

theorem MvPolynomial.isSymmetric_universalResolvent_coeff {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (k : ℕ) : (Φ.universalResolvent.coeff k).IsSymmetric

Every coefficient of the universal resolvent is symmetric in the formal roots.

theorem TauCeti.esymmSubst_injective (n : ℕ) : Function.Injective ⇑(esymmSubst n)

Substitution by the elementary symmetric polynomials is injective.

theorem MvPolynomial.existsUnique_orbitProduct {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) : ∃! D : Polynomial (MvPolynomial (Fin n) ℤ), Polynomial.map (TauCeti.esymmSubst n) D = Φ.universalResolvent

The universal resolvent has a unique expression in the elementary symmetric polynomials.

theorem MvPolynomial.monic_of_map_esymmSubst_eq {n : ℕ} {Φ : MvPolynomial (Fin n) ℤ} {D : Polynomial (MvPolynomial (Fin n) ℤ)} (hD : Polynomial.map (TauCeti.esymmSubst n) D = Φ.universalResolvent) : D.Monic

An integral expression for the universal resolvent in the elementary symmetric polynomials is itself monic, since elementary-symmetric substitution is injective.

theorem MvPolynomial.natDegree_of_map_esymmSubst_eq {n : ℕ} {Φ : MvPolynomial (Fin n) ℤ} {D : Polynomial (MvPolynomial (Fin n) ℤ)} (hD : Polynomial.map (TauCeti.esymmSubst n) D = Φ.universalResolvent) : D.natDegree = Φ.renameOrbit.card

An integral expression for the universal resolvent has the degree of the universal resolvent, the number of elements of the rename-orbit.