Roots and factors of a resolvent over the base field #
A resolvent specification TauCeti.ResolventSpec n carries an invariant Φ in n formal roots
whose stabilizer under renaming the variables is exactly its subgroup H ≤ Equiv.Perm (Fin n).
Specializing it at a monic separable f : F[X] of degree n gives
TauCeti.ResolventSpec.specialize, a monic polynomial over F whose image in an extension E
where f splits is the product of X - Ψ(x) over the orbit of Φ, evaluated at the roots x
of f.
This file compares the roots of that polynomial in F with the Galois group. Numbering the roots
of f in E by an equivalence e : f.rootSet E ≃ Fin n turns the image of the Galois action on
the roots into a subgroup of Equiv.Perm (Fin n). An automorphism of E over F carries the
value of Φ at the roots to the value of the invariant renamed along the permutation it induces,
so that value is fixed by the whole Galois group, hence lies in F, as soon as the image lies in
H; and it is a root of the resolvent. Renaming the invariant, the resolvent therefore has a root
in F whenever the image lies in a conjugate of H. That direction assumes nothing about the
resolvent.
The converse does assume something. After specialization two distinct elements of the orbit may
take the same value at the roots of f, and a root of the resolvent then no longer singles out
one coset of H. Separability of the specialized resolvent rules this out: it makes the values of
the orbit pairwise distinct, so a root in F is the value of exactly one renamed invariant, that
invariant is fixed by every element of the Galois image, and the image lies in its stabilizer,
which is a conjugate of H.
Both readings pass through a numbering of the roots, while the resolvent itself and the property
of being conjugate into H do not depend on one.
The root criterion is the linear case of a description of the whole factorization. The value of
the invariant renamed along τ depends only on the coset τH, and an automorphism of E moves it
to the value at the coset obtained by applying the permutation the automorphism induces: the
Galois action on the values of the orbit is the action of the Galois image on the cosets of H.
When the resolvent is separable the values at distinct cosets are distinct, so the roots of the
resolvent in E are in equivariant bijection with the cosets. Its monic irreducible factors over
F, which are the minimal polynomials of these roots, therefore correspond to the orbits of the
Galois image on the cosets, and the degree of a factor is the size of its orbit.
Main results #
TauCeti.ResolventSpec.exists_isRoot_specialize_of_leandTauCeti.ResolventSpec.exists_isRoot_specialize_of_le_map_conj: a Galois image insideH, respectively inside a conjugate ofH, gives the resolvent a root in the base field.TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize: conversely, when the specialized resolvent is separable, a root of it in the base field confines the Galois image to a conjugate ofH.TauCeti.ResolventSpec.exists_isRoot_specialize_iff_exists_le_map_conj: the two together, the criterion that a separable resolvent provides.TauCeti.ResolventSpec.splits_specialize: the specialized resolvent splits in the field containing the numbered roots off.TauCeti.ResolventSpec.orbitQuotientEquivFactors: the factorization theorem, the bijection between the orbits of the Galois image on the cosets ofHand the monic irreducible factors of a separable resolvent.TauCeti.ResolventSpec.orbitQuotientEquivFactors_apply_mkandTauCeti.ResolventSpec.orbitQuotientEquivFactors_symm_apply_eq_mk_iff: the orbit of the coset ofτgoes to the minimal polynomial of the value of the invariant renamed alongτ.TauCeti.ResolventSpec.natCard_orbit_eq_natDegree_factor: along it, the size of an orbit is the degree of the matching factor.TauCeti.ResolventSpec.map_natDegree_normalizedFactors_specialize: the multiset of factor degrees of a separable resolvent is the multiset of orbit sizes.
References #
The numbered roots and the Galois action #
From the Galois image to a root of the resolvent #
A Galois image inside H gives the resolvent a root in the base field. If, read through
some numbering of the roots of a monic separable f of degree n in a Galois splitting extension
E, the image of the Galois action lies in the subgroup of the specification, then the value of
the invariant at those roots is fixed by every automorphism of E over F, hence lies in F,
and it is a root of the resolvent of f.
Nothing is assumed about the resolvent here; the converse
TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize does assume its separability.
A Galois image inside a conjugate of H gives the resolvent a root in the base field.
The conjugated subgroup is the subgroup of the specification of the renamed invariant, and
renaming the invariant does not change the resolvent.
Values on cosets of the stabilizer #
From a root of a separable resolvent to the Galois image #
A root of a separable resolvent confines the Galois image to a conjugate of H. Let f
be monic and separable of degree n, let E be a normal splitting extension, and let the
resolvent of f for the specification be separable. The values of the orbit of the invariant at
the roots of f are then pairwise distinct, so a root of the resolvent in F is the value of
exactly one renamed invariant; that invariant is fixed by every element of the Galois image, which
therefore lies in its stabilizer, a conjugate of H.
Separability of the resolvent is what makes the argument work, and it cannot be dropped: two
cosets whose invariants happen to collide at the roots of a particular f produce a root of the
resolvent in F that constrains the Galois image no further. The opposite implication,
TauCeti.ResolventSpec.exists_isRoot_specialize_of_le_map_conj, holds unconditionally.
The resolvent criterion. Let f be monic and separable of degree n, let E be a Galois
splitting extension, and let the resolvent of f for the specification be separable. The resolvent
then has a root in the base field exactly when the Galois image, read through a numbering of the
roots, lies in a conjugate of the subgroup of the specification.
The factorization of a separable resolvent #
The specialized resolvent splits over the field containing the numbered roots of a monic
polynomial of degree n. No separability of the resolvent is required.
The factorization theorem for a separable resolvent. Let f be monic of
degree n, let E be a normal splitting extension, number the roots of f in E by e, and
let the resolvent of f for the specification be separable. The orbits of the Galois image, read
through e, on the cosets of H are then in bijection with the monic irreducible factors of the
resolvent over F: the orbit of the coset of τ goes to the minimal polynomial of the value at
the roots of the invariant renamed along τ.
The degree of each factor is the size of the matching orbit,
TauCeti.ResolventSpec.natCard_orbit_eq_natDegree_factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The factorization equivalence sends the orbit of the coset of τ to the minimal polynomial
of the value at the roots of f of the invariant renamed along τ.
A factor corresponds to the orbit of the coset of τ exactly when it is the minimal
polynomial of the value at the roots of f of the invariant renamed along τ.
Factor degrees are orbit sizes. Along TauCeti.ResolventSpec.orbitQuotientEquivFactors,
the size of an orbit of the Galois image on the cosets of H is the degree of the matching monic
irreducible factor of the separable resolvent.
The factor degrees of a separable resolvent are the orbit sizes. Under the hypotheses of
TauCeti.ResolventSpec.orbitQuotientEquivFactors, the multiset of degrees of the monic irreducible
factors of the resolvent is the multiset of sizes of the orbits of the Galois image on the cosets
of H.