mathlib documentation

ring_theory.polynomial.eisenstein

Eisenstein polynomials #

Given an ideal π“Ÿ of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at π“Ÿ if f.leading_coeff βˆ‰ π“Ÿ, βˆ€ n, n < f.nat_degree β†’ f.coeff n ∈ π“Ÿ and f.coeff 0 βˆ‰ π“Ÿ ^ 2. In this file we gather miscellaneous results about Eisenstein polynomials.

Main definitions #

Main results #

Implementation details #

We also define a notion is_weakly_eisenstein_at requiring only that βˆ€ n < f.nat_degree β†’ 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.is_weakly_eisenstein_at_iff {R : Type u} [comm_semiring R] (f : polynomial R) (π“Ÿ : ideal R) :
f.is_weakly_eisenstein_at π“Ÿ ↔ βˆ€ {n : β„•}, n < f.nat_degree β†’ f.coeff n ∈ π“Ÿ
structure polynomial.is_weakly_eisenstein_at {R : Type u} [comm_semiring 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.nat_degree β†’ f.coeff n ∈ π“Ÿ.

structure polynomial.is_eisenstein_at {R : Type u} [comm_semiring 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.leading_coeff βˆ‰ π“Ÿ, βˆ€ n, n < f.nat_degree β†’ f.coeff n ∈ π“Ÿ and f.coeff 0 βˆ‰ π“Ÿ ^ 2.

theorem polynomial.is_eisenstein_at_iff {R : Type u} [comm_semiring R] (f : polynomial R) (π“Ÿ : ideal R) :
f.is_eisenstein_at π“Ÿ ↔ f.leading_coeff βˆ‰ π“Ÿ ∧ (βˆ€ {n : β„•}, n < f.nat_degree β†’ f.coeff n ∈ π“Ÿ) ∧ f.coeff 0 βˆ‰ π“Ÿ ^ 2
theorem polynomial.is_weakly_eisenstein_at.map {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.is_weakly_eisenstein_at π“Ÿ) {A : Type v} [comm_ring A] (Ο† : R β†’+* A) :
theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree {R : Type u} [comm_ring R] {f : polynomial R} {S : Type v} [comm_ring S] [algebra R S] {p : R} {x : S} (hx : ⇑(polynomial.aeval x) f = 0) (hmo : f.monic) (hf : f.is_weakly_eisenstein_at (submodule.span R {p})) :
βˆƒ (y : S) (H : y ∈ algebra.adjoin R {x}), ⇑(algebra_map R S) p * y = x ^ (polynomial.map (algebra_map R S) f).nat_degree
theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le {R : Type u} [comm_ring R] {f : polynomial R} {S : Type v} [comm_ring S] [algebra R S] {p : R} {x : S} (hx : ⇑(polynomial.aeval x) f = 0) (hmo : f.monic) (hf : f.is_weakly_eisenstein_at (submodule.span R {p})) (i : β„•) :
(polynomial.map (algebra_map R S) f).nat_degree ≀ i β†’ (βˆƒ (y : S) (H : y ∈ algebra.adjoin R {x}), ⇑(algebra_map R S) p * y = x ^ i)
theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_root_of_monic_mem {R : Type u} [comm_ring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.is_weakly_eisenstein_at π“Ÿ) {x : R} (hroot : f.is_root x) (hmo : f.monic) (i : β„•) :
f.nat_degree ≀ i β†’ x ^ i ∈ π“Ÿ
theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_aeval_zero_of_monic_mem_map {R : Type u} [comm_ring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.is_weakly_eisenstein_at π“Ÿ) {S : Type v} [comm_ring S] [algebra R S] {x : S} (hx : ⇑(polynomial.aeval x) f = 0) (hmo : f.monic) (i : β„•) :
theorem polynomial.scale_roots.is_weakly_eisenstein_at {R : Type u} [comm_ring R] (p : polynomial R) {x : R} {P : ideal R} (hP : x ∈ P) :
theorem polynomial.dvd_pow_nat_degree_of_evalβ‚‚_eq_zero {R : Type u} {A : Type u_1} [comm_ring R] [comm_ring A] {f : R β†’+* A} (hf : function.injective ⇑f) {p : polynomial R} (hp : p.monic) (x y : R) (z : A) (h : polynomial.evalβ‚‚ f z p = 0) (hz : ⇑f x * z = ⇑f y) :
theorem polynomial.dvd_pow_nat_degree_of_aeval_eq_zero {R : Type u} {A : Type u_1} [comm_ring R] [comm_ring A] [algebra R A] [nontrivial A] [no_zero_smul_divisors R A] {p : polynomial R} (hp : p.monic) (x y : R) (z : A) (h : ⇑(polynomial.aeval z) p = 0) (hz : z * ⇑(algebra_map R A) x = ⇑(algebra_map R A) y) :
theorem polynomial.monic.leading_coeff_not_mem {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.monic) (h : π“Ÿ β‰  ⊀) :
theorem polynomial.monic.is_eisenstein_at_of_mem_of_not_mem {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.monic) (h : π“Ÿ β‰  ⊀) (hmem : βˆ€ {n : β„•}, n < f.nat_degree β†’ f.coeff n ∈ π“Ÿ) (hnot_mem : f.coeff 0 βˆ‰ π“Ÿ ^ 2) :
f.is_eisenstein_at π“Ÿ
theorem polynomial.is_eisenstein_at.is_weakly_eisenstein_at {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.is_eisenstein_at π“Ÿ) :
theorem polynomial.is_eisenstein_at.coeff_mem {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.is_eisenstein_at π“Ÿ) {n : β„•} (hn : n β‰  f.nat_degree) :
f.coeff n ∈ π“Ÿ
theorem polynomial.is_eisenstein_at.irreducible {R : Type u} [comm_ring R] [is_domain R] {π“Ÿ : ideal R} {f : polynomial R} (hf : f.is_eisenstein_at π“Ÿ) (hprime : π“Ÿ.is_prime) (hu : f.is_primitive) (hfd0 : 0 < f.nat_degree) :

If a primitive f satisfies f.is_eisenstein_at π“Ÿ, where π“Ÿ.is_prime, then f is irreducible.

theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K] [is_integrally_closed R] {B : power_basis K L} (hp : prime p) (hBint : is_integral R B.gen) {z : L} {Q : polynomial R} (hQ : ⇑(polynomial.aeval B.gen) Q = p β€’ z) (hzint : is_integral R z) (hei : (minpoly R B.gen).is_eisenstein_at (submodule.span R {p})) :

Let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if Q : polynomial R is such that aeval B.gen Q = p β€’ z, then p ∣ Q.coeff 0.

theorem mem_adjoin_of_dvd_coeff_of_dvd_aeval {A : Type u_1} {B : Type u_2} [comm_semiring A] [comm_ring B] [algebra A B] [no_zero_smul_divisors A B] {Q : polynomial A} {p : A} {x z : B} (hp : p β‰  0) (hQ : βˆ€ (i : β„•), i ∈ finset.range (Q.nat_degree + 1) β†’ p ∣ Q.coeff i) (hz : ⇑(polynomial.aeval x) Q = p β€’ z) :
theorem mem_adjoin_of_smul_prime_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K] [is_integrally_closed R] {B : power_basis K L} (hp : prime p) (hBint : is_integral R B.gen) {z : L} (hzint : is_integral R z) (hz : p β€’ z ∈ algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).is_eisenstein_at (submodule.span R {p})) :

Let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if p β€’ z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}.

theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K] [is_integrally_closed R] {B : power_basis K L} (hp : prime p) (hBint : is_integral R B.gen) {n : β„•} {z : L} (hzint : is_integral R z) (hz : p ^ n β€’ z ∈ algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).is_eisenstein_at (submodule.span R {p})) :

Let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if p ^ n β€’ z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}. Together with algebra.discr_mul_is_integral_mem_adjoin this result often allows to compute the ring of integers of L.