feat(ring_theory/polynomial/eisenstein): add cyclotomic_comp_X_add_one_is_eisenstein_at (#12447)

We add `cyclotomic_comp_X_add_one_is_eisenstein_at`: `(cyclotomic p ℤ).comp (X + 1)` is Eisenstein at `p`.

From flt-regular

Author: riccardobrasca

src/data/polynomial/coeff.lean

@@ -169,6 +169,17 @@ theorem mul_X_pow_eq_zero {p : R[X]} {n : ℕ}
   (H : p * X ^ n = 0) : p = 0 :=
 ext $ λ k, (coeff_mul_X_pow p n k).symm.trans $ ext_iff.1 H (k+n)
 
+lemma mul_X_pow_injective (n : ℕ) : function.injective (λ P : R[X], X ^ n * P) :=
+begin
+  intros P Q hPQ,
+  simp only at hPQ,
+  ext i,
+  rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
+end
+
+lemma mul_X_injective : function.injective (λ P : R[X], X * P) :=
+by simpa only [pow_one] using mul_X_pow_injective 1
+
 lemma C_mul_X_pow_eq_monomial (c : R) (n : ℕ) : C c * X^n = monomial n c :=
 by { ext1, rw [monomial_eq_smul_X, coeff_smul, coeff_C_mul, smul_eq_mul] }
 

src/field_theory/minpoly.lean

@@ -359,7 +359,7 @@ minpoly.unique _ _ (minpoly.monic hx)
     (is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero K S T hST
       (h ▸ root_q : polynomial.aeval (algebra_map S T x) q = 0)))
 
-lemma minpoly_add_algebra_map {B : Type*} [comm_ring B] [algebra A B] {x : B}
+lemma add_algebra_map {B : Type*} [comm_ring B] [algebra A B] {x : B}
   (hx : is_integral A x) (a : A) :
   minpoly A (x + (algebra_map A B a)) = (minpoly A x).comp (X - C a) :=
 begin
@@ -375,10 +375,10 @@ begin
       nat_degree_X_add_C, mul_one] at H }
 end
 
-lemma minpoly_sub_algebra_map {B : Type*} [comm_ring B] [algebra A B] {x : B}
+lemma sub_algebra_map {B : Type*} [comm_ring B] [algebra A B] {x : B}
   (hx : is_integral A x) (a : A) :
   minpoly A (x - (algebra_map A B a)) = (minpoly A x).comp (X + C a) :=
-by simpa [sub_eq_add_neg] using minpoly_add_algebra_map hx (-a)
+by simpa [sub_eq_add_neg] using add_algebra_map hx (-a)
 
 section gcd_domain
 

src/number_theory/cyclotomic/primitive_roots.lean

@@ -222,6 +222,15 @@ begin
   { exact hζ.norm_eq_one hn hirr }
 end
 
+lemma minpoly_sub_one_eq_cyclotomic_comp [is_cyclotomic_extension {n} K L]
+  (h : irreducible (polynomial.cyclotomic n K)) :
+  minpoly K (ζ - 1) = (cyclotomic n K).comp (X + 1) :=
+begin
+  rw [show ζ - 1 = ζ + (algebra_map K L (-1)), by simp [sub_eq_add_neg], minpoly.add_algebra_map
+    (is_cyclotomic_extension.integral {n} K L ζ), hζ.minpoly_eq_cyclotomic_of_irreducible h],
+  simp
+end
+
 /-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of
 `ζ - 1` is `eval 1 (cyclotomic n ℤ)`. -/
 lemma sub_one_norm_eq_eval_cyclotomic [is_cyclotomic_extension {n} K L]

src/ring_theory/polynomial/basic.lean

@@ -215,6 +215,56 @@ begin
   refl,
 end
 
