Zulip Chat Archive

Stream: maths

Topic: Eiseinstein polynomials

Riccardo Brasca (Jan 20 2022 at 18:54):

What do you think about a file ring_theory.polynomial.eisenstein about Eiseinstein polynomials? Something like

import ring_theory.eisenstein_criterion

universe u

variables {R : Type u} [comm_semiring R]

namespace polynomial

structure is_eisenstein_at (𝓟 : ideal R) (f : polynomial R) :=
(monic : f.monic)
(mem : ∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟)
(not_mem : f.coeff 0 ∉ 𝓟 ^ 2)

end polynomial

Currently we have irreducibility via docs#polynomial.irreducible_of_eisenstein_criterion, but I plan to add more results concerning Eisenstein polynomials in flt-regular, especially the fact that if the minimal polynomial of an algebraic integer $x$ is Eisenstein at $p$ then $\mathbb{Z}[x]$ is $p$ -maximal inside $\mathcal{O}_{\mathbb{Q}(x)}$ .

Yakov Pechersky (Jan 20 2022 at 18:58):

You'd likely want to make the ideal over which it is Eisenstein explicit

Riccardo Brasca (Jan 20 2022 at 19:00):

Ah, of course

Damiano Testa (Jan 20 2022 at 19:06):

Also, why do you want the polynomial to be monic and not simply have leading coefficient not in the ideal?

Riccardo Brasca (Jan 20 2022 at 19:06):

I was expecting that objection :grinning:

Damiano Testa (Jan 20 2022 at 19:07):

Actually you could change the for all condition to simply skip the natdegree and quantify over all nats

Riccardo Brasca (Jan 20 2022 at 19:07):

Well, of course it depends on the application we have in mind. For irreducibility primitive is enough, but for what I want to do I think I need monic

Riccardo Brasca (Jan 20 2022 at 19:07):

Of course I can just state my result for a monic Eisenstein polynomial

Damiano Testa (Jan 20 2022 at 19:08):

In the more general context of Newton polygons, it makes sense to think about just having valuation zero, but I am not planning to use this soon, so I am happy with whatever, really!

Riccardo Brasca (Jan 20 2022 at 19:09):

I think the point is to try to guess how many times this def will be used. If 90% of the time is with monic is probably a good idea to have it in the definition

Riccardo Brasca (Jan 20 2022 at 19:09):

I need stuff like

lemma eisenstein {x : S} {P : polynomial S} (hP : eval x P = 0) {p : S}
  (hmo : P.monic) (hdiv : ∀ n < P.nat_degree, p ∣ P.coeff n ) :
  ∀ i, P.nat_degree ≤ i → p ∣ x ^ i :=

Riccardo Brasca (Jan 20 2022 at 19:10):

So I want to write x ^ i as a linear combination of lower powers

Riccardo Brasca (Jan 20 2022 at 19:10):

(well, here eisenstein is not necessary, but it is later)

Damiano Testa (Jan 20 2022 at 19:16):

My inclination would still be to make mem an iff with n ≠ natdegree

Riccardo Brasca (Jan 20 2022 at 19:24):

I don't see the point. The definition will be a little more elegant, but to check it holds one need more work. Of course this can be a lemma.

Damiano Testa (Jan 20 2022 at 20:09):

Regardless of the issue of what definition you use, I think that if you switch the order of the ideal and the polynomial in the definition, dot-notation allows for

ˋf.is_eisentein_at Pˋ

Damiano Testa (Jan 20 2022 at 20:19):

Also, my main motivation for wanting not necessarily monic polynomials has its roots in this proof of the irreducibility of the truncated exponential polynomials:

https://mattbaker.blog/2014/05/02/newton-polygons-and-galois-groups/#more-612

However, it may be better to start from somewhere and then incrementally generalize.

Riccardo Brasca (Jan 20 2022 at 20:27):

Mmh, wikipedia agrees with your definition...

Riccardo Brasca (Jan 20 2022 at 20:28):

So let's drop monic

Damiano Testa (Jan 20 2022 at 20:33):

Honestly, for me "Eisenstein" either means "prove the p'th cyclotomic polynomial is irreducible" or is a special case of Newton polygons. All these questions of generalizations are mostly academic... :shrug:

Riccardo Brasca (Jan 20 2022 at 20:57):

The criterion I am proving is really useful in real life. The first example is of course cyclotomic fields, but any time one is able to compute the discriminant of a number field it is a good try to compute the ring of integers.

Riccardo Brasca (Jan 24 2022 at 19:25):

In #11577 I've PRed some technical lemmas, like

lemma pow_nat_degree_le_of_aeval_zero_of_eisenstein_criterion_mem_map [algebra R S] {x : S}
  {f : polynomial R} (hx : aeval x f = 0) (hmo : f.monic)
  (hdiv : ∀ n < f.nat_degree, f.coeff n ∈ p) :
  ∀ i, (f.map (algebra_map R S)).nat_degree ≤ i → x ^ i ∈ p.map (algebra_map R S)

I will use these for Eisenstein polynomials, but the real hypothesis is weaker than being Eiseinstein, so I put them in the most basic file I found.

Would it be reasonable to have them in the file about Eiseinstein polynomials? (In this case we can have them as stated, or directly for Eiseinstein polynomials. Or maybe we can have something like is_weak_eisenstein_at.) Note that this file will import a lot of stuff, since the interesting results about Eisenstein polynomials require quite a big machinery to be proved.

Riccardo Brasca (Jan 26 2022 at 16:09):

After some thinking I am now convinced it's OK to have these results in the eiseinstein.lean file, even if importing it it's not very convenient. The reason is that these results are really technical, and probably nobody will ever use them.

Johan Commelin (Jan 26 2022 at 16:11):

Sorry, I missed your previous message. I think it's fine that a file on Eisenstein polynomials has heavy imports. If it becomes a problem, we can restructure later.

Riccardo Brasca (Jan 26 2022 at 16:11):

No problem :)

Johan Commelin (Jan 26 2022 at 16:11):

It's pretty "advanced" stuff, for mathlib. So it can import a lot.

Last updated: Dec 20 2023 at 11:08 UTC