Resolvents and transitive-group labels

The resolvent criterion of TauCeti.ResolventSpec.exists_isRoot_specialize_iff_exists_le_map_conj compares the roots of a specialized resolvent in the base field with the Galois image of f read through a numbering of its roots. That image is only defined up to a numbering, while the transitive-group label TauCeti.HasGaloisLabel of f is not, so the criterion is restated here against the label: a resolvent of f 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.

One direction assumes nothing about the resolvent; the converse needs the specialized resolvent to be separable, since two orbit values that collide at the roots of f produce a root of the resolvent that constrains the Galois image no further.

This is what turns a resolvent into a test on labels: for a fixed degree, the labels whose reference subgroup is conjugate into the subgroup of the specification can be listed once and for all as a statement of permutation group theory, and the resolvent then decides membership in that list.

Main results

• TauCeti.HasGaloisLabel.exists_isRoot_specialize_of_exists_le_map_conj: a label whose reference subgroup lies in a conjugate of the subgroup of the specification gives the resolvent a root in the base field.
• TauCeti.HasGaloisLabel.exists_isRoot_specialize_iff: conversely for a separable specialized resolvent, so that the resolvent decides the containment.

References

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

theorem TauCeti.HasGaloisLabel.exists_isRoot_specialize_of_exists_le_map_conj {F : Type u_1} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hf : f.Monic) (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).IsRoot a

A label confined to the subgroup of a specification gives the resolvent 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 the resolvent of f has a root in the base field. Nothing is assumed about the resolvent.

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

The resolvent criterion, read on the label. Let f be monic with a transitive-group label, and let the resolvent of f for a specification be separable. The resolvent then 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 is what the forward implication needs; the reverse implication is TauCeti.HasGaloisLabel.exists_isRoot_specialize_of_exists_le_map_conj, which assumes nothing about the resolvent.