+lemma geom_sum_X_comp_X_add_one_eq_sum (n : ℕ) :
+  (geom_sum (X : R[X]) n).comp (X + 1) =
+  (finset.range n).sum (λ (i : ℕ), (n.choose (i + 1) : R[X]) * X ^ i) :=
+begin
+  ext i,
+  transitivity (n.choose (i + 1) : R), swap,
+  { simp only [finset_sum_coeff, ← C_eq_nat_cast, coeff_C_mul_X_pow],
+    rw [finset.sum_eq_single i, if_pos rfl],
+    { simp only [@eq_comm _ i, if_false, eq_self_iff_true, implies_true_iff] {contextual := tt}, },
+    { simp only [nat.lt_add_one_iff, nat.choose_eq_zero_of_lt, nat.cast_zero, finset.mem_range,
+        not_lt, eq_self_iff_true, if_true, implies_true_iff] {contextual := tt}, } },
+  induction n with n ih generalizing i,
+  { simp only [geom_sum_zero, zero_comp, coeff_zero, nat.choose_zero_succ, nat.cast_zero], },
+  simp only [geom_sum_succ', ih, add_comp, pow_comp, X_comp, coeff_add, nat.choose_succ_succ,
+    nat.cast_add, add_pow, one_pow, mul_one, finset_sum_coeff, ← C_eq_nat_cast, mul_comm _ (C _),
+    coeff_C_mul_X_pow],
+  rw [finset.sum_eq_single i, if_pos rfl],
+  { simp only [@eq_comm _ i, if_false, eq_self_iff_true, implies_true_iff] {contextual := tt}, },
+  { simp only [nat.lt_add_one_iff, nat.choose_eq_zero_of_lt, nat.cast_zero, finset.mem_range,
+      eq_self_iff_true, if_true, implies_true_iff, not_le] {contextual := tt}, },
+end
+
+lemma monic.geom_sum {R : Type*} [semiring R] {P : R[X]}
+  (hP : P.monic) (hdeg : 0 < P.nat_degree) {n : ℕ} (hn : n ≠ 0) : (geom_sum P n).monic :=
+begin
+  nontriviality R,
+  cases n, { exact (hn rfl).elim },
+  rw [geom_sum_succ', geom_sum_def],
+  refine monic_add_of_left (monic_pow hP _) _,
+  refine lt_of_le_of_lt (degree_sum_le _ _) _,
+  rw [finset.sup_lt_iff],
+  { simp only [finset.mem_range, degree_eq_nat_degree (monic_pow hP _).ne_zero,
+      with_bot.coe_lt_coe, hP.nat_degree_pow],
+    intro k, exact nsmul_lt_nsmul hdeg },
+  { rw [bot_lt_iff_ne_bot, ne.def, degree_eq_bot],
+    exact (monic_pow hP _).ne_zero }
+end
+
+lemma monic.geom_sum' {R : Type*} [semiring R] {P : R[X]}
+  (hP : P.monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (geom_sum P n).monic :=
+hP.geom_sum (nat_degree_pos_iff_degree_pos.2 hdeg) hn
+
+lemma monic_geom_sum_X (R : Type*) [semiring R] {n : ℕ} (hn : n ≠ 0) :
+  (geom_sum (X : R[X]) n).monic :=
+begin
+  nontriviality R,
+  apply monic_X.geom_sum _ hn,
+  simpa only [nat_degree_X] using zero_lt_one
+end
+
 section to_subring
 
 variables (p : R[X]) (T : subring R)

src/ring_theory/polynomial/eisenstein.lean

@@ -7,6 +7,7 @@ Authors: Riccardo Brasca
 import ring_theory.eisenstein_criterion
 import ring_theory.integrally_closed
 import ring_theory.norm
+import ring_theory.polynomial.cyclotomic.basic
 
 /-!
 # Eisenstein polynomials
@@ -194,6 +195,55 @@ end is_eisenstein_at
 
 end polynomial
 
+section cyclotomic
+
+variables {p : ℕ}
+
+local notation `𝓟` := submodule.span ℤ {p}
+
+open polynomial
+
+lemma cyclotomic_comp_X_add_one_is_eisenstein_at [hp : fact p.prime] :
+  ((cyclotomic p ℤ).comp (X + 1)).is_eisenstein_at 𝓟 :=
+{ leading :=
+  begin
+    intro h,
+    rw [show (X + 1 : ℤ[X]) = X + C 1, by simp] at h,
+    suffices : ((cyclotomic p ℤ).comp (X + C 1)).monic,
+    { rw [monic.def.1 this, ideal.submodule_span_eq, ideal.mem_span_singleton] at h,
+      exact nat.prime.not_dvd_one hp.out (by exact_mod_cast h) },
+    refine monic.comp (cyclotomic.monic p ℤ) (monic_X_add_C 1) (λ h₁, _),
+    rw [nat_degree_X_add_C] at h₁,
+    exact zero_ne_one h₁.symm,
+  end,
+  mem := λ i hi,
+  begin
+    rw [cyclotomic_eq_geom_sum hp.out, geom_sum_X_comp_X_add_one_eq_sum, ← lcoeff_apply,
+      linear_map.map_sum],
+    conv { congr, congr, skip, funext,
+      rw [lcoeff_apply, ← C_eq_nat_cast, ← monomial_eq_C_mul_X, coeff_monomial] },
+    rw [nat_degree_comp, show (X + 1 : ℤ[X]) = X + C 1, by simp, nat_degree_X_add_C, mul_one,
+      nat_degree_cyclotomic, nat.totient_prime hp.out] at hi,
+    simp only [lt_of_lt_of_le hi (nat.sub_le _ _), int.nat_cast_eq_coe_nat, sum_ite_eq', mem_range,
+      if_true, ideal.submodule_span_eq, ideal.mem_span_singleton],
+    exact int.coe_nat_dvd.2
+      (nat.prime.dvd_choose_self (nat.succ_pos i) (lt_tsub_iff_right.1 hi) hp.out)
+  end,
+  not_mem :=
+  begin
+    rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_eq_geom_sum hp.out, eval_add, eval_X,
+      eval_one, zero_add, eval_geom_sum, one_geom_sum, int.nat_cast_eq_coe_nat,
+      ideal.submodule_span_eq, ideal.span_singleton_pow, ideal.mem_span_singleton],
+    intro h,
+    obtain ⟨k, hk⟩ := int.coe_nat_dvd.1 h,
+    rw [← mul_assoc, mul_one, mul_assoc] at hk,
+    nth_rewrite 0 [← nat.mul_one p] at hk,
+    rw [nat.mul_right_inj hp.out.pos] at hk,
+    exact nat.prime.not_dvd_one hp.out (dvd.intro k (hk.symm)),
+  end }
+
+end cyclotomic
+
 section is_integral
 
 variables {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L]
@@ -350,12 +400,12 @@ begin
     have H := degree_mod_by_monic_lt Q₁ (minpoly.monic hBint),
     rw [← hQ₁, ← hP] at H,
     replace H:= nat.lt_iff_add_one_le.1 (lt_of_lt_of_le (lt_of_le_of_lt
-      (nat.lt_iff_add_one_le.1 (lt_of_succ_lt_succ (mem_range.1 hj))) (lt_succ_self _))
+      (nat.lt_iff_add_one_le.1 (nat.lt_of_succ_lt_succ (mem_range.1 hj))) (lt_succ_self _))
       (nat.lt_iff_add_one_le.1 (((nat_degree_lt_nat_degree_iff hQzero).2 H)))),
     rw [add_assoc] at H,
     have Hj : Q.nat_degree + 1 = j + 1 + (Q.nat_degree - j),
     { rw [← add_comm 1, ← add_comm 1, add_assoc, add_right_inj, ← nat.add_sub_assoc
-        (lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm, nat.add_sub_cancel] },
+        (nat.lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm, nat.add_sub_cancel] },
 
     -- By induction hypothesis we can find `g : ℕ → R` such that
     -- `k ∈ range (j + 1) → Q.coeff k • B.gen ^ k = (algebra_map R L) p * g k • B.gen ^ k`-
@@ -408,7 +458,7 @@ begin
   -- we didn't know were multiples of `p`, and we take the norm on both sides.
   replace hQ := congr_arg (λ x, x * B.gen ^ (P.nat_degree - (j + 2))) hQ,
   simp_rw [sum_map, add_left_embedding_apply, add_mul, sum_mul, mul_assoc] at hQ,
-  rw [← insert_erase (mem_range.2 (tsub_pos_iff_lt.2 $ lt_of_succ_lt_succ $ mem_range.1 hj)),
+  rw [← insert_erase (mem_range.2 (tsub_pos_iff_lt.2 $ nat.lt_of_succ_lt_succ $ mem_range.1 hj)),
       sum_insert (not_mem_erase 0 _), add_zero, sum_congr rfl hf₁, ← mul_sum, ← mul_sum,
       add_assoc, ← mul_add, smul_mul_assoc, ← pow_add, smul_def] at hQ,
   replace hQ := congr_arg (norm K) (eq_sub_of_add_eq hQ),