Galois Groups of Morse Polynomials

This file proves that Morse polynomials have Galois group S_n. A Morse polynomial is a polynomial whose roots have at most one collision modulo each maximal ideal.

Main results

• Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top: If the roots of f in S have at most one collision modulo each maximal ideal m, and if a group G acting transitively on the roots in S is generated by inertia subgroups, then G surjects onto the symmetric group S_n.

Such polynomials are called Morse functions in Section 4.4 of [serre-galois].

TODO

• Specialize to the case of number fields where generation by inertia subgroups is a consequence of Minkowski's theorem.
• Show that the Selmer polynomials X ^ n - X - 1 have Galois group S_n.

References

• [J. P. Serre, Topics in Galois Theory][serre-galois], Section 4.4

theorem Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] {G : Type u_3} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] {f : Polynomial R} [DecidableEq ↑(f.rootSet S)] (hf : (map (algebraMap R S) f).Splits) (p : Ideal S) [p.IsPrime] (hp : (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ p)).ncard + 1) (g : G) (hg : g ∈ Ideal.inertia G p) : (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

If the roots of f in S have at most one collision mod p, then a MulSemiringAction on the roots in S must be the identity permutation or a transposition.

Such polynomials are called Morse functions in Section 4.4 of [serre-galois].

theorem Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] {G : Type u_3} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] {f : Polynomial R} (hf : (map (algebraMap R S) f).Splits) [MulAction.IsPretransitive G ↑(f.rootSet S)] (h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1) (hG : ⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal = ⊤) : Function.Surjective ⇑(MulAction.toPermHom G ↑(f.rootSet S))

If the roots of f in S have at most one collision modulo each maximal ideal m, and if a group G acting transitively on the roots in S is generated by inertia subgroups, then G surjects onto the symmetric group S_n.

Such polynomials are called Morse functions in Section 4.4 of [serre-galois].