The Eisenstein criterion

Polynomial.generalizedEisenstein : Let R be an integral domain and let K an R-algebra which is a field Let q : R[X] be a monic polynomial which is prime in K[X]. Let f : R[X] be a polynomial of strictly positive degree satisfying the following properties:

• the image of f in K[X] is a power of q.
• the leading coefficient of f is not zero in K
• the polynomial f is primitive. Assume moreover that f.modByMonic q is not zero in (R ⧸ (P ^ 2))[X], where P is the kernel of algebraMap R K. Then f is irreducible.

We give in Archive.Examples.Eisenstein an explicit example of application of this criterion.

• Polynomial.irreducible_of_eisenstein_criterion : the classic Eisenstein criterion. It is the particular case where q := X.

TODO

The case of a polynomial q := X - a is interesting, then the mod P ^ 2 hypothesis can rephrased as saying that f.derivative.eval a ∉ P ^ 2. (TODO) The case of cyclotomic polynomials of prime index p could be proved directly using that result, taking a = 1.

The result can also be generalized to the case where the leading coefficients of f and q do not belong to P. (By localization at P, make these coefficients invertible.) There are two obstructions, though :

• Usually, one will only obtain irreducibility in F[X], where F is the field of fractions of R. (If R is a UFD, this will be close to what is wanted, but not in general.)

• The mod P ^ 2 hypothesis will have to be rephrased to a condition in the second symbolic power of P. When P is a maximal ideal, that symbolic power coincides with P ^ 2, but not in general.

theorem Polynomial.generalizedEisenstein {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] {q f : Polynomial R} {p : ℕ} (hq_irr : Irreducible (map (algebraMap R K) q)) (hq_monic : q.Monic) (hf_prim : f.IsPrimitive) (hfd0 : 0 < f.natDegree) (hfP : (algebraMap R K) f.leadingCoeff ≠ 0) (hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p) (hfmodP2 : map (Ideal.Quotient.mk (RingHom.ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0) : Irreducible f

A generalized Eisenstein criterion

Let R be an integral domain and K an R-algebra which is a domain. Let q : R[X] be a monic polynomial which is prime in K[X]. Let f : R[X] be a primitive polynomial of strictly positive degree whose leading coefficient is not zero in K and such that the image f in K[X] is a power of q. Assume moreover that f.modByMonic q is not zero in (R ⧸ (P ^ 2))[X], where P is the kernel of algebraMap R K. Then f is irreducible.

theorem Polynomial.irreducible_of_eisenstein_criterion {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} {P : Ideal R} (hP : P.IsPrime) (hfl : f.leadingCoeff ∉ P) (hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P) (hfd0 : 0 < f.degree) (h0 : f.coeff 0 ∉ P ^ 2) (hu : f.IsPrimitive) : Irreducible f

If f is a non constant polynomial with coefficients in R, and P is a prime ideal in R, then if every coefficient in R except the leading coefficient is in P, and the trailing coefficient is not in P^2 and no non units in R divide f, then f is irreducible.