feat(number_theory/cyclotomic/basic): add cyclotomic_field and cyclot…

…omic_ring (#11383)

We add `cyclotomic_field` and `cyclotomic_ring`, that provide an explicit cyclotomic extension of a given field/ring.

From flt-regular

src/number_theory/cyclotomic/basic.lean

@@ -18,11 +18,18 @@ primitive roots of unity, for all `n ∈ S`.
 ## Main definition
 
 * `is_cyclotomic_extension S A B` : means that `B` is obtained from `A` by adding `n`-th primitive
-roots of unity, for all `n ∈ S`.
+  roots of unity, for all `n ∈ S`.
+* `cyclotomic_field`: given `n : ℕ+` and a field `K`, we define `cyclotomic n K` as the splitting
+  field of `cyclotomic n K`. If `n` is nonzero in `K`, it has the instance
+  `is_cyclotomic_extension {n} K (cyclotomic_field n K)`.
+* `cyclotomic_ring` : if `A` is a domain with fraction field `K` and `n : ℕ+`, we define
+  `cyclotomic_ring n A K` as the `A`-subalgebra of `cyclotomic_field n K` generated by the roots of
+  `X ^ n - 1`. If `n` is nonzero in `A`, it has the instance
+  `is_cyclotomic_extension {n} A (cyclotomic_ring n A K)`.
 
 ## Main results
 
-* `is_cyclotomic_extension.trans`: if `is_cyclotomic_extension S A B` and
+* `is_cyclotomic_extension.trans` : if `is_cyclotomic_extension S A B` and
   `is_cyclotomic_extension T B C`, then `is_cyclotomic_extension (S ∪ T) A C`.
 * `is_cyclotomic_extension.union_right` : given `is_cyclotomic_extension (S ∪ T) A B`, then
   `is_cyclotomic_extension T (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }) B`.
@@ -43,8 +50,9 @@ Our definition of `is_cyclotomic_extension` is very general, to allow rings of a
 and infinite extensions, but it will mainly be used in the case `S = {n}` with `(n : A) ≠ 0` (and
 for integral domains).
 All results are in the `is_cyclotomic_extension` namespace.
-Note that some results, `is_cyclotomic_extension.trans`, `is_cyclotomic_extension.finite`,
-`is_cyclotomic_extension.number_field` and `is_cyclotomic_extension.finite_dimensional` are lemmas,
+Note that some results, for example `is_cyclotomic_extension.trans`,
+`is_cyclotomic_extension.finite`, `is_cyclotomic_extension.number_field`,
+`is_cyclotomic_extension.finite_dimensional` and `cyclotomic_field.algebra_base` are lemmas,
 but they can be made local instances.
 
 -/
@@ -310,3 +318,124 @@ end singleton
 end field
 
 end is_cyclotomic_extension
+
+section cyclotomic_field
+
+/-- Given `n : ℕ+` and a field `K`, we define `cyclotomic n K` as the splitting field of
+`cyclotomic n K`. If `ne_zero ((n : ℕ) : K)`, it has the instance
+`is_cyclotomic_extension {n} K (cyclotomic_field n K)`. -/
+@[derive [field, algebra K, inhabited]]
+def cyclotomic_field : Type w := (cyclotomic n K).splitting_field
+
+namespace cyclotomic_field
+
+instance is_cyclotomic_extension [ne_zero ((n : ℕ) : K)] :
+  is_cyclotomic_extension {n} K (cyclotomic_field n K) :=
+{ exists_root := λ a han,
+  begin
+    rw mem_singleton_iff at han,
+    subst a,
+    exact exists_root_of_splits _ (splitting_field.splits _) (degree_cyclotomic_pos n K (n.pos)).ne'
+  end,
+  adjoin_roots :=
+  begin
+    rw [←algebra.eq_top_iff, ←splitting_field.adjoin_roots, eq_comm],
+    letI := classical.dec_eq (cyclotomic_field n K),
+    obtain ⟨ζ, hζ⟩ := exists_root_of_splits _ (splitting_field.splits (cyclotomic n K))
+      (degree_cyclotomic_pos n _ n.pos).ne',
+    haveI : ne_zero ((n : ℕ) : (cyclotomic_field n K)) :=
+      ne_zero.nat_of_injective (algebra_map K _).injective,
+    rw [eval₂_eq_eval_map, map_cyclotomic, ← is_root.def, is_root_cyclotomic_iff] at hζ,
+    exact is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots n hζ,
+  end }
+
+end cyclotomic_field
+
+end cyclotomic_field
+
+section is_domain
+
+variables [is_domain A] [algebra A K] [is_fraction_ring A K]
+
+section cyclotomic_ring
+
+/-- If `K` is the fraction field of `A`, the `A`-algebra structure on `cyclotomic_field n K`.
+This is not an instance since it causes diamonds when `A = ℤ`. -/
+@[nolint unused_arguments]
+def cyclotomic_field.algebra_base : algebra A (cyclotomic_field n K) :=
+((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra
+
+local attribute [instance] cyclotomic_field.algebra_base
+
+instance cyclotomic_field.no_zero_smul_divisors : no_zero_smul_divisors A (cyclotomic_field n K) :=
+no_zero_smul_divisors.of_algebra_map_injective $ function.injective.comp
+(no_zero_smul_divisors.algebra_map_injective _ _) $ is_fraction_ring.injective A K
+
+/-- If `A` is a domain with fraction field `K` and `n : ℕ+`, we define `cyclotomic_ring n A K` as
+the `A`-subalgebra of `cyclotomic_field n K` generated by the roots of `X ^ n - 1`. If
+`ne_zero ((n : ℕ) : A)`, it has the instance
+`is_cyclotomic_extension {n} A (cyclotomic_ring n A K)`. -/
+@[derive [comm_ring, is_domain, inhabited]]
+def cyclotomic_ring : Type w := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }
+
+namespace cyclotomic_ring
+
+/-- The `A`-algebra structure on `cyclotomic_ring n A K`.
+This is not an instance since it causes diamonds when `A = ℤ`. -/
+def algebra_base : algebra A (cyclotomic_ring n A K) := (adjoin A _).algebra
+
+local attribute [instance] cyclotomic_ring.algebra_base
+
+instance : no_zero_smul_divisors A (cyclotomic_ring n A K) := (adjoin A _).no_zero_smul_divisors_bot
+
+lemma algebra_base_injective : function.injective $ algebra_map A (cyclotomic_ring n A K) :=
+no_zero_smul_divisors.algebra_map_injective _ _
+
+instance : algebra (cyclotomic_ring n A K) (cyclotomic_field n K) :=
+(adjoin A _).to_algebra
+
+lemma adjoin_algebra_injective :
+  function.injective $ algebra_map (cyclotomic_ring n A K) (cyclotomic_field n K) :=
+subtype.val_injective
+
+instance : no_zero_smul_divisors (cyclotomic_ring n A K) (cyclotomic_field n K) :=
+no_zero_smul_divisors.of_algebra_map_injective (adjoin_algebra_injective n A K)
+
+instance : is_scalar_tower A (cyclotomic_ring n A K) (cyclotomic_field n K) :=
+is_scalar_tower.subalgebra' _ _ _ _
+
+instance is_cyclotomic_extension [ne_zero ((n : ℕ) : A)] :
+  is_cyclotomic_extension {n} A (cyclotomic_ring n A K) :=
+{ exists_root := λ a han,
+  begin
+    rw mem_singleton_iff at han,
+    subst a,
+    haveI : ne_zero ((n : ℕ) : K) := ne_zero.of_no_zero_smul_divisors A K,
+    haveI : ne_zero ((n : ℕ) : cyclotomic_ring n A K) := ne_zero.of_no_zero_smul_divisors A _,
+    haveI : ne_zero ((n : ℕ) : cyclotomic_field n K) := ne_zero.of_no_zero_smul_divisors A _,
+    obtain ⟨μ, hμ⟩ := let h := (cyclotomic_field.is_cyclotomic_extension n K).exists_root
+                      in h $ mem_singleton n,
+    refine ⟨⟨μ, subset_adjoin _⟩, _⟩,
+    { apply (is_root_of_unity_iff n.pos (cyclotomic_field n K)).mpr,
+      refine ⟨n, nat.mem_divisors_self _ n.ne_zero, _⟩,
+      rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic] at hμ },
+    simp_rw [aeval_def, eval₂_eq_eval_map,
+      map_cyclotomic, ←is_root.def, is_root_cyclotomic_iff] at hμ ⊢,
+    rwa ←is_primitive_root.map_iff_of_injective (adjoin_algebra_injective n A K)
+  end,
+  adjoin_roots := λ x,
+  begin
+    refine adjoin_induction' (λ y hy, _) (λ a, _) (λ y z hy hz, _) (λ y z hy hz, _) x,
+    { refine subset_adjoin _,
+      simp only [mem_singleton_iff, exists_eq_left, mem_set_of_eq],
+      rwa [← subalgebra.coe_eq_one, subalgebra.coe_pow, subtype.coe_mk] },
+    { exact subalgebra.algebra_map_mem _ a },
+    { exact subalgebra.add_mem _ hy hz },
+    { exact subalgebra.mul_mem _ hy hz },
+  end }
+
+end cyclotomic_ring
+
+end cyclotomic_ring
+
+end is_domain

src/ring_theory/localization.lean

@@ -2107,6 +2107,9 @@ lemma coe_submodule_strict_mono :
   strict_mono (coe_submodule K : ideal R → submodule R K) :=
 strict_mono_of_le_iff_le (λ _ _, coe_submodule_le_coe_submodule.symm)
 
+@[priority 100] instance [no_zero_divisors K] : no_zero_smul_divisors R K :=
+no_zero_smul_divisors.of_algebra_map_injective $ is_fraction_ring.injective R K
+
 variables (R K)
 
 lemma coe_submodule_injective :