Degrees of polynomial factors modulo a prime

For an integral polynomial f and a prime p, Polynomial.factorDegrees f p is the multiset of degrees of the monic irreducible factors of the reduction of f modulo p. Multiplicities are retained: a repeated irreducible factor contributes its degree repeatedly.

This file gives the generic polynomial API for the carrier: membership, products, total degree, and its relationship with irreducibility. Worked examples for X ^ 5 - X - 1 are in TauCeti/FieldTheory/GaloisGroups/FactorDegrees.lean.

Main declarations

• Polynomial.factorDegrees: the multiset of factor degrees of f modulo p.
• Polynomial.factorDegrees_def: a convenient defining equation for the carrier.
• Polynomial.mem_factorDegrees_iff: a number occurs as a factor degree exactly when it is the degree of a normalized irreducible factor of the reduction.
• Polynomial.factorDegrees_mul: the factor degrees of a product with nonzero reductions are the sum of the factor degrees.
• Polynomial.factorDegrees_eq_map_natDegree_of_map_eq_prod: compute the factor degrees from any factorization of the reduction into irreducibles.
• Polynomial.sum_factorDegrees_eq_natDegree_map, Polynomial.Monic.sum_factorDegrees: the factor degrees sum to the degree after reduction, which for monic f is f.natDegree.
• Polynomial.factorDegrees_eq_singleton_iff: the factor degrees are {n} exactly when the reduction is irreducible of degree n.
• Polynomial.squarefree_map_of_nodup_factorDegrees: pairwise distinct factor degrees force the reduction to be squarefree.

References

• D. A. Marcus, Number Fields, 2nd edition, Springer 2018, Chapter 4.
• J. Neukirch, Algebraic Number Theory, Springer 1999, Chapter I, §8.

noncomputable def Polynomial.factorDegrees (f : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] : Multiset ℕ

The multiset of degrees of the monic irreducible factors of the reduction of an integral polynomial modulo a prime. Repeated factors occur with their multiplicities.

Equations

• f.factorDegrees p = Multiset.map Polynomial.natDegree (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) f))

theorem Polynomial.factorDegrees_def (f : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] : f.factorDegrees p = Multiset.map natDegree (UniqueFactorizationMonoid.normalizedFactors (map (Int.castRingHom (ZMod p)) f))

A convenient defining equation for Polynomial.factorDegrees.

@[simp]

theorem Polynomial.mem_factorDegrees_iff {f : Polynomial ℤ} {p d : ℕ} [Fact (Nat.Prime p)] : d ∈ f.factorDegrees p ↔ ∃ q ∈ UniqueFactorizationMonoid.normalizedFactors (map (Int.castRingHom (ZMod p)) f), q.natDegree = d

A natural number occurs in f.factorDegrees p exactly when it is the degree of a normalized irreducible factor of the reduction of f modulo p.

theorem Polynomial.pos_of_mem_factorDegrees {f : Polynomial ℤ} {p d : ℕ} [Fact (Nat.Prime p)] (hd : d ∈ f.factorDegrees p) : 0 < d

Every degree occurring in f.factorDegrees p is positive.

@[simp]

theorem Polynomial.card_factorDegrees (f : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] : (f.factorDegrees p).card = (UniqueFactorizationMonoid.normalizedFactors (map (Int.castRingHom (ZMod p)) f)).card

The number of factor degrees is the number of normalized irreducible factors, counted with multiplicity.

@[simp]

theorem Polynomial.factorDegrees_zero (p : ℕ) [Fact (Nat.Prime p)] : factorDegrees 0 p = 0

The zero polynomial has no factor degrees.

@[simp]

theorem Polynomial.factorDegrees_one (p : ℕ) [Fact (Nat.Prime p)] : factorDegrees 1 p = 0

The constant polynomial one has no factor degrees.

theorem Polynomial.factorDegrees_mul (f g : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hf : map (Int.castRingHom (ZMod p)) f ≠ 0) (hg : map (Int.castRingHom (ZMod p)) g ≠ 0) : (f * g).factorDegrees p = f.factorDegrees p + g.factorDegrees p

Factor degrees turn a product whose reductions are nonzero into multiset addition.

theorem Polynomial.factorDegrees_eq_map_natDegree_of_map_eq_prod {f : Polynomial ℤ} {p : ℕ} [Fact (Nat.Prime p)] {s : Multiset (Polynomial (ZMod p))} (hs : ∀ q ∈ s, Irreducible q) (hfs : map (Int.castRingHom (ZMod p)) f = s.prod) : f.factorDegrees p = Multiset.map natDegree s

The factor degrees are read off from any factorization of the reduction into irreducibles, without normalizing the factors first.

@[simp]

theorem Polynomial.sum_factorDegrees_eq_natDegree_map (f : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] : (f.factorDegrees p).sum = (map (Int.castRingHom (ZMod p)) f).natDegree

The sum of the factor degrees is the degree of the polynomial after reduction.

theorem Polynomial.Monic.sum_factorDegrees {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] : (f.factorDegrees p).sum = f.natDegree

For a monic polynomial, the degrees of all irreducible factors of its reduction modulo a prime, counted with multiplicity, sum to the degree of the original polynomial.

theorem Polynomial.factorDegrees_eq_singleton_of_irreducible (f : Polynomial ℤ) (p : ℕ) [Fact (Nat.Prime p)] (h : Irreducible (map (Int.castRingHom (ZMod p)) f)) : f.factorDegrees p = {(map (Int.castRingHom (ZMod p)) f).natDegree}

If the reduction of f modulo p is irreducible, its only factor degree is its degree.

theorem Polynomial.irreducible_map_of_card_factorDegrees_eq_one {f : Polynomial ℤ} {p : ℕ} [Fact (Nat.Prime p)] (h : (f.factorDegrees p).card = 1) : Irreducible (map (Int.castRingHom (ZMod p)) f)

A single factor degree, whatever it is, forces the reduction to be irreducible.

@[simp]

theorem Polynomial.factorDegrees_eq_singleton_iff {f : Polynomial ℤ} {p n : ℕ} [Fact (Nat.Prime p)] : f.factorDegrees p = {n} ↔ Irreducible (map (Int.castRingHom (ZMod p)) f) ∧ (map (Int.castRingHom (ZMod p)) f).natDegree = n

The factor degrees of f modulo p are the singleton {n} exactly when the reduction is irreducible of degree n.

theorem Polynomial.Monic.factorDegrees_eq_singleton_iff_irreducible {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] : f.factorDegrees p = {f.natDegree} ↔ Irreducible (Polynomial.map (Int.castRingHom (ZMod p)) f)

For a monic integral polynomial, having its own degree as sole factor degree is equivalent to its reduction being irreducible.

theorem Polynomial.squarefree_map_of_nodup_factorDegrees {f : Polynomial ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hf : map (Int.castRingHom (ZMod p)) f ≠ 0) (h : (f.factorDegrees p).Nodup) : Squarefree (map (Int.castRingHom (ZMod p)) f)

A nonzero reduction whose irreducible factors have pairwise distinct degrees is squarefree: no irreducible factor can then occur twice.