Recently, in the Zulip server for Lean users, somebody went with something that looked like homework, but managed to sting me a little bit.
It was about irreducibility of polynomials with integer coefficients. Specifically, the guy wanted a proof that the polynomial is irreducible, claiming that the Eisenstein criterion was not good at it.
What was to proven (this is what irreducible means) is that it is impossible to write that polynomial as the product of two polynomials with integer coefficients, except by writing as or as .
This is both a complicated and a trivial question
Trivial because there are general bounds (initially due to Mignotte) for the integers that appear in any such factorization, and it could just be sufficient to try any possibility in the given range and conclude. Brute force, not very intelligent, but with a certain outcome.
Complicated because those computations would often be long, and there are many criteria in number theory to assert irreducibility.
One of the easiest criteria is the aforementioned Eisenstein criterion.
This criterion requires an auxiliary prime number, and I'll state it as an example, using another polynomial, say . Here, one takes the prime number 2, and one observes that modulo 2, the polynomial is equal to , while the constant term, 2, is not divisible by . In that case, the criterion immediately asserts that the polynomial is irreducible.
With all due respect to Eisenstein, I don't like that criterion too much, though, because it only applies in kind of exceptional situations. Still, it is often useful.
There is a classic case of application, by the way, of the Eisenstein criterion, namely the irreducibility of cyclotomic polynomials of prime index, for example, (for the prime number ). But it is not visible that the criterion applies, and one needs to perform the change of variable .
I had noticed that in that case, it maybe interesting to generalize the Eisenstein criterion to avoid this change of variables. Indeed, for a monic polynomial in , a variant of the criterion states: take an integer and a prime number , and assume that :
- (derivative at ) is not divisible by .
Then is irreducible.
For the cyclotomic polynomial of index , , still taking , one has and is not divisible by . Consequently, it is irreducible. And the same argument works for all cyclotomic polynomials of prime index.
The reason, that avoids any strange computation, is that , which modulo 5 is — by the divisibility of the binomial coefficients.
To go back to the initial example, , there are indeed no prime numbers with which the Eisenstein criterion can be applied. This is obvious in the standard form, because the constant coefficient is 1. But the variant doesn't help neither. The only prime it could seems to be 2, but its derivative at 1 is equal to , and is divisible by 4.
This is where a new variant of the criterion can be applied, this time with the prime number 3.
Theorem. — Let be a monic polynomial, let be a prime number such that is irreducible in . Let be a monic polynomial. Assume that modulo , but that modulo . Then is irreducible in .
To see how this criterion applies, observe that modulo 3, one has . So we are almost as in the initial criterion, but the polynomial is not . The first thing that allows this criterion to apply is that is irreducible modulo 3. In this case, this is because is not a square mod 3.
The criterion also requires of variant of the condition on the derivative — it holds because the polynomial is not zero modulo $\langle T^2+1, 9\rangle. Here, one has hence it is equal to 3 modulo .
And so we have an Eisenstein-type proof that the polynomial is irreducible over the integers. CQFD!
I made the fun last a bit longer by formalizing the proof in Lean, first of the generalized criterion, and then of the particular example. It is not absolutely convincing yet, because Lean/Mathlib still lacks a bit of tools for handling explicit computations. And probably many parts can be streamlined. Still, it was a fun exercise to do.
The proof works in a more general context and gives the following theore:
Theorem. — Let be an integral domain, let be a prime ideal of and let be the field of fractions of . Let be a monic polynomial such that is irreducible in . Let be a monic polynomial. Assume that modulo , but that modulo . Then is irreducible in .