Galois groups over ℚ from factorizations modulo primes

Let f be a monic integral polynomial and p a prime not dividing disc f. Dedekind's theorem, TauCeti.NumberField.exists_gal_fullCycleType_eq_factorizationType, says that the degrees of the irreducible factors of f mod p are the cycle lengths, fixed points included, of some element of the Galois group of f over ℚ acting on the complex roots of f. This file reads that theorem as membership of the factorization type in the set of full cycle types of the Galois image, and draws the consequences for the Galois group.

A factorization type exhibits an element of the Galois image, so it only ever bounds the image from below. The shapes read off here are:

• an irreducible reduction exhibits a cycle through all the roots;
• a reduction with exactly one quadratic factor, all its other factors being of odd degree, exhibits a transposition, as an odd power of the element it produces;
• a reduction whose only factor of degree at least two is a cubic exhibits a 3-cycle.

Combined with the recognition theorems for permutation groups, these give the classical criteria for a large Galois group. In prime degree, irreducibility over ℚ and a transposition force the full symmetric group. In any degree, irreducibility over ℚ, a reduction of type (1, n - 1) and a reduction with a single quadratic factor and odd other factors force the full symmetric group: the first two make the Galois image doubly transitive, hence primitive, and a primitive group containing a transposition is everything. This is the criterion behind van der Waerden's construction of integral polynomials of every degree with Galois group Sₙ, where the three reductions are prescribed modulo 2, 3 and 5.

Main results

• TauCeti.natCard_rootSet_complex_eq_natDegree: an integral polynomial with nonzero discriminant has as many distinct complex roots as its degree.
• TauCeti.exists_mem_range_galActionHom_fullCycleType_eq_factorDegrees: the factor degrees of f modulo a prime not dividing disc f are the full cycle type of an element of the Galois image.
• TauCeti.lcm_factorDegrees_dvd_natCard_gal: the least common multiple of the factor degrees of f modulo a prime not dividing disc f divides the order of the Galois group.
• TauCeti.exists_isCycle_mem_range_galActionHom_of_irreducible_map: an irreducible reduction exhibits a cycle moving every root.
• TauCeti.not_irreducible_map_of_even_natDegree_of_range_le_alternatingGroup: an even-degree polynomial whose Galois image consists of even permutations has no irreducible reduction.
• TauCeti.exists_isSwap_mem_range_galActionHom: a reduction with one quadratic factor and odd other factors exhibits a transposition.
• TauCeti.exists_isThreeCycle_mem_range_galActionHom: a reduction whose only nonlinear factor is cubic exhibits a 3-cycle.
• TauCeti.alternatingGroup_le_range_galActionHom: a primitive Galois image with a reduction whose only nonlinear factor is a cubic contains the alternating group.
• TauCeti.surjective_galActionHom_of_prime_natDegree: in prime degree, irreducibility and a reduction exhibiting a transposition give the full symmetric group.
• TauCeti.surjective_galActionHom_of_factorDegrees: irreducibility, a reduction of type (1, n - 1) and a reduction exhibiting a transposition give the full symmetric group.
• TauCeti.surjective_galActionHom_X_pow_five_sub_X_sub_one: the Galois group of X ^ 5 - X - 1 over ℚ is the full symmetric group on its five roots.

References

• B. L. van der Waerden, Algebra I, Springer, §61.
• H. Cohen, A Course in Computational Algebraic Number Theory, Springer 1993, §6.3.

def TauCeti.IsGoodPrime (f : Polynomial ℤ) (p : ℕ) : Prop

A prime candidate is good for an integral polynomial when it does not divide the polynomial discriminant.

Equations

• TauCeti.IsGoodPrime f p = ¬↑p ∣ f.discr

@[simp]

theorem TauCeti.isGoodPrime_iff (f : Polynomial ℤ) (p : ℕ) : IsGoodPrime f p ↔ ¬↑p ∣ f.discr

The defining characterization of a good prime.

theorem TauCeti.natCard_rootSet_complex_eq_natDegree {f : Polynomial ℤ} (hd : f.discr ≠ 0) : Nat.card ↑((Polynomial.map (Int.castRingHom ℚ) f).rootSet ℂ) = f.natDegree

An integral polynomial with nonzero discriminant has as many distinct complex roots as its degree.

