feat(number_theory/cyclotomic/zeta): add lemmas (#11753)

Various lemmas about `zeta`.

From flt-regular.



Co-authored-by: Eric <ericrboidi@gmail.com>

src/number_theory/cyclotomic/basic.lean

@@ -7,6 +7,7 @@ Authors: Riccardo Brasca
 import ring_theory.polynomial.cyclotomic.basic
 import number_theory.number_field
 import algebra.char_p.algebra
+import field_theory.galois
 
 /-!
 # Cyclotomic extensions
@@ -52,8 +53,8 @@ for integral domains).
 All results are in the `is_cyclotomic_extension` namespace.
 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.
+`is_cyclotomic_extension.finite_dimensional`, `is_cyclotomic_extension.is_galois` and
+`cyclotomic_field.algebra_base` are lemmas, but they can be made local instances.
 
 -/
 
@@ -222,9 +223,9 @@ lemma integral [is_domain B] [is_noetherian_ring A] [fintype S] [is_cyclotomic_e
 is_integral_of_noetherian $ is_noetherian_of_fg_of_noetherian' $ (finite S A B).out
 
 /-- If `S` is finite and `is_cyclotomic_extension S K A`, then `finite_dimensional K A`. -/
-lemma finite_dimensional [fintype S] [algebra K A] [is_domain A] [is_cyclotomic_extension S K A] :
-  finite_dimensional K A :=
-finite S K A
+lemma finite_dimensional (C : Type z) [fintype S] [comm_ring C] [algebra K C] [is_domain C]
+  [is_cyclotomic_extension S K C] : finite_dimensional K C :=
+finite S K C
 
 end fintype
 
@@ -324,6 +325,15 @@ lemma splitting_field_X_pow_sub_one : is_splitting_field K L (X ^ (n : ℕ) - 1)
       n.pos _), is_root.def, eval_sub, eval_pow, eval_C, eval_X, sub_eq_zero]
   end }
 
+include n
+
+lemma is_galois : is_galois K L :=
+begin
+  letI := splitting_field_X_pow_sub_one n K L,
+  exact is_galois.of_separable_splitting_field (X_pow_sub_one_separable_iff.2
+    (ne_zero.ne _ : ((n : ℕ) : K) ≠ 0)),
+end
+
 /-- If `is_cyclotomic_extension {n} K L` and `ne_zero (n : K)`, then `L` is the splitting
 field of `cyclotomic n K`. -/
 lemma splitting_field_cyclotomic : is_splitting_field K L (cyclotomic n K) :=

src/number_theory/cyclotomic/zeta.lean

@@ -6,6 +6,7 @@ Authors: Alex Best, Riccardo Brasca, Eric Rodriguez
 
 import number_theory.cyclotomic.basic
 import ring_theory.adjoin.power_basis
+import ring_theory.norm
 
 /-!
 # `ζ` elements in cyclotmic fields
@@ -16,25 +17,29 @@ assumptions) a primitive `n`-root of unity in `B` and we study its properties.
 * `is_cyclotomic_extension.zeta n A B` : if `is_cyclotomic_extension {n} A B`, than `zeta n A B`
   is an element of `B` that plays the role of a primitive `n`-th root of unity.
 * `is_cyclotomic_extension.zeta.power_basis` : if `K` and `L` are fields such that
-  `is_cyclotomic_extension {n} K L` and `ne_zero ((n : ℕ) : K)`, then `zeta.power_basis` is the
+  `is_cyclotomic_extension {n} K L` and `ne_zero (n : K)`, then `zeta.power_basis` is the
   power basis given by `zeta n K L`.
 * `is_cyclotomic_extension.zeta.embeddings_equiv_primitive_roots` : the equiv between `L →ₐ[K] A`
   and `primitive_roots n A` given by the choice of `zeta`.
 
 ## Main results
-* `is_cyclotomic_extension.zeta_primitive_root` : if `is_domain B` and `ne_zero ((n : ℕ) : B)` then
+* `is_cyclotomic_extension.zeta_primitive_root` : if `is_domain B` and `ne_zero (n : B)` then
   `zeta n A B` is a primitive `n`-th root of unity.
+* `is_cyclotomic_extension.finrank` : if `irreducible (cyclotomic n K)` (in particular for
+  `K = ℚ`), then the `finrank` of a cyclotomic extension is `n.totient`.
+* `is_cyclotomic_extension.norm_zeta_sub_one` : if `irreducible (cyclotomic n K)` (in particular for
+  `K = ℚ`), then the norm of `zeta n K L - 1` is `eval 1 (cyclotomic n ℤ)`.
 
 ## Implementation details
 `zeta n A B` is defined as any root of `cyclotomic n A` in `B`, that exists because of
 `is_cyclotomic_extension {n} A B`. It is not true in general that it is a primitive `n`-th root of
