Resolvent specifications #
A resolvent tests whether the Galois group of a polynomial of degree n, viewed as a subgroup of
Equiv.Perm (Fin n) through a numbering of the roots, lies in a conjugate of a subgroup H. The
test is built from an invariant Φ in n formal roots whose stabilizer under permutation of the
variables is exactly H: the orbit of Φ is then in bijection with the cosets of H, and the
factorization of the orbit product records how the Galois group permutes those cosets. A mere
containment of H in the stabilizer would not let the resolvent detect H.
A TauCeti.ResolventSpec n packages this universal data once, independently of any polynomial or
coefficient ring: the subgroup, the integral invariant, the exact stabilizer statement, and the
unique integral expression of the orbit product in the elementary symmetric polynomials. The
last field is determined by the invariant (MvPolynomial.existsUnique_orbitProduct), and so is
the subgroup, so a specification is determined by its invariant (TauCeti.ResolventSpec.ext).
Specializing at a polynomial f over any commutative ring substitutes the signed coefficients of
f for the elementary symmetric polynomials. The result is monic of degree the index [Sₙ : H]
over every nonzero ring, commutes with every ring morphism applied to the coefficients, and, when
the roots of f are listed with multiplicity in a domain, is the orbit product of the values of
the orbit of Φ at those roots.
Main definitions #
TauCeti.ResolventSpec: a resolvent specification.TauCeti.ResolventSpec.mk': the specification attached to an invariant with prescribed exact stabilizer, with its orbit product supplied by the symmetric descent.TauCeti.ResolventSpec.specialize: the resolvent of a polynomial over a commutative ring.TauCeti.ResolventSpec.rename: the specification of a renamed invariant, for the conjugate subgroup.
Main results #
TauCeti.ResolventSpec.ext: a specification is determined by its invariant.TauCeti.ResolventSpec.specialize_map: specialization commutes with base change.TauCeti.ResolventSpec.monic_specializeandTauCeti.ResolventSpec.natDegree_specialize: the resolvent is monic of degree[Sₙ : H].TauCeti.ResolventSpec.map_specialize_eq_galResolvent: the resolvent is the orbit product at the roots.TauCeti.ResolventSpec.isRoot_specialize_eval₂_rename: every orbit value at the roots is a root of the resolvent.TauCeti.ResolventSpec.specialize_rename: renaming the invariant does not change the resolvent.
A resolvent specification in degree n: a subgroup H of Equiv.Perm (Fin n), an
integral invariant Φ in n formal roots whose stabilizer under renaming is exactly H, and the
integral expression of the orbit product of Φ in the elementary symmetric polynomials. No
polynomial and no coefficient ring appears; specialization is ResolventSpec.specialize.
- H : Subgroup (Equiv.Perm (Fin n))
The subgroup the resolvent tests membership in.
- Φ : MvPolynomial (Fin n) ℤ
The invariant polynomial in the formal roots, with integral coefficients.
- orbitProduct : Polynomial (MvPolynomial (Fin n) ℤ)
The orbit product of
Φ, written in the elementary symmetric polynomials. It is determined byΦ: seeResolventSpec.orbitProduct_unique. Substituting the elementary symmetric polynomials recovers the universal resolvent.
Instances For
The subgroup of a specification is the stabilizer of its invariant.
The integral expression of the orbit product is unique.
A specification is determined by its invariant: the subgroup is the stabilizer of the invariant, and the orbit product is its unique symmetric expression.
The specification attached to an invariant Φ whose stabilizer is exactly H; its orbit
product is the unique one provided by the symmetric descent.
Equations
- TauCeti.ResolventSpec.mk' H Φ h = { H := H, Φ := Φ, stabilizer_eq := h, orbitProduct := ⋯.choose, orbitProduct_esymm := ⋯ }
Instances For
The orbit of the invariant has [Sₙ : H] elements.
The integral orbit product is monic.
The integral orbit product has degree [Sₙ : H].
Specialization at a polynomial #
The resolvent of a polynomial f over a commutative ring R: substitute the signed
coefficients of f for the elementary symmetric polynomials in the integral orbit product. The
definition is total; it is the orbit product at the roots when f is monic of degree n
(ResolventSpec.map_specialize_eq_galResolvent).
Equations
- spec.specialize R f = Polynomial.map (TauCeti.vietaHom n f) spec.orbitProduct
Instances For
Base change. Specialization commutes with a ring morphism applied to the coefficients,
with no hypothesis on f.
The resolvent is monic, for every polynomial f.
The resolvent has degree [Sₙ : H] over every nonzero ring and for every polynomial f:
specialization can make orbit values coincide, but it never lowers the degree.
The resolvent is linear exactly when the specification tests the whole symmetric group.
For a specification testing the trivial subgroup, the resolvent has degree n!.
The resolvent is the orbit product at the roots. If f is monic of degree n and its
image in a domain L has roots x, listed with multiplicity, then the image of the resolvent of
f is the product of X - Ψ(x) over the orbit of the invariant.
Every orbit value is a root of the resolvent. If f is the product of the linear factors
attached to a family x, then the value at x of every renaming of the invariant is a root of
the resolvent of f.
Renaming the invariant #
The specification of the invariant renamed along e. Its subgroup is the conjugate of H
by e, and its orbit product is unchanged, since the orbit is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Renaming the invariant does not change the resolvent of any polynomial.