Irreducibility of pure polynomials with integral valuations

Let v be a real additive valuation taking integer values on nonzero elements, for example a discrete valuation normalised at a uniformiser. A polynomial is pure of slope q when every finite slope of its Newton polygon equals q. Its endpoints have integer heights, so q times its horizontal length is an integer; for rational q the denominator of q divides that length, by Polynomial.den_dvd_card_newtonSlopes.

The slopes of a factor of a nonzero polynomial are among the slopes of the polynomial, by Polynomial.newtonSlopes_le_of_dvd. Hence every factor of a pure polynomial is pure of the same slope, and if the polynomial has a nonzero constant coefficient the denominator of the slope divides the degree of every factor. Over a field this gives the Newton polygon irreducibility criterion: a polynomial with nonzero constant coefficient whose finite slopes all equal a / d, where d > 0 is its degree and a is coprime to d, is irreducible. More generally a pure polynomial of degree d with nonzero constant coefficient whose slope has denominator e has at most d / e irreducible factors, counted with multiplicity. Purity alone does not imply irreducibility, nor does a polygon with a single segment.

An Eisenstein polynomial of degree d is pure of slope -1 / d, by Polynomial.newtonSlopes_eq_replicate_of_eisenstein, and -1 is coprime to d, so the criterion recovers the Eisenstein criterion over the field. Mathlib's Polynomial.irreducible_of_eisenstein_criterion is the corresponding statement over a ring for a prime ideal, for primitive polynomials.

Main results

• Polynomial.den_dvd_natDegree_of_dvd: the denominator of the slope of a pure polynomial with nonzero constant coefficient divides the degree of each of its factors.
• Polynomial.irreducible_of_forall_mem_newtonSlopes_eq: a pure polynomial with nonzero constant coefficient whose degree is the denominator of its slope is irreducible, with the coprime numerator form Polynomial.irreducible_of_forall_mem_newtonSlopes_eq_div.
• Polynomial.card_normalizedFactors_mul_den_le_natDegree: a pure polynomial of degree d with nonzero constant coefficient whose slope has denominator e has at most d / e irreducible factors, counted with multiplicity.
• Polynomial.irreducible_of_eisenstein: the Eisenstein criterion over a field with a valuation taking integer values on nonzero elements, as a consequence of the Newton polygon irreducibility criterion.

References

• J. Neukirch, Algebraic Number Theory, Grundlehren 322, Springer, 1999, Chapter II §6, for Newton polygons over discretely valued fields, and Proposition 6.3 and its corollary for Eisenstein polynomials.
• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §3.

theorem Polynomial.den_dvd_natDegree_of_dvd {R : Type u_1} [Ring R] {v : AddValuation R (WithTop ℝ)} (hint : ∀ (x : R), x ≠ 0 → ∃ (n : ℤ), v x = ↑↑n) {f g : Polynomial R} (hf : f.coeff 0 ≠ 0) {q : ℚ} (hq : ∀ m ∈ f.newtonSlopes v, m = ↑q) (hgf : g ∣ f) : q.den ∣ g.natDegree

If the valuation takes integer values on nonzero elements and f has nonzero constant coefficient and every finite slope equal to the rational number q, then the denominator of q divides the degree of every factor of f.

theorem Polynomial.irreducible_of_forall_mem_newtonSlopes_eq {K : Type u_1} [Field K] {v : AddValuation K (WithTop ℝ)} (hint : ∀ (x : K), x ≠ 0 → ∃ (n : ℤ), v x = ↑↑n) {f : Polynomial K} (hf : f.coeff 0 ≠ 0) {q : ℚ} (hq : ∀ m ∈ f.newtonSlopes v, m = ↑q) (hden : q.den = f.natDegree) : Irreducible f

Newton polygon irreducibility criterion. If the valuation takes integer values on nonzero elements, a polynomial f with nonzero constant coefficient whose finite slopes all equal a rational number q, and whose degree is the denominator of q, is irreducible.

theorem Polynomial.irreducible_of_forall_mem_newtonSlopes_eq_div {K : Type u_1} [Field K] {v : AddValuation K (WithTop ℝ)} (hint : ∀ (x : K), x ≠ 0 → ∃ (n : ℤ), v x = ↑↑n) {f : Polynomial K} (hf : f.coeff 0 ≠ 0) (hdeg : 0 < f.natDegree) {a : ℤ} (hcop : a.natAbs.Coprime f.natDegree) (ha : ∀ m ∈ f.newtonSlopes v, m = ↑a / ↑f.natDegree) : Irreducible f

Newton polygon irreducibility criterion, coprime form. If the valuation takes integer values on nonzero elements, a polynomial f of degree d > 0 with nonzero constant coefficient whose finite slopes all equal a / d, for an integer a coprime to d, is irreducible.

theorem Polynomial.card_normalizedFactors_mul_den_le_natDegree {K : Type u_1} [Field K] {v : AddValuation K (WithTop ℝ)} [DecidableEq K] (hint : ∀ (x : K), x ≠ 0 → ∃ (n : ℤ), v x = ↑↑n) {f : Polynomial K} (hf : f.coeff 0 ≠ 0) {q : ℚ} (hq : ∀ m ∈ f.newtonSlopes v, m = ↑q) : (UniqueFactorizationMonoid.normalizedFactors f).card * q.den ≤ f.natDegree

If the valuation takes integer values on nonzero elements, a polynomial f of degree d with nonzero constant coefficient whose finite slopes all equal a rational number with denominator e has at most d / e irreducible factors, counted with multiplicity: each irreducible factor has degree a positive multiple of e.

theorem Polynomial.irreducible_of_eisenstein {K : Type u_1} [Field K] {v : AddValuation K (WithTop ℝ)} (hint : ∀ (x : K), x ≠ 0 → ∃ (n : ℤ), v x = ↑↑n) {f : Polynomial K} (hlead : v f.leadingCoeff = 0) (h0 : v (f.coeff 0) = 1) (hmem : ∀ (n : ℕ), 0 < n → n < f.natDegree → 1 ≤ v (f.coeff n)) : Irreducible f

Eisenstein criterion. If the valuation takes integer values on nonzero elements, a polynomial whose leading coefficient has valuation zero, whose constant coefficient has valuation one, and whose other coefficients below the degree have valuation at least one, is irreducible. This is the Newton polygon irreducibility criterion for the single slope -1 / d.