feat(ring_theory/polynomial/eisenstein): add a technical lemma (#11839)

A technical lemma about Eiseinstein minimal polynomials.

From flt-regular

Author: riccardobrasca

src/algebra/associated.lean

@@ -129,6 +129,27 @@ lemma prime.pow_dvd_of_dvd_mul_right
   {p a b : α} (hp : prime p) (n : ℕ) (h : ¬p ∣ b) (h' : p ^ n ∣ a * b) : p ^ n ∣ a :=
 by { rw [mul_comm] at h', exact hp.pow_dvd_of_dvd_mul_left n h h' }
 
+lemma prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd [cancel_comm_monoid_with_zero α]
+  {p a b : α} {n : ℕ} (hp : prime p) (hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n)
+  (hb : ¬ p ^ 2 ∣ b) : p ∣ a :=
+begin
+  -- Suppose `p ∣ b`, write `b = p * x` and `hy : a ^ n.succ * b ^ n = p ^ n.succ * y`.
+  cases (hp.dvd_or_dvd ((dvd_pow_self p (nat.succ_ne_zero n)).trans hpow)) with H hbdiv,
+  { exact hp.dvd_of_dvd_pow H },
+  obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv,
+  obtain ⟨y, hy⟩ := hpow,
+  -- Then we can divide out a common factor of `p ^ n` from the equation `hy`.
+  have : a ^ n.succ * x ^ n = p * y,
+  { refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) _,
+    rw [← mul_assoc _ p, ← pow_succ', ← hy, mul_pow, ← mul_assoc (a ^ n.succ),
+      mul_comm _ (p ^ n), mul_assoc] },
+  -- So `p ∣ a` (and we're done) or `p ∣ x`, which can't be the case since it implies `p^2 ∣ b`.
+  refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right (λ hdvdx, hb _)),
+  obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx,
+  rw [pow_two, ← mul_assoc],
+  exact dvd_mul_right _ _,
+end
+
 /-- `irreducible p` states that `p` is non-unit and only factors into units.
 
 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a

src/data/nat/basic.lean

@@ -607,6 +607,12 @@ theorem mul_self_inj {n m : ℕ} : n * n = m * m ↔ n = m :=
 le_antisymm_iff.trans (le_antisymm_iff.trans
   (and_congr mul_self_le_mul_self_iff mul_self_le_mul_self_iff)).symm
 
+lemma le_add_pred_of_pos (n : ℕ) {i : ℕ} (hi : i ≠ 0) : n ≤ i + (n - 1) :=
+begin
+  refine le_trans _ (add_tsub_le_assoc),
+  simp [add_comm, nat.add_sub_assoc, one_le_iff_ne_zero.2 hi]
+end
+
 /-!
 ### Recursion and induction principles
 

src/data/polynomial/monic.lean

@@ -307,6 +307,28 @@ have (-q).coeff (-q).nat_degree = 1 :=
 by rw [nat_degree_neg, coeff_neg, show q.coeff q.nat_degree = -1, from hq, neg_neg],
 by { rw sub_eq_add_neg, apply monic_add_of_right this, rwa degree_neg }
 
+@[simp]
+lemma nat_degree_map_of_monic [semiring S] [nontrivial S] {P : polynomial R} (hmo : P.monic)
+  (f : R →+* S) : (P.map f).nat_degree = P.nat_degree :=
+begin
+  refine le_antisymm (nat_degree_map_le _ _) (le_nat_degree_of_ne_zero _),
+  rw [coeff_map, monic.coeff_nat_degree hmo, ring_hom.map_one],
+  exact one_ne_zero
+end
+
+@[simp]
+lemma degree_map_of_monic [semiring S] [nontrivial S] {P : polynomial R} (hmo : P.monic)
+  (f : R →+* S) : (P.map f).degree = P.degree :=
+begin
+  by_cases hP : P = 0,
+  { simp [hP] },
+  { refine le_antisymm (degree_map_le _ _) _,
+    rw [degree_eq_nat_degree hP],
+    refine le_degree_of_ne_zero _,
+    rw [coeff_map, monic.coeff_nat_degree hmo, ring_hom.map_one],
+    exact one_ne_zero }
+end
+
 section injective
 open function
 variables [semiring S] {f : R →+* S} (hf : injective f)

src/ring_theory/integral_closure.lean

@@ -351,6 +351,13 @@ theorem is_integral_mul {x y : A}
   (hx : is_integral R x) (hy : is_integral R y) : is_integral R (x * y) :=
 (algebra_map R A).is_integral_mul hx hy
 
+lemma is_integral_smul [algebra S A] [algebra R S] [is_scalar_tower R S A] {x : A} (r : R)
+  (hx : is_integral S x) : is_integral S (r • x) :=
+begin
+  rw [algebra.smul_def, is_scalar_tower.algebra_map_apply R S A],
+  exact is_integral_mul is_integral_algebra_map hx,
+end
+
 variables (R A)
 
 /-- The integral closure of R in an R-algebra A. -/

src/ring_theory/polynomial/eisenstein.lean

@@ -5,6 +5,8 @@ Authors: Riccardo Brasca
 -/
 
 import ring_theory.eisenstein_criterion
+import ring_theory.integrally_closed
+import ring_theory.norm
 
 /-!
 # Eisenstein polynomials
@@ -13,10 +15,10 @@ Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f
 `f.coeff 0 ∉ 𝓟 ^ 2`. In this file we gather miscellaneous results about Eisenstein polynomials.
 
 ## Main definitions
-* `polynomial.is_eisenstein_at f 𝓟` : the property of being Eisenstein at `𝓟`.
+* `polynomial.is_eisenstein_at f 𝓟`: the property of being Eisenstein at `𝓟`.
 
 ## Main results
-* `polynomial.is_eisenstein_at.irreducible` : if a primitive `f` satisfies `f.is_eisenstein_at 𝓟`,
+* `polynomial.is_eisenstein_at.irreducible`: if a primitive `f` satisfies `f.is_eisenstein_at 𝓟`,
   where `𝓟.is_prime`, then `f` is irreducible.
 
 ## Implementation details
@@ -26,7 +28,7 @@ useful since it is sometimes better behaved (for example it is stable under `pol
 
 -/
 
-universes u v
+universes u v w z
 
 variables {R : Type u}
 
@@ -185,3 +187,95 @@ end is_domain
 end is_eisenstein_at
 
 end polynomial
+
+section is_integral
+
+variables {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L]
+variables [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L]
+variables [is_domain R] [normalized_gcd_monoid R] [is_fraction_ring R K] [is_integrally_closed R]
+
+local notation `𝓟` := submodule.span R {p}
+
+open is_integrally_closed power_basis nat polynomial is_scalar_tower
+
+/-- 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. Given `z : L` integral over `R`, if `Q : polynomial R` is such that
+`aeval B.gen Q = p • z`, then `p ∣ Q.coeff 0`. -/
+lemma dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at {B : power_basis K L}
+  (hp : prime p) (hei : (minpoly R B.gen).is_eisenstein_at 𝓟) (hBint : is_integral R B.gen) {z : L}
+  {Q : polynomial R} (hQ : aeval B.gen Q = p • z) (hzint : is_integral R z) :
+  p ∣ Q.coeff 0 :=
+begin
+  -- First define some abbreviations.
+  letI := B.finite_dimensional,
+  let P := minpoly R B.gen,
+  obtain ⟨n , hn⟩ := nat.exists_eq_succ_of_ne_zero B.dim_pos.ne',
+  have finrank_K_L : finite_dimensional.finrank K L = B.dim := B.finrank,
+  have deg_K_P : (minpoly K B.gen).nat_degree = B.dim := B.nat_degree_minpoly,
+  have deg_R_P : P.nat_degree = B.dim,
+  { rw [← deg_K_P, minpoly.gcd_domain_eq_field_fractions K hBint,
+        nat_degree_map_of_monic (minpoly.monic hBint) (algebra_map R K)] },
+  choose! f hf using hei.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le
+    (minpoly.aeval R B.gen) (minpoly.monic hBint),
+  simp only [nat_degree_map_of_monic (minpoly.monic hBint), deg_R_P] at hf,
+
+  -- The Eisenstein condition shows that `p` divides `Q.coeff 0`
+  -- if `p^n` divides the following multiple of `Q^n`:
+  suffices : p ^ n.succ ∣
+    (Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)),
+  { have hndiv : ¬ p ^ 2 ∣ ((minpoly R B.gen)).coeff 0 := λ h,
+      hei.not_mem ((span_singleton_pow p 2).symm ▸ (ideal.mem_span_singleton.2 h)),
+    refine prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd hp ((_ : _ ^ n.succ ∣ _)) hndiv,
+    convert (is_unit.dvd_mul_right ⟨(-1) ^ (n.succ * n), rfl⟩).mpr this using 1,
+    push_cast,
+    ring_nf, simp [pow_right_comm _ _ 2] },
+
+  -- We claim the quotient of `Q^n * _` by `p^n` is the following `r`:
+  have aux : ∀ i ∈ (range (Q.nat_degree + 1)).erase 0, B.dim ≤ i + n,
+  { intros i hi,
+    simp only [mem_range, mem_erase] at hi,
+    rw [hn],
+    exact le_add_pred_of_pos _ hi.1 },
+  have hintsum : is_integral R (z * B.gen ^ n -
+    ∑ (x : ℕ) in (range (Q.nat_degree + 1)).erase 0, Q.coeff x • f (x + n)),
+  { refine is_integral_sub (is_integral_mul hzint (is_integral.pow hBint _))
+      (is_integral.sum _ (λ i hi, (is_integral_smul _ _))),
+    exact adjoin_le_integral_closure hBint (hf _ (aux i hi)).1 },
+  obtain ⟨r, hr⟩ := is_integral_iff.1 (is_integral_norm K hintsum),
+  use r,
+
+  -- Do the computation in `K` so we can work in terms of `z` instead of `r`.
+  apply is_fraction_ring.injective R K,
+  simp only [_root_.map_mul, _root_.map_pow, _root_.map_neg, _root_.map_one],
+  -- Both sides are actually norms:
+  calc _ = norm K (Q.coeff 0 • B.gen ^ n) : _
+  ... = norm K (p • (z * B.gen ^ n) - ∑ (x : ℕ) in (range (Q.nat_degree + 1)).erase 0,
+          p • Q.coeff x • f (x + n))
+    : congr_arg (norm K) (eq_sub_of_add_eq _)
+  ... = _ : _,
+  { simp only [algebra.smul_def, algebra_map_apply R K L, norm_algebra_map, _root_.map_mul,
+      _root_.map_pow, finrank_K_L, power_basis.norm_gen_eq_coeff_zero_minpoly,
+      minpoly.gcd_domain_eq_field_fractions K hBint, coeff_map, ← hn],
+    ring_exp },
+  swap, { simp_rw [← smul_sum, ← smul_sub, algebra.smul_def p, algebra_map_apply R K L,
+      _root_.map_mul, norm_algebra_map, finrank_K_L, hr, ← hn] },
+
+  calc _ = (Q.coeff 0 • 1 + ∑ (x : ℕ) in (range (Q.nat_degree + 1)).erase 0,
+              Q.coeff x • B.gen ^ x) * B.gen ^ n : _
+  ... = (Q.coeff 0 • B.gen ^ 0 + ∑ (x : ℕ) in (range (Q.nat_degree + 1)).erase 0,
+              Q.coeff x • B.gen ^ x) * B.gen ^ n : by rw pow_zero
+  ... = (aeval B.gen Q) * B.gen ^ n : _
+  ... = _ : by rw [hQ, algebra.smul_mul_assoc],
+  { have : ∀ i ∈ (range (Q.nat_degree + 1)).erase 0,
+      Q.coeff i • (B.gen ^ i * B.gen ^ n) =
+      p • Q.coeff i • f (i + n),
+    { intros i hi,
+      rw [← pow_add, ← (hf _ (aux i hi)).2, ← smul_def, smul_smul, mul_comm _ p, smul_smul] },
+    simp only [add_mul, smul_mul_assoc, one_mul, sum_mul, sum_congr rfl this] },
+  { rw [aeval_eq_sum_range,
+        finset.add_sum_erase (range (Q.nat_degree + 1)) (λ i, Q.coeff i • B.gen ^ i)],
+    simp },
+end
+
+end is_integral