Resolvents of a Tschirnhaus transform

A resolvent specialized at a monic separable polynomial f detects the Galois image of f only when it is separable: two values of the orbit of the invariant can collide at the roots of f, which makes the resolvent inseparable, and then a root of the resolvent in the base field need not confine the Galois image to a conjugate of the subgroup of the specification. The classical remedy replaces f by an admissible Tschirnhaus transform Polynomial.tschirnhausPolynomial f T, whose roots are the values T(α) at the roots α of f, and computes the resolvent of the transform instead.

This file shows that the remedy is sound. An admissible transform of a monic separable f is again monic and separable of the same degree, and, when its roots are numbered through α ↦ T(α), its Galois image is the Galois image of f (Polynomial.TschirnhausAdmissible.map_range_galActionHom_tschirnhausPolynomial). The resolvent criterion and the factorization theorem applied to the transform are therefore statements about f. In particular, if the resolvent of the transform is separable and has a root in the base field, then the Galois image of f lies in a conjugate of the subgroup of the specification. Separability of the resolvent of the transform is the only extra condition: like every specialization, it is monic of the full orbit degree.

Main results

• TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize_tschirnhausPolynomial: a root of the separable resolvent of an admissible transform confines the Galois image of f to a conjugate of H.
• TauCeti.ResolventSpec.exists_isRoot_specialize_tschirnhausPolynomial_of_le_map_conj: conversely, without any hypothesis on the resolvent, a Galois image of f inside a conjugate of H gives the resolvent of every admissible transform a root.
• TauCeti.ResolventSpec.exists_isRoot_specialize_tschirnhausPolynomial_iff_exists_le_map_conj: the resolvent criterion, applied through an admissible transform.
• TauCeti.ResolventSpec.map_natDegree_normalizedFactors_specialize_tschirnhausPolynomial: the factor degrees of the separable resolvent of an admissible transform are the sizes of the orbits of the Galois image of f on the cosets of H.
• TauCeti.HasGaloisLabel.exists_isRoot_specialize_tschirnhausPolynomial_of_exists_le_map_conj and TauCeti.HasGaloisLabel.exists_isRoot_specialize_tschirnhausPolynomial_iff: the two directions read on the transitive-group label of f.

References

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

theorem TauCeti.ResolventSpec.exists_le_map_conj_of_isRoot_specialize_tschirnhausPolynomial {F : Type u_1} [Field F] {f T : Polynomial F} {n : ℕ} {E : Type u_2} [Field E] [Algebra F E] [hfsp : Fact (Polynomial.map (algebraMap F E) f).Splits] (spec : ResolventSpec n) [Normal F E] (hf : f.Monic) (hsep : f.Separable) (hdeg : f.natDegree = n) (hT : f.TschirnhausAdmissible T) (e : ↑(f.rootSet E) ≃ Fin n) (hres : (spec.specialize F (f.tschirnhausPolynomial T)).Separable) {a : F} (ha : (spec.specialize F (f.tschirnhausPolynomial T)).IsRoot a) : ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom f E).range ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) spec.H

A root of the separable resolvent of an admissible transform confines the Galois image. Let f be monic and separable of degree n, let E be a normal splitting extension, number the roots of f in E by e, and let T be admissible for f. If the resolvent of the Tschirnhaus transform of f by T is separable and has a root in F, then the Galois image of f, read through e, lies in a conjugate of the subgroup of the specification.

The resolvent of f itself may be inseparable here; this is the case the transform is for.

theorem TauCeti.ResolventSpec.exists_isRoot_specialize_tschirnhausPolynomial_of_le_map_conj {F : Type u_1} [Field F] {f T : Polynomial F} {n : ℕ} {E : Type u_2} [Field E] [Algebra F E] [hfsp : Fact (Polynomial.map (algebraMap F E) f).Splits] (spec : ResolventSpec n) [IsGalois F E] (hf : f.Monic) (hsep : f.Separable) (hdeg : f.natDegree = n) (hT : f.TschirnhausAdmissible T) (e : ↑(f.rootSet E) ≃ Fin n) (τ : Equiv.Perm (Fin n)) (hle : Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom f E).range ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) spec.H) : ∃ (a : F), (spec.specialize F (f.tschirnhausPolynomial T)).IsRoot a

A Galois image inside a conjugate of H gives the resolvent of every admissible transform a root. Let f be monic and separable of degree n, let E be a Galois splitting extension, and number the roots of f in E by e. If the Galois image of f, read through e, lies in a conjugate of the subgroup of the specification, then for every admissible T the resolvent of the Tschirnhaus transform of f by T has a root in F. Nothing is assumed about that resolvent.

