feat(number_theory/cyclotomic): alg-closed fields are cyclotomic exte…

…nsions over themselves (#13366)




Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

archive/100-theorems-list/37_solution_of_cubic.lean

@@ -46,7 +46,7 @@ variables {ω p q r s t : K}
 
 lemma cube_root_of_unity_sum (hω : is_primitive_root ω 3) : 1 + ω + ω^2 = 0 :=
 begin
-  convert is_root_cyclotomic (nat.succ_pos _) hω,
+  convert hω.is_root_cyclotomic (nat.succ_pos _),
   rw [cyclotomic_eq_geom_sum nat.prime_three, eval_geom_sum],
   simp only [geom_sum_succ, geom_sum_zero],
   ring,

src/number_theory/cyclotomic/basic.lean

@@ -8,6 +8,7 @@ import ring_theory.polynomial.cyclotomic.basic
 import number_theory.number_field
 import algebra.char_p.algebra
 import field_theory.galois
+import analysis.complex.polynomial
 
 /-!
 # Cyclotomic extensions
@@ -254,7 +255,7 @@ begin
     obtain ⟨i, hin, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos,
     refine set_like.mem_coe.2 (subalgebra.pow_mem _ (subset_adjoin _) _),
     rwa [finset.mem_coe, multiset.mem_to_finset, mem_roots $ cyclotomic_ne_zero n B],
-    exact is_root_cyclotomic n.pos hζ }
+    exact hζ.is_root_cyclotomic n.pos }
 end
 
 lemma adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic [decidable_eq B] [is_domain B]
@@ -271,7 +272,7 @@ begin
          map_cyclotomic, mem_roots $ cyclotomic_ne_zero n B] at hx },
   { simp only [mem_singleton_iff, exists_eq_left, mem_set_of_eq] at hx,
     simpa only [hx, multiset.mem_to_finset, finset.mem_coe, map_cyclotomic,
-                mem_roots (cyclotomic_ne_zero n B)] using is_root_cyclotomic n.pos hζ }
+                mem_roots (cyclotomic_ne_zero n B)] using hζ.is_root_cyclotomic n.pos }
 end
 
 lemma adjoin_primitive_root_eq_top [is_domain B] [h : is_cyclotomic_extension {n} A B]
@@ -291,8 +292,8 @@ lemma _root_.is_primitive_root.adjoin_is_cyclotomic_extension [is_domain B] {ζ
   begin
     rw [set.mem_singleton_iff] at hi,
     refine ⟨⟨ζ, subset_adjoin $ set.mem_singleton ζ⟩, _⟩,
-    have := is_root_cyclotomic n.pos h,
-    rw [is_root.def, ← map_cyclotomic _ (algebra_map A B), eval_map, ← aeval_def, ← hi] at this,
+    replace h := h.is_root_cyclotomic n.pos,
+    rw [is_root.def, ← map_cyclotomic _ (algebra_map A B), eval_map, ← aeval_def, ← hi] at h,
     rwa [← subalgebra.coe_eq_zero, aeval_subalgebra_coe, subtype.coe_mk]
   end,
   adjoin_roots := λ x,
@@ -557,3 +558,11 @@ end cyclotomic_ring
 end cyclotomic_ring
 
 end is_domain
+
+/-- Algebraically closed fields are cyclotomic extensions over themselves. -/
+lemma is_alg_closed.is_cyclotomic_extension (K) [field K] [is_alg_closed K] (S) :
+  is_cyclotomic_extension S K K :=
+⟨λ a _, is_alg_closed.exists_aeval_eq_zero _ _ (degree_cyclotomic_pos _ _ a.pos).ne',
+ algebra.eq_top_iff.mp $ subsingleton.elim _ _ ⟩
+
+instance : ∀ S, is_cyclotomic_extension S ℂ ℂ := is_alg_closed.is_cyclotomic_extension ℂ

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -568,8 +568,8 @@ section roots
 variables {R : Type*} {n : ℕ} [comm_ring R] [is_domain R]
 
 /-- Any `n`-th primitive root of unity is a root of `cyclotomic n K`.-/
-lemma is_root_cyclotomic (hpos : 0 < n) {μ : R} (h : is_primitive_root μ n) :
-  is_root (cyclotomic n R) μ :=
+lemma _root_.is_primitive_root.is_root_cyclotomic (hpos : 0 < n) {μ : R}
+  (h : is_primitive_root μ n) : is_root (cyclotomic n R) μ :=
 begin
   rw [← mem_roots (cyclotomic_ne_zero n R),
       cyclotomic_eq_prod_X_sub_primitive_roots h, roots_prod_X_sub_C, ← finset.mem_def],
@@ -581,7 +581,7 @@ private lemma is_root_cyclotomic_iff' {n : ℕ} {K : Type*} [field K] {μ : K} [
 begin
   -- in this proof, `o` stands for `order_of μ`
   have hnpos : 0 < n := (ne_zero.of_ne_zero_coe K).out.bot_lt,
-  refine ⟨λ hμ, _, is_root_cyclotomic hnpos⟩,
+  refine ⟨λ hμ, _, is_primitive_root.is_root_cyclotomic hnpos⟩,
   have hμn : μ ^ n = 1,
   { rw is_root_of_unity_iff hnpos,
     exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩ },