feat(ring_theory/polynomial/cyclotomic): add order_of_root_cyclotomic (…

…#5151)

Two lemmas about roots of cyclotomic polynomials modulo `p`.

`order_of_root_cyclotomic` is the main algebraic tool to prove the existence of infinitely many primes congruent to `1` modulo `n`.


Co-authored-by: Johan Commelin <johan@commelin.net>

src/number_theory/divisors.lean

@@ -126,6 +126,19 @@ begin
   exact nat.le_of_dvd (nat.succ_pos m),
 end
 
+lemma divisors_subset_of_dvd {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) : divisors m ⊆ divisors n :=
+finset.subset_iff.2 $ λ x hx, nat.mem_divisors.mpr (⟨dvd.trans (nat.mem_divisors.mp hx).1 h, hzero⟩)
+
+lemma divisors_subset_proper_divisors {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
+  divisors m ⊆ proper_divisors n :=
+begin
+  apply finset.subset_iff.2,
+  intros x hx,
+  exact nat.mem_proper_divisors.2 (⟨dvd.trans (nat.mem_divisors.1 hx).1 h,
+    lt_of_le_of_lt (divisor_le hx) (lt_of_le_of_ne (divisor_le (nat.mem_divisors.2
+    ⟨h, hzero⟩)) hdiff)⟩)
+end
+
 @[simp]
 lemma divisors_zero : divisors 0 = ∅ := by { ext, simp }
 

src/ring_theory/polynomial/cyclotomic.lean

@@ -10,6 +10,7 @@ import algebra.polynomial.big_operators
 import number_theory.arithmetic_function
 import data.polynomial.lifts
 import analysis.complex.roots_of_unity
+import field_theory.separable
 
 /-!
 # Cyclotomic polynomials.
@@ -455,6 +456,20 @@ begin
   exact monic.ne_zero prod_monic (degree_eq_bot.1 h)
 end
 
+/-- If `m` is a proper divisor of `n`, then `X ^ m - 1` divides
+`∏ i in nat.proper_divisors n, cyclotomic i R`. -/
+lemma X_pow_sub_one_dvd_prod_cyclotomic (R : Type*) [comm_ring R] {n m : ℕ} (hpos : 0 < n)
+  (hm : m ∣ n) (hdiff : m ≠ n) : X ^ m - 1 ∣ ∏ i in nat.proper_divisors n, cyclotomic i R :=
+begin
+  replace hm := nat.mem_proper_divisors.2 ⟨hm, lt_of_le_of_ne (nat.divisor_le (nat.mem_divisors.2
+    ⟨hm, (ne_of_lt hpos).symm⟩)) hdiff⟩,
+  rw [← finset.sdiff_union_of_subset (nat.divisors_subset_proper_divisors (ne_of_lt hpos).symm
+    (nat.mem_proper_divisors.1 hm).1 (ne_of_lt (nat.mem_proper_divisors.1 hm).2)),
+    finset.prod_union finset.sdiff_disjoint, prod_cyclotomic_eq_X_pow_sub_one
+    (nat.pos_of_mem_proper_divisors hm)],
+  exact ⟨(∏ (x : ℕ) in n.proper_divisors \ m.divisors, cyclotomic x R), by rw mul_comm⟩
+end
+
 /-- If there is a primitive `n`-th root of unity in `K`, then
 `cyclotomic n K = ∏ μ in primitive_roots n R, (X - C μ)`. In particular,
 `cyclotomic n K = cyclotomic' n K` -/
@@ -510,7 +525,7 @@ begin
 end
 
 /-- The constant term of `cyclotomic n R` is `1` if `2 ≤ n`. -/
-lemma cyclotomic_coeff_zero {R : Type*} [comm_ring R] (n : ℕ) (hn : 2 ≤ n) :
+lemma cyclotomic_coeff_zero (R : Type*) [comm_ring R] {n : ℕ} (hn : 2 ≤ n) :
   (cyclotomic n R).coeff 0 = 1 :=
 begin
   induction n using nat.strong_induction_on with n hi,
@@ -543,6 +558,87 @@ begin
   exact neg_inj.mp (eq.symm heq)
 end
 
+/-- If `(a : ℕ)` is a root of `cyclotomic n (zmod p)`, where `p` is a prime, then `a` and `p` are
+coprime. -/
+lemma coprime_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : fact p.prime] {a : ℕ}
+  (hroot : is_root (cyclotomic n (zmod p)) (nat.cast_ring_hom (zmod p) a)) :
+  a.coprime p :=
+begin
+  apply nat.coprime.symm,
+  rw [nat.prime.coprime_iff_not_dvd hprime],
+  by_contra h,
+  replace h := (zmod.nat_coe_zmod_eq_zero_iff_dvd a p).2 h,
+  rw [is_root.def, ring_hom.eq_nat_cast, h, ← coeff_zero_eq_eval_zero] at hroot,
+  by_cases hone : n = 1,
+  { simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero,
+    one_ne_zero, coeff_sub] at hroot,
+    exact hroot },
+  rw [cyclotomic_coeff_zero (zmod p) (nat.succ_le_of_lt (lt_of_le_of_ne
+    (nat.succ_le_of_lt hpos) (ne.symm hone)))] at hroot,
+  exact one_ne_zero hroot
+end
+
 end cyclotomic
 