theorem TauCeti.exists_mem_range_galActionHom_fullCycleType_eq_factorDegrees {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, σ.fullCycleType = f.factorDegrees p

Factor degrees are a full cycle type of the Galois image. Let f be a monic integral polynomial and p a prime not dividing disc f. Some permutation of the complex roots of f induced by the Galois group of f over ℚ has as its cycle lengths, one part for each fixed root, the degrees of the irreducible factors of f modulo p.

The polynomial f need not be irreducible.

theorem TauCeti.lcm_factorDegrees_dvd_natCard_gal {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) : (f.factorDegrees p).lcm ∣ Nat.card (Polynomial.map (Int.castRingHom ℚ) f).Gal

Factorization types bound the order of the Galois group from below. Let f be a monic integral polynomial and p a prime not dividing disc f. The least common multiple of the degrees of the irreducible factors of f modulo p divides the order of the Galois group of f over ℚ: it is the order of the element of the Galois image that the factorization exhibits.

A factorization type bounds the Galois image only from below: it exhibits an element of the image, which every larger permutation group also contains, so it cannot confine the image to a proper subgroup.

theorem TauCeti.exists_isCycle_mem_range_galActionHom_of_irreducible_map {f : Polynomial ℤ} (hf : f.Monic) (hdeg : 2 ≤ f.natDegree) (p : ℕ) [Fact (Nat.Prime p)] (hirr : Irreducible (Polynomial.map (Int.castRingHom (ZMod p)) f)) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, σ.IsCycle ∧ σ.support = Finset.univ

An irreducible reduction exhibits a full cycle. If a monic integral polynomial f of degree at least two is irreducible modulo a prime p, then the Galois image of f over ℚ contains a cycle moving every complex root of f.

No hypothesis on the discriminant is needed: an irreducible polynomial over the perfect field ZMod p is separable, so p does not divide disc f.

theorem TauCeti.not_irreducible_map_of_even_natDegree_of_range_le_alternatingGroup {f : Polynomial ℤ} (hf : f.Monic) (hdeg : 2 ≤ f.natDegree) (heven : Even f.natDegree) (hA : (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range ≤ alternatingGroup ↑((Polynomial.map (Int.castRingHom ℚ) f).rootSet ℂ)) (p : ℕ) [Fact (Nat.Prime p)] : ¬Irreducible (Polynomial.map (Int.castRingHom (ZMod p)) f)

If a monic integral polynomial has even degree at least two and its Galois action on the complex roots consists of even permutations, then its reduction modulo any prime is reducible. An irreducible reduction would exhibit a cycle through all the roots, which is odd in even degree.

theorem TauCeti.exists_isSwap_mem_range_galActionHom {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) (htwo : Multiset.count 2 (f.factorDegrees p) = 1) (hodd : ∀ k ∈ f.factorDegrees p, k ≠ 2 → Odd k) : ∃ τ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, τ.IsSwap

A single quadratic factor exhibits a transposition. Let f be a monic integral polynomial and p a prime not dividing disc f. If exactly one irreducible factor of f modulo p is quadratic and all the others have odd degree, then the Galois image of f over ℚ contains a transposition of the complex roots of f.

theorem TauCeti.exists_isThreeCycle_mem_range_galActionHom {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) (hthree : Multiset.filter (fun (x : ℕ) => 2 ≤ x) (f.factorDegrees p) = {3}) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, σ.IsThreeCycle

A single cubic factor exhibits a 3-cycle. Let f be a monic integral polynomial and let p be a prime not dividing disc f. If the only irreducible factor of f modulo p of degree at least two is a cubic, then the Galois image contains a 3-cycle.

theorem TauCeti.alternatingGroup_le_range_galActionHom {f : Polynomial ℤ} (hf : f.Monic) (hprim : MulAction.IsPreprimitive ↥(Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range ↑((Polynomial.map (Int.castRingHom ℚ) f).rootSet ℂ)) (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) (hthree : Multiset.filter (fun (x : ℕ) => 2 ≤ x) (f.factorDegrees p) = {3}) : alternatingGroup ↑((Polynomial.map (Int.castRingHom ℚ) f).rootSet ℂ) ≤ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range

A cubic factor forces the alternating group. Let f be a monic integral polynomial whose Galois image over ℚ acts primitively on the complex roots of f, and let p be a prime not dividing disc f. If the only irreducible factor of f modulo p of degree at least two is a cubic, then the Galois image contains the alternating group of the roots.

theorem TauCeti.surjective_galActionHom_of_prime_natDegree {f : Polynomial ℤ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (hprime : Nat.Prime f.natDegree) (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) (htwo : Multiset.count 2 (f.factorDegrees p) = 1) (hodd : ∀ k ∈ f.factorDegrees p, k ≠ 2 → Odd k) : Function.Surjective ⇑(Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ)

The full symmetric group in prime degree. Let f be a monic integral polynomial of prime degree, irreducible over ℚ, and let p be a prime not dividing disc f. If exactly one irreducible factor of f modulo p is quadratic and all the others have odd degree, then the Galois group of f over ℚ induces every permutation of the complex roots of f.

theorem TauCeti.surjective_galActionHom_of_factorDegrees {f : Polynomial ℤ} (hf : f.Monic) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)) (q : ℕ) [Fact (Nat.Prime q)] (hqdeg : f.factorDegrees q = {1, f.natDegree - 1}) (r : ℕ) [Fact (Nat.Prime r)] (hr : ¬↑r ∣ f.discr) (htwo : Multiset.count 2 (f.factorDegrees r) = 1) (hodd : ∀ k ∈ f.factorDegrees r, k ≠ 2 → Odd k) : Function.Surjective ⇑(Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ)

The full symmetric group from two reductions. Let f be a monic integral polynomial of degree n, irreducible over ℚ, and let q and r be primes. Suppose that f modulo q is the product of an irreducible factor of degree n - 1 and a linear factor, and that r does not divide disc f, with exactly one irreducible factor of f modulo r quadratic and all the others of odd degree. Then the Galois group of f over ℚ induces every permutation of the complex roots of f.

Irreducibility over ℚ may itself come from a third prime, modulo which f is irreducible.

The quintic X ^ 5 - X - 1

theorem TauCeti.monic_X_pow_five_sub_X_sub_one : (Polynomial.X ^ 5 - Polynomial.X - 1).Monic

The polynomial X ^ 5 - X - 1 is monic.

theorem TauCeti.not_two_dvd_discr_X_pow_five_sub_X_sub_one : ¬↑2 ∣ (Polynomial.X ^ 5 - Polynomial.X - 1).discr

Modulo 2, the irreducible factors of X ^ 5 - X - 1 have the distinct degrees 3 and 2, so the reduction is squarefree, hence separable, and 2 does not divide the discriminant.

theorem TauCeti.surjective_galActionHom_X_pow_five_sub_X_sub_one : Function.Surjective ⇑(Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - Polynomial.X - 1)) ℂ)

The Galois group of X ^ 5 - X - 1 over ℚ is S₅.