-unity, but this holds if `is_domain B` and `ne_zero ((n : ℕ) : B)`.
+unity, but this holds if `is_domain B` and `ne_zero (n : B)`.
 
 -/
 
 noncomputable theory
 
-open polynomial
+open polynomial algebra finset finite_dimensional
 
 universes u v w z
 
@@ -53,21 +58,25 @@ classical.some_spec (exists_root (set.mem_singleton n) : ∃ r : B, aeval r (cyc
 lemma zeta_spec' : is_root (cyclotomic n B) (zeta n A B) :=
 by { convert zeta_spec n A B, rw [is_root.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic] }
 
-/-- If `is_domain B` and `ne_zero ((n : ℕ) : B)` then `zeta n A B` is a primitive `n`-th root of
+lemma zeta_pow : (zeta n A B) ^ (n : ℕ) = 1 :=
+is_root_of_unity_of_root_cyclotomic (nat.mem_divisors_self _ n.pos.ne') (zeta_spec' _ _ _)
+
+/-- If `is_domain B` and `ne_zero (n : B)` then `zeta n A B` is a primitive `n`-th root of
 unity. -/
-lemma zeta_primitive_root [is_domain B] [ne_zero ((n : ℕ) : B)] :
+lemma zeta_primitive_root [is_domain B] [ne_zero (n : B)] :
   is_primitive_root (zeta n A B) n :=
 by { rw ←is_root_cyclotomic_iff, exact zeta_spec' n A B }
 
 section field
 
-variables {K : Type u} (L : Type v) [field K] [field L] [algebra K L] [algebra K A]
-variables [is_cyclotomic_extension {n} K L] [ne_zero ((n : ℕ) : K)]
+variables {K : Type u} (L : Type v) (C : Type w)
+variables [field K] [field L] [comm_ring C] [algebra K L] [algebra K C]
+variables [is_cyclotomic_extension {n} K L] [ne_zero (n : K)]
 
 /-- If `irreducible (cyclotomic n K)`, then the minimal polynomial of `zeta n K A` is
 `cyclotomic n K`. -/
-lemma zeta_minpoly {n : ℕ+} (hirr : irreducible (cyclotomic n K)) [is_cyclotomic_extension {n} K A]
-  [nontrivial A] : minpoly K (zeta n K A) = cyclotomic n K :=
+lemma zeta_minpoly {n : ℕ+} (hirr : irreducible (cyclotomic n K)) [is_cyclotomic_extension {n} K C]
+  [nontrivial C] : minpoly K (zeta n K C) = cyclotomic n K :=
 (minpoly.eq_of_irreducible_of_monic hirr (zeta_spec _ _ _) (cyclotomic.monic n K)).symm
 
 include n
@@ -78,11 +87,10 @@ variable (K)
 @[simps] def zeta.power_basis : power_basis K L :=
 begin
   haveI := (ne_zero.of_no_zero_smul_divisors K L n).trans,
-  refine power_basis.map
-    (algebra.adjoin.power_basis $ integral {n} K L $ zeta n K L) _,
+  refine power_basis.map (adjoin.power_basis $ integral {n} K L $ zeta n K L) _,
   exact (subalgebra.equiv_of_eq _ _
       (is_cyclotomic_extension.adjoin_primitive_root_eq_top n _ $ zeta_primitive_root n K L)).trans
-      algebra.top_equiv
+      top_equiv
 end
 
 variables {K} {n}
@@ -94,26 +102,32 @@ begin
   exact zeta_minpoly L hirr
 end
 
-variables (K) (n)
+/-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the `finrank` of a
+cyclotomic extension is `n.totient`. -/
+lemma finrank (hirr : irreducible (cyclotomic n K)) : finrank K L = (n : ℕ).totient :=
+begin
+  rw [power_basis.finrank (zeta.power_basis n K L), zeta.power_basis_dim, ← zeta.power_basis_gen,
+    zeta.power_basis_gen_minpoly L hirr, nat_degree_cyclotomic]
+end
 
 /-- `zeta.embeddings_equiv_primitive_roots` is the equiv between `L →ₐ[K] A` and
   `primitive_roots n A` given by the choice of `zeta`. -/
 @[simps]
-def zeta.embeddings_equiv_primitive_roots [is_domain A] (hirr : irreducible (cyclotomic n K)) :
-  (L →ₐ[K] A) ≃ primitive_roots n A :=
+def zeta.embeddings_equiv_primitive_roots [is_domain C] (hirr : irreducible (cyclotomic n K)) :
+  (L →ₐ[K] C) ≃ primitive_roots n C :=
 ((zeta.power_basis n K L).lift_equiv).trans
 { to_fun    := λ x,
   begin
-    haveI hn := (ne_zero.of_no_zero_smul_divisors K A n).trans,
+    haveI hn := (ne_zero.of_no_zero_smul_divisors K C n).trans,
     refine ⟨x.1, _⟩,
     cases x,
     rwa [mem_primitive_roots n.pos, ←is_root_cyclotomic_iff, is_root.def,
-      ← map_cyclotomic _ (algebra_map K A), ← zeta.power_basis_gen_minpoly L hirr,
+      ← map_cyclotomic _ (algebra_map K C), ← zeta.power_basis_gen_minpoly L hirr,
       ← eval₂_eq_eval_map, ← aeval_def]
   end,
   inv_fun   := λ x,
   begin
-    haveI hn := (ne_zero.of_no_zero_smul_divisors K A n).trans,
+    haveI hn := (ne_zero.of_no_zero_smul_divisors K C n).trans,
     refine ⟨x.1, _⟩,
     cases x,
     rwa [aeval_def, eval₂_eq_eval_map, zeta.power_basis_gen_minpoly L hirr, map_cyclotomic,
@@ -122,6 +136,45 @@ def zeta.embeddings_equiv_primitive_roots [is_domain A] (hirr : irreducible (cyc
   left_inv  := λ x, subtype.ext rfl,
   right_inv := λ x, subtype.ext rfl }
 
+variables (K) (n)
+
+/-- If `K` is linearly ordered (in particular for `K = ℚ`), the norm of `zeta n K L` is `1`
+if `n` is odd. -/
+lemma norm_zeta_eq_one (K : Type u) [linear_ordered_field K] (L : Type v) [field L] [algebra K L]
+  [is_cyclotomic_extension {n} K L] (hodd : odd (n : ℕ)) : norm K (zeta n K L) = 1 :=
+begin
+  haveI := (ne_zero.of_no_zero_smul_divisors K L n).trans,
+  have hz := congr_arg (norm K) ((is_primitive_root.iff_def _ n).1 (zeta_primitive_root n K L)).1,
+  rw [← ring_hom.map_one (algebra_map K L), norm_algebra_map, one_pow, monoid_hom.map_pow,
+    ← one_pow ↑n] at hz,
+  exact strict_mono.injective hodd.strict_mono_pow hz
+end
+
+/-- If `irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of
+`zeta n K L - 1` is `eval 1 (cyclotomic n ℤ)`. -/
+lemma norm_zeta_sub_one_eq_eval_cyclotomic (hirr : irreducible (cyclotomic n K)) (h : 2 < (n : ℕ)) :
+  norm K (zeta n K L - 1) = ↑(eval 1 (cyclotomic n ℤ)) :=
+begin
+  let E := algebraic_closure L,
+  obtain ⟨z, hz⟩ := is_alg_closed.exists_root _ (degree_cyclotomic_pos n E n.pos).ne.symm,
+  apply (algebra_map K E).injective,
+  letI := finite_dimensional {n} K L,
+  letI := is_galois n K L,
+  rw [norm_eq_prod_embeddings],
+  conv_lhs { congr, skip, funext,
+    rw [← neg_sub, alg_hom.map_neg, alg_hom.map_sub, alg_hom.map_one, neg_eq_neg_one_mul] },
+  rw [prod_mul_distrib, prod_const, card_univ, alg_hom.card, finrank L hirr,
+    nat.neg_one_pow_of_even (nat.totient_even h), one_mul],
+  have : univ.prod (λ (σ : L →ₐ[K] E), 1 - σ (zeta n K L)) = eval 1 (cyclotomic' n E),
+  { rw [cyclotomic', eval_prod, ← @finset.prod_attach E E, ← univ_eq_attach],
+    refine fintype.prod_equiv (zeta.embeddings_equiv_primitive_roots L E hirr) _ _ (λ σ, _),
+    simp },
+  haveI : ne_zero ((n : ℕ) : E) := (ne_zero.of_no_zero_smul_divisors K _ (n : ℕ)),
+  rw [this, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitive_roots (is_root_cyclotomic_iff.1 hz),
+      ← map_cyclotomic_int, (algebra_map K E).map_int_cast, ←int.cast_one, eval_int_cast_map,
+      ring_hom.eq_int_cast, int.cast_id]
+end
+
 end field
 
 end is_cyclotomic_extension