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).

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 < f.natDegree → f.coeff n ∈ 𝓟

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

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

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 : f.leadingCoeff ∉ 𝓟
• mem : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
• not_mem : f.coeff 0 ∉ 𝓟 ^ 2

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

theorem Polynomial.IsEisensteinAt.leading {R : Type u} [CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R} (self : f.IsEisensteinAt 𝓟) : f.leadingCoeff ∉ 𝓟

theorem Polynomial.IsEisensteinAt.mem {R : Type u} [CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R} (self : f.IsEisensteinAt 𝓟) {n : ℕ} : n < f.natDegree → f.coeff n ∈ 𝓟

theorem Polynomial.IsEisensteinAt.not_mem {R : Type u} [CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R} (self : f.IsEisensteinAt 𝓟) : f.coeff 0 ∉ 𝓟 ^ 2

theorem Polynomial.IsWeaklyEisensteinAt.map {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : f.IsWeaklyEisensteinAt 𝓟) {A : Type v} [CommRing A] (φ : R →+* A) : (Polynomial.map φ f).IsWeaklyEisensteinAt (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 : f.Monic) (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) : ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

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 : f.Monic) (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) (i : ℕ) : (Polynomial.map (algebraMap R S) f).natDegree ≤ 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 : f.IsWeaklyEisensteinAt 𝓟) {x : R} (hroot : f.IsRoot x) (hmo : f.Monic) (i : ℕ) : f.natDegree ≤ 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} {S : Type v} [CommRing S] [Algebra R S] (hf : f.IsWeaklyEisensteinAt 𝓟) {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (i : ℕ) : (Polynomial.map (algebraMap R S) f).natDegree ≤ 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) : (p.scaleRoots x).IsWeaklyEisensteinAt 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 : p.Monic) (x : R) (y : R) (z : A) (h : Polynomial.eval₂ f z p = 0) (hz : f x * z = f y) : x ∣ y ^ p.natDegree

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 : p.Monic) (x : R) (y : R) (z : A) (h : (Polynomial.aeval z) p = 0) (hz : z * (algebraMap R A) x = (algebraMap R A) y) : x ∣ y ^ p.natDegree

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

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

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

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

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

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