Eisenstein polynomials

Given an ideal 𝓟 of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at 𝓟 if f.leadingCoeff ∉ 𝓟, ∀ n, n < f.natDegree → f.coeff n ∈ 𝓟 and f.coeff 0 ∉ 𝓟 ^ 2. In this file we gather miscellaneous results about Eisenstein polynomials.

Main definitions

• Polynomial.IsEisensteinAt f 𝓟: the property of being Eisenstein at 𝓟.

Main results

• Polynomial.IsEisensteinAt.irreducible: if a primitive f satisfies f.IsEisensteinAt 𝓟, where 𝓟.IsPrime, then f is irreducible.

Implementation details

We also define a notion IsWeaklyEisensteinAt requiring only that ∀ n < f.natDegree → f.coeff n ∈ 𝓟. This makes certain results slightly more general and it is useful since it is sometimes better behaved (for example it is stable under Polynomial.map).

theorem Polynomial.isWeaklyEisensteinAt_iff {R : Type u} [CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R) : Polynomial.IsWeaklyEisensteinAt f 𝓟 ↔ ∀ {n : ℕ}, n < Polynomial.natDegree f → Polynomial.coeff f n ∈ 𝓟

structure Polynomial.IsWeaklyEisensteinAt {R : Type u} [CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R) : Prop

Given an ideal 𝓟 of a commutative semiring R, we say that a polynomial f : R[X] is weakly Eisenstein at 𝓟 if ∀ n, n < f.natDegree → f.coeff n ∈ 𝓟.

• mem : ∀ {n : ℕ}, n < Polynomial.natDegree f → Polynomial.coeff f n ∈ 𝓟

theorem Polynomial.isEisensteinAt_iff {R : Type u} [CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R) : Polynomial.IsEisensteinAt f 𝓟 ↔ Polynomial.leadingCoeff f ∉ 𝓟 ∧ (∀ {n : ℕ}, n < Polynomial.natDegree f → Polynomial.coeff f n ∈ 𝓟) ∧ Polynomial.coeff f 0 ∉ 𝓟 ^ 2

structure Polynomial.IsEisensteinAt {R : Type u} [CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R) : Prop

Given an ideal 𝓟 of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at 𝓟 if f.leadingCoeff ∉ 𝓟, ∀ n, n < f.natDegree → f.coeff n ∈ 𝓟 and f.coeff 0 ∉ 𝓟 ^ 2.

• leading : Polynomial.leadingCoeff f ∉ 𝓟
• mem : ∀ {n : ℕ}, n < Polynomial.natDegree f → Polynomial.coeff f n ∈ 𝓟
• not_mem : Polynomial.coeff f 0 ∉ 𝓟 ^ 2

theorem Polynomial.IsWeaklyEisensteinAt.map {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.IsWeaklyEisensteinAt f 𝓟) {A : Type v} [CommRing A] (φ : R →+* A) : Polynomial.IsWeaklyEisensteinAt (Polynomial.map φ f) (Ideal.map φ 𝓟)

theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : Polynomial.Monic f) (hf : Polynomial.IsWeaklyEisensteinAt f (Submodule.span R {p})) : ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ Polynomial.natDegree (Polynomial.map (algebraMap R S) f)

theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : Polynomial.Monic f) (hf : Polynomial.IsWeaklyEisensteinAt f (Submodule.span R {p})) (i : ℕ) : Polynomial.natDegree (Polynomial.map (algebraMap R S) f) ≤ i → ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ i

theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem {R : Type u} [CommRing R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.IsWeaklyEisensteinAt f 𝓟) {x : R} (hroot : Polynomial.IsRoot f x) (hmo : Polynomial.Monic f) (i : ℕ) : Polynomial.natDegree f ≤ i → x ^ i ∈ 𝓟

theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map {R : Type u} [CommRing R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.IsWeaklyEisensteinAt f 𝓟) {S : Type v} [CommRing S] [Algebra R S] {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : Polynomial.Monic f) (i : ℕ) : Polynomial.natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

theorem Polynomial.scaleRoots.isWeaklyEisensteinAt {R : Type u} [CommRing R] (p : Polynomial R) {x : R} {P : Ideal R} (hP : x ∈ P) : Polynomial.IsWeaklyEisensteinAt (Polynomial.scaleRoots p x) P

theorem Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero {R : Type u} {A : Type u_1} [CommRing R] [CommRing A] {f : R →+* A} (hf : Function.Injective ⇑f) {p : Polynomial R} (hp : Polynomial.Monic p) (x : R) (y : R) (z : A) (h : Polynomial.eval₂ f z p = 0) (hz : f x * z = f y) : x ∣ y ^ Polynomial.natDegree p

theorem Polynomial.dvd_pow_natDegree_of_aeval_eq_zero {R : Type u} {A : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial A] [NoZeroSMulDivisors R A] {p : Polynomial R} (hp : Polynomial.Monic p) (x : R) (y : R) (z : A) (h : (Polynomial.aeval z) p = 0) (hz : z * (algebraMap R A) x = (algebraMap R A) y) : x ∣ y ^ Polynomial.natDegree p

theorem Polynomial.Monic.leadingCoeff_not_mem {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.Monic f) (h : 𝓟 ≠ ⊤) : Polynomial.leadingCoeff f ∉ 𝓟

theorem Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.Monic f) (h : 𝓟 ≠ ⊤) (hmem : ∀ {n : ℕ}, n < Polynomial.natDegree f → Polynomial.coeff f n ∈ 𝓟) (hnot_mem : Polynomial.coeff f 0 ∉ 𝓟 ^ 2) : Polynomial.IsEisensteinAt f 𝓟

theorem Polynomial.IsEisensteinAt.isWeaklyEisensteinAt {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.IsEisensteinAt f 𝓟) : Polynomial.IsWeaklyEisensteinAt f 𝓟

theorem Polynomial.IsEisensteinAt.coeff_mem {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.IsEisensteinAt f 𝓟) {n : ℕ} (hn : n ≠ Polynomial.natDegree f) : Polynomial.coeff f n ∈ 𝓟

theorem Polynomial.IsEisensteinAt.irreducible {R : Type u} [CommRing R] [IsDomain R] {𝓟 : Ideal R} {f : Polynomial R} (hf : Polynomial.IsEisensteinAt f 𝓟) (hprime : Ideal.IsPrime 𝓟) (hu : Polynomial.IsPrimitive f) (hfd0 : 0 < Polynomial.natDegree f) : Irreducible f

If a primitive f satisfies f.IsEisensteinAt 𝓟, where 𝓟.IsPrime, then f is irreducible.