Squarefree polynomials with prescribed factorization patterns over finite fields

This file constructs two squarefree factorization patterns over finite fields that are used to exhibit a large symmetric Galois group by reduction modulo primes:

• degrees (1, n - 1), whose Frobenius cycle type is an (n - 1)-cycle with one fixed point, which makes a transitive group doubly transitive;
• exactly one factor of degree 2 and all other factor degrees odd, whose Frobenius cycle type has an odd power that is a transposition.

These patterns are inputs to the three-prime realization of the full symmetric group Sₙ as a Galois group over ℚ.

Main results

• TauCeti.exists_monic_squarefree_map_natDegree_normalizedFactors_eq_pair_one_sub_one: for 2 ≤ n, a monic squarefree polynomial of degree n whose factor degrees are {1, n - 1}.
• TauCeti.exists_monic_squarefree_count_two_map_natDegree_normalizedFactors_eq_one_and_odd: for 2 ≤ n, a monic squarefree polynomial of degree n with exactly one quadratic irreducible factor and all other irreducible factors of odd degree.

References

• B. L. van der Waerden, Algebra I, §61, for the three-prime realization of Sₙ over ℚ that these patterns feed.

theorem TauCeti.exists_monic_squarefree_map_natDegree_normalizedFactors_eq_pair_one_sub_one (k : Type u_1) [Field k] [Finite k] [DecidableEq k] (n : ℕ) (hn : 2 ≤ n) : ∃ (g : Polynomial k), g.Monic ∧ g.natDegree = n ∧ Squarefree g ∧ Multiset.map Polynomial.natDegree (UniqueFactorizationMonoid.normalizedFactors g) = {1, n - 1}

For 2 ≤ n, a finite field has a monic squarefree polynomial of degree n whose irreducible factors have degrees 1 and n - 1.

theorem TauCeti.exists_monic_squarefree_count_two_map_natDegree_normalizedFactors_eq_one_and_odd (k : Type u_1) [Field k] [Finite k] [DecidableEq k] (n : ℕ) (hn : 2 ≤ n) : ∃ (g : Polynomial k), g.Monic ∧ g.natDegree = n ∧ Squarefree g ∧ Multiset.count 2 (Multiset.map Polynomial.natDegree (UniqueFactorizationMonoid.normalizedFactors g)) = 1 ∧ ∀ d ∈ Multiset.map Polynomial.natDegree (UniqueFactorizationMonoid.normalizedFactors g), d ≠ 2 → Odd d

For 2 ≤ n, a finite field has a monic squarefree polynomial of degree n with exactly one irreducible factor of degree 2, all of whose other irreducible factors have odd degree.

For n = 2 the polynomial is irreducible quadratic; for odd n the factors have degrees 2 and n - 2; for even n ≥ 4 they have degrees 2, 1 and n - 3.