theorem TauCeti.ResolventSpec.exists_isRoot_specialize_tschirnhausPolynomial_iff_exists_le_map_conj {F : Type u_1} [Field F] {f T : Polynomial F} {n : ℕ} {E : Type u_2} [Field E] [Algebra F E] [hfsp : Fact (Polynomial.map (algebraMap F E) f).Splits] (spec : ResolventSpec n) [IsGalois F E] (hf : f.Monic) (hsep : f.Separable) (hdeg : f.natDegree = n) (hT : f.TschirnhausAdmissible T) (e : ↑(f.rootSet E) ≃ Fin n) (hres : (spec.specialize F (f.tschirnhausPolynomial T)).Separable) : (∃ (a : F), (spec.specialize F (f.tschirnhausPolynomial T)).IsRoot a) ↔ ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom f E).range ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) spec.H

The resolvent criterion through an admissible transform. Let f be monic and separable of degree n, let E be a Galois splitting extension, number the roots of f in E by e, and let T be admissible for f. If the resolvent of the Tschirnhaus transform of f by T is separable, it has a root in F exactly when the Galois image of f, read through e, lies in a conjugate of the subgroup of the specification.

theorem TauCeti.ResolventSpec.map_natDegree_normalizedFactors_specialize_tschirnhausPolynomial {F : Type u_1} [Field F] {f T : Polynomial F} {n : ℕ} {E : Type u_2} [Field E] [Algebra F E] [hfsp : Fact (Polynomial.map (algebraMap F E) f).Splits] (spec : ResolventSpec n) [Normal F E] (hf : f.Monic) (hdeg : f.natDegree = n) (hT : f.TschirnhausAdmissible T) (e : ↑(f.rootSet E) ≃ Fin n) (hres : (spec.specialize F (f.tschirnhausPolynomial T)).Separable) : Multiset.map Polynomial.natDegree (UniqueFactorizationMonoid.normalizedFactors (spec.specialize F (f.tschirnhausPolynomial T))) = Multiset.map (fun (ω : MulAction.orbitRel.Quotient (↥(Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom f E).range)) (Equiv.Perm (Fin n) ⧸ spec.H)) => Nat.card ↑ω.orbit) Finset.univ.val

The factor degrees of the separable resolvent of an admissible transform are orbit sizes. 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 T be admissible for f. If the resolvent of the Tschirnhaus transform of f by T is separable, the multiset of degrees of its monic irreducible factors is the multiset of sizes of the orbits of the Galois image of f, read through e, on the cosets of H.

theorem TauCeti.HasGaloisLabel.exists_isRoot_specialize_tschirnhausPolynomial_of_exists_le_map_conj {F : Type u_1} [Field F] {f T : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hf : f.Monic) (hT : f.TschirnhausAdmissible T) (spec : ResolventSpec n) (hle : ∃ (τ : Equiv.Perm (Fin n)), referenceSubgroup n j ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) spec.H) : ∃ (a : F), (spec.specialize F (f.tschirnhausPolynomial T)).IsRoot a

A label confined to the subgroup of a specification gives the resolvent of every admissible transform a root. If the reference subgroup of the label of a monic f lies in a conjugate of the subgroup of a resolvent specification, then for every admissible T the resolvent of the Tschirnhaus transform of f by T has a root in the base field. Nothing is assumed about that resolvent.

theorem TauCeti.HasGaloisLabel.exists_isRoot_specialize_tschirnhausPolynomial_iff {F : Type u_1} [Field F] {f T : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hf : f.Monic) (hT : f.TschirnhausAdmissible T) (spec : ResolventSpec n) (hres : (spec.specialize F (f.tschirnhausPolynomial T)).Separable) : (∃ (a : F), (spec.specialize F (f.tschirnhausPolynomial T)).IsRoot a) ↔ ∃ (τ : Equiv.Perm (Fin n)), referenceSubgroup n j ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) spec.H

The resolvent criterion through an admissible transform, read on the label. Let f be monic with a transitive-group label and let T be admissible for f. If the resolvent of the Tschirnhaus transform of f by T is separable, it has a root in the base field exactly when the reference subgroup of the label of f lies in a conjugate of the subgroup of the specification.

Separability of the resolvent of the transform is what the forward implication needs; the reverse implication is TauCeti.HasGaloisLabel.exists_isRoot_specialize_tschirnhausPolynomial_of_exists_le_map_conj.