Eisenstein polynomials

In this file we gather more miscellaneous results about Eisenstein polynomials

Main results

• mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt: 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_isIntegral_mem_adjoin this result often allows to compute the ring of integers of L.

theorem cyclotomic_comp_X_add_one_isEisensteinAt (p : ℕ) [hp : Fact (Nat.Prime p)] : Polynomial.IsEisensteinAt (Polynomial.comp (Polynomial.cyclotomic p ℤ) (Polynomial.X + 1)) (Submodule.span ℤ {↑p})

theorem cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : Polynomial.IsEisensteinAt (Polynomial.comp (Polynomial.cyclotomic (p ^ (n + 1)) ℤ) (Polynomial.X + 1)) (Submodule.span ℤ {↑p})

theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [CommRing R] [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] [IsSeparable K L] [IsDomain R] [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L} (hp : Prime p) (hBint : IsIntegral R B.gen) {z : L} {Q : Polynomial R} (hQ : (Polynomial.aeval B.gen) Q = p • z) (hzint : IsIntegral R z) (hei : Polynomial.IsEisensteinAt (minpoly R B.gen) (Submodule.span R {p})) : p ∣ Polynomial.coeff Q 0

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 : R[X] 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} [CommSemiring A] [CommRing B] [Algebra A B] [NoZeroSMulDivisors A B] {Q : Polynomial A} {p : A} {x : B} {z : B} (hp : p ≠ 0) (hQ : ∀ i ∈ Finset.range (Polynomial.natDegree Q + 1), p ∣ Polynomial.coeff Q i) (hz : (Polynomial.aeval x) Q = p • z) : z ∈ Algebra.adjoin A {x}

theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [CommRing R] [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] [IsSeparable K L] [IsDomain R] [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L} (hp : Prime p) (hBint : IsIntegral R B.gen) {z : L} (hzint : IsIntegral R z) (hz : p • z ∈ Algebra.adjoin R {B.gen}) (hei : Polynomial.IsEisensteinAt (minpoly R B.gen) (Submodule.span R {p})) : z ∈ Algebra.adjoin R {B.gen}

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_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [CommRing R] [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] [IsSeparable K L] [IsDomain R] [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L} (hp : Prime p) (hBint : IsIntegral R B.gen) {n : ℕ} {z : L} (hzint : IsIntegral R z) (hz : p ^ n • z ∈ Algebra.adjoin R {B.gen}) (hei : Polynomial.IsEisensteinAt (minpoly R B.gen) (Submodule.span R {p})) : z ∈ Algebra.adjoin R {B.gen}

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_isIntegral_mem_adjoin this result often allows to compute the ring of integers of L.