+section order
+
+/-- If `(a : ℕ)` is a root of `cyclotomic n (zmod p)`, then the multiplicative order of `a` modulo
+`p` divides `n`. -/
+lemma order_of_root_cyclotomic_dvd {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : fact p.prime]
+  {a : ℕ} (hroot : is_root (cyclotomic n (zmod p)) (nat.cast_ring_hom (zmod p) a)) :
+  order_of (zmod.unit_of_coprime a (coprime_of_root_cyclotomic hpos hroot)) ∣ n :=
+begin
+  apply order_of_dvd_of_pow_eq_one,
+  suffices hpow : eval (nat.cast_ring_hom (zmod p) a) (X ^ n - 1 : polynomial (zmod p)) = 0,
+  { simp only [eval_X, eval_one, eval_pow, eval_sub, ring_hom.eq_nat_cast] at hpow,
+    apply units.coe_eq_one.1,
+    simp only [sub_eq_zero.mp hpow, zmod.cast_unit_of_coprime, units.coe_pow] },
+  rw [is_root.def] at hroot,
+  rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (zmod p),
+    nat.divisors_eq_proper_divisors_insert_self_of_pos hpos,
+    finset.prod_insert nat.proper_divisors.not_self_mem, eval_mul, hroot, zero_mul]
+end
+
+/-- If `(a : ℕ)` is a root of `cyclotomic n (zmod p)`, where `p` is a prime that does not divide
+`n`, then the multiplicative order of `a` modulo `p` is exactly `n`. -/
+lemma order_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : fact p.prime] {a : ℕ}
+  (hn : ¬ p ∣ n) (hroot : is_root (cyclotomic n (zmod p)) (nat.cast_ring_hom (zmod p) a)) :
+  order_of (zmod.unit_of_coprime a (coprime_of_root_cyclotomic hpos hroot)) = n :=
+begin
+  set m := order_of (zmod.unit_of_coprime a (coprime_of_root_cyclotomic hpos hroot)),
+  have ha := coprime_of_root_cyclotomic hpos hroot,
+  have hdivcycl : map (int.cast_ring_hom (zmod p)) (X - a) ∣ (cyclotomic n (zmod p)),
+  { replace hrootdiv := dvd_iff_is_root.2 hroot,
+    simp only [C_eq_nat_cast, ring_hom.eq_nat_cast] at hrootdiv,
+    simp only [hrootdiv, map_nat_cast, map_X, map_sub] },
+  by_contra hdiff,
+  have hdiv : map (int.cast_ring_hom (zmod p)) (X - a) ∣
+    ∏ i in nat.proper_divisors n, cyclotomic i (zmod p),
+  { suffices hdivm : map (int.cast_ring_hom (zmod p)) (X - a) ∣ X ^ m - 1,
+    { exact dvd_trans hdivm (X_pow_sub_one_dvd_prod_cyclotomic (zmod p) hpos
+        (order_of_root_cyclotomic_dvd hpos hroot) hdiff) },
+    rw [map_sub, map_X, map_nat_cast, ← C_eq_nat_cast, dvd_iff_is_root, is_root.def, eval_sub,
+      eval_pow, eval_one, eval_X, sub_eq_zero, ← zmod.cast_unit_of_coprime a ha, ← units.coe_pow,
+      units.coe_eq_one],
+    exact pow_order_of_eq_one (zmod.unit_of_coprime a ha) },
+  have habs : (map (int.cast_ring_hom (zmod p)) (X - a)) ^ 2 ∣ X ^ n - 1,
+  { obtain ⟨P, hP⟩ := hdivcycl,
+    obtain ⟨Q, hQ⟩ := hdiv,
+    rw [← prod_cyclotomic_eq_X_pow_sub_one hpos, nat.divisors_eq_proper_divisors_insert_self_of_pos
+      hpos, finset.prod_insert nat.proper_divisors.not_self_mem, hP, hQ],
+    exact ⟨P * Q, by ring⟩ },
+  have hnzero : ↑n ≠ (0 : (zmod p)),
+  { intro ha,
+    exact hn (int.coe_nat_dvd.1 ((zmod.int_coe_zmod_eq_zero_iff_dvd n p).1 ha)) },
+  rw [pow_two] at habs,
+  replace habs := squarefree_X_pow_sub_C (1 : (zmod p)) hnzero one_ne_zero
+    (map (int.cast_ring_hom (zmod p)) (X - a)) habs,
+  simp only [map_nat_cast, map_X, map_sub] at habs,
+  replace habs := degree_eq_zero_of_is_unit habs,
+  rw [← C_eq_nat_cast, degree_X_sub_C] at habs,
+  norm_cast at habs
+end
+
+end order
+
 end polynomial