Dedekind's theorem: the cycle type of a Frobenius is the factorization type

Let f be a monic integer polynomial and p a prime modulo which f is squarefree. Let M be a number field in which f splits, and let σ ∈ Gal(M/ℚ) be an arithmetic Frobenius at a prime Q of 𝓞 M over p. Dedekind's theorem says that the permutation σ induces on the roots of f in M has, counting fixed points, cycle lengths the degrees of the irreducible factors of f modulo p.

The proof reduces the roots modulo Q. The roots of f are algebraic integers, and reduction modulo Q maps them bijectively onto the roots of f mod p in the residue field 𝓞 M ⧸ Q: their images are all the roots of f mod p, counted with multiplicity, and these are distinct because f mod p is squarefree over the perfect field 𝔽_p. The Frobenius congruence σ x ≡ x ^ p (mod Q) makes this bijection carry σ to the p-th power map, whose cycle type on the roots of a squarefree polynomial over 𝔽_p is its factorization type (TauCeti.FiniteField.fullCycleType_eq_map_natDegree_normalizedFactors). Neither the index of ℤ[θ] nor the ramification of p in the field generated by a root enters the argument.

Since p ∤ disc f makes f mod p squarefree, the theorem applies at every such prime to the splitting field of f over ℚ, where Frobenius elements exist. Moving from that splitting field to ℂ does not change the cycle type of a Galois automorphism, which gives the statement in the vocabulary of Polynomial.Gal.

Main results

• TauCeti.NumberField.fullCycleType_galActionHom_restrict_eq_factorDegrees: Dedekind's theorem for a Frobenius element of a number field in which f splits.
• TauCeti.NumberField.fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod is the same statement for the minimal polynomial of an algebraic integer θ, with the factor degrees read off from RingOfIntegers.monicFactorsMod θ p.
• TauCeti.NumberField.factorizationType_eq_cycleType_isArithFrobAt: the same statement with the cycle type and the number of fixed points as separate summands.
• TauCeti.NumberField.exists_gal_fullCycleType_eq_factorizationType: for monic f and a prime p ∤ disc f, some element of the Galois group of f over ℚ acts on the complex roots of f with full cycle type the factor degrees of f modulo p.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §8, Exercises 4 and 5.
• D. A. Marcus, Number Fields, 2nd edition, Springer 2018, Chapter 4.

theorem TauCeti.NumberField.fullCycleType_galActionHom_restrict_eq_factorDegrees {M : Type u_1} [Field M] [NumberField M] {f : Polynomial ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hf : f.Monic) (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) f)) [Fact (Polynomial.map (algebraMap ℚ M) (Polynomial.map (Int.castRingHom ℚ) f)).Splits] (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] {σ : Gal(M/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : ((Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) M) ((Polynomial.Gal.restrict (Polynomial.map (Int.castRingHom ℚ) f) M) σ)).fullCycleType = f.factorDegrees p

Dedekind's theorem. Let f be a monic integer polynomial which is squarefree modulo the prime p, and let M be a number field in which f splits. If σ ∈ Gal(M/ℚ) is an arithmetic Frobenius at a prime Q of 𝓞 M over p, then the permutation of the roots of f in M induced by σ has, counting fixed points, cycle lengths the degrees of the irreducible factors of f modulo p, with multiplicity.

theorem TauCeti.NumberField.fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod {M : Type u_1} [Field M] [NumberField M] {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))) [Fact (Polynomial.map (algebraMap ℚ M) (minpoly ℚ ↑θ)).Splits] (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] {σ : Gal(M/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : ((Polynomial.Gal.galActionHom (minpoly ℚ ↑θ) M) ((Polynomial.Gal.restrict (minpoly ℚ ↑θ) M) σ)).fullCycleType = Multiset.map Polynomial.natDegree (RingOfIntegers.monicFactorsMod θ p).val

Dedekind's theorem for a generator. Let θ be an algebraic integer of a number field K whose minimal polynomial is squarefree modulo the prime p, and let M be a number field in which the minimal polynomial of θ splits. If σ ∈ Gal(M/ℚ) is an arithmetic Frobenius at a prime Q of 𝓞 M over p, then the permutation of the roots of minpoly ℚ θ in M induced by σ has, counting fixed points, cycle lengths the degrees of the monic irreducible factors RingOfIntegers.monicFactorsMod θ p of minpoly ℤ θ modulo p.

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

The polynomial form of Dedekind's theorem. Let f be a monic integer polynomial and p a prime not dividing the discriminant of f. Then some element of the Galois group of f over ℚ acts on the complex roots of f with full cycle type (cycle lengths counted together with fixed points) equal to the multiset of degrees of the irreducible factors of f modulo p.

The statement allows reducible f: the factor degrees of all the irreducible factors of f are read off from a single Galois automorphism.

theorem TauCeti.NumberField.factorizationType_eq_cycleType_isArithFrobAt {M : Type u_1} [Field M] [NumberField M] {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))) [Fact (Polynomial.map (algebraMap ℚ M) (minpoly ℚ ↑θ)).Splits] (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] {σ : Gal(M/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : Multiset.map Polynomial.natDegree (RingOfIntegers.monicFactorsMod θ p).val = ((Polynomial.Gal.galActionHom (minpoly ℚ ↑θ) M) ((Polynomial.Gal.restrict (minpoly ℚ ↑θ) M) σ)).cycleType + Multiset.replicate (Nat.card ↑(Function.fixedPoints ⇑((Polynomial.Gal.galActionHom (minpoly ℚ ↑θ) M) ((Polynomial.Gal.restrict (minpoly ℚ ↑θ) M) σ)))) 1

Dedekind's theorem, with the fixed points counted separately. The multiset of degrees of the monic irreducible factors of minpoly ℤ θ modulo p is the cycle type of a Frobenius at a prime above p acting on the roots of minpoly ℚ θ, together with one part 1 for each fixed root. This is the form with the cycle type and the fixed points separated; the full cycle type of fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod packages the two summands.