chore(number_theory/cyclotomic/zeta): generalize to primitive roots (#11941)

This was done as `(zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ)) = zeta p ℚ ℚ(ζₚ)` is independent of Lean's type theory. Allows far more flexibility with results.



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

Author: ericrbg

src/number_theory/cyclotomic/gal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
 
-import number_theory.cyclotomic.zeta
+import number_theory.cyclotomic.primitive_roots
 import field_theory.polynomial_galois_group
 
 /-!
@@ -40,19 +40,16 @@ it is always a subgroup, and if the `n`th cyclotomic polynomial is irreducible,
 
 local attribute [instance] pnat.fact_pos
 
-variables (n : ℕ+) (K : Type*) [field K] (L : Type*) [field L] {μ : L} (hμ : is_primitive_root μ n)
+variables {n : ℕ+} (K : Type*) [field K] {L : Type*} [field L] {μ : L} (hμ : is_primitive_root μ n)
           [algebra K L] [is_cyclotomic_extension {n} K L]
 
-local notation `ζ` := is_cyclotomic_extension.zeta n K L
+open polynomial ne_zero is_cyclotomic_extension
 
-open polynomial ne_zero
-
-namespace is_cyclotomic_extension
+namespace is_primitive_root
 
 /-- `is_primitive_root.aut_to_pow` is injective in the case that it's considered over a cyclotomic
 field extension, where `n` does not divide the characteristic of K. -/
-lemma aut_to_pow_injective [ne_zero ((n : ℕ) : K)] : function.injective $
-    (@zeta_primitive_root n K L _ _ _ _ _ $ of_no_zero_smul_divisors K L n).aut_to_pow K :=
+lemma aut_to_pow_injective : function.injective $ hμ.aut_to_pow K :=
 begin
   intros f g hfg,
   apply_fun units.val at hfg,
@@ -61,67 +58,66 @@ begin
   have hf := hf'.some_spec,
   have hg := hg'.some_spec,
   generalize_proofs hζ at hf hg,
-  suffices : f hζ.to_roots_of_unity = g hζ.to_roots_of_unity,
+  suffices : f hμ.to_roots_of_unity = g hμ.to_roots_of_unity,
   { apply alg_equiv.coe_alg_hom_injective,
-    apply (zeta.power_basis n K L).alg_hom_ext,
+    apply (hμ.power_basis K).alg_hom_ext,
     exact this },
   rw zmod.eq_iff_modeq_nat at hfg,
   refine (hf.trans _).trans hg.symm,
   rw [←roots_of_unity.coe_pow _ hf'.some, ←roots_of_unity.coe_pow _ hg'.some],
   congr' 1,
   rw [pow_eq_pow_iff_modeq],
   convert hfg,
-  rw [hζ.eq_order_of],
-  rw [←hζ.coe_to_roots_of_unity_coe] {occs := occurrences.pos [2]},
+  rw [hμ.eq_order_of],
+  rw [←hμ.coe_to_roots_of_unity_coe] {occs := occurrences.pos [2]},
   rw [order_of_units, order_of_subgroup]
 end
 
+end is_primitive_root
+
+namespace is_cyclotomic_extension
+
 /-- Cyclotomic extensions are abelian. -/
 noncomputable def aut.comm_group [ne_zero ((n : ℕ) : K)] : comm_group (L ≃ₐ[K] L) :=
-(aut_to_pow_injective n K L).comm_group _ (map_one _) (map_mul _) (map_inv _) (map_div _)
-
-/-- The power basis given by `ζ ^ t`. -/
-@[simps] noncomputable def zeta_pow_power_basis [ne_zero ((n : ℕ) : K)] (t : (zmod n)ˣ) :
-  power_basis K L :=
-begin
-  haveI := of_no_zero_smul_divisors K L n,
-  refine power_basis.map (algebra.adjoin.power_basis $ integral {n} K L $ ζ ^ (t : zmod n).val) _,
-  refine (subalgebra.equiv_of_eq _ _ (adjoin_primitive_root_eq_top n _ _)).trans algebra.top_equiv,
-  exact (zeta_primitive_root n K L).pow_of_coprime _ (zmod.val_coe_unit_coprime t),
-end
+let _ := of_no_zero_smul_divisors K L n in by exactI
+((zeta_primitive_root n K L).aut_to_pow_injective K).comm_group _
+  (map_one _) (map_mul _) (map_inv _) (map_div _)
 
-variables (h : irreducible (cyclotomic n K)) {K}
+variables (h : irreducible (cyclotomic n K)) {K} (L)
 
 include h
 
-/-- The `mul_equiv` that takes an automorphism to the power of μ that μ gets mapped to under it.
-    A stronger version of `is_primitive_root.aut_to_pow`. -/
+/-- The `mul_equiv` that takes an automorphism `f` to the element `k : (zmod n)ˣ` such that
+  `f μ = μ ^ k`. A stronger version of `is_primitive_root.aut_to_pow`. -/
 @[simps] noncomputable def aut_equiv_pow [ne_zero ((n : ℕ) : K)] : (L ≃ₐ[K] L) ≃* (zmod n)ˣ :=
-let hn := of_no_zero_smul_divisors K L n in by exactI
-{ inv_fun := λ t, (zeta.power_basis n K L).equiv_of_minpoly (zeta_pow_power_basis n K L t)
+let hn := of_no_zero_smul_divisors K L n in
+by exactI
+let hζ := zeta_primitive_root n K L,
+    hμ := λ t, hζ.pow_of_coprime _ (zmod.val_coe_unit_coprime t) in
+{ inv_fun := λ t, (hζ.power_basis K).equiv_of_minpoly ((hμ t).power_basis K)
   begin
-    simp only [zeta.power_basis_gen, zeta_pow_power_basis_gen],
+    simp only [is_primitive_root.power_basis_gen],
     have hr := is_primitive_root.minpoly_eq_cyclotomic_of_irreducible
                ((zeta_primitive_root n K L).pow_of_coprime _ (zmod.val_coe_unit_coprime t)) h,
     exact ((zeta_primitive_root n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr
   end,
   left_inv := λ f, begin
     simp only [monoid_hom.to_fun_eq_coe],
     apply alg_equiv.coe_alg_hom_injective,
-    apply (zeta.power_basis n K L).alg_hom_ext,
+    apply (hζ.power_basis K).alg_hom_ext,
     simp only [alg_equiv.coe_alg_hom, alg_equiv.map_pow],
     rw power_basis.equiv_of_minpoly_gen,
-    simp only [zeta_pow_power_basis_gen, zeta.power_basis_gen, is_primitive_root.aut_to_pow_spec],
+    simp only [is_primitive_root.power_basis_gen, is_primitive_root.aut_to_pow_spec],
   end,
   right_inv := λ x, begin
     simp only [monoid_hom.to_fun_eq_coe],
-    generalize_proofs _ hζ _ h,
-    have key := hζ.aut_to_pow_spec K ((zeta.power_basis n K L).equiv_of_minpoly
-                                      (zeta_pow_power_basis n K L x) h),
-    have := (zeta.power_basis n K L).equiv_of_minpoly_gen,
-    rw zeta.power_basis_gen at this {occs := occurrences.pos [2]},
-    rw [this, zeta_pow_power_basis_gen] at key,
-    rw ← hζ.coe_to_roots_of_unity_coe at key {occs := occurrences.pos [1, 3]},
+    generalize_proofs _ _ _ h,
+    have key := hζ.aut_to_pow_spec K ((hζ.power_basis K).equiv_of_minpoly
+                                      ((hμ x).power_basis K) h),
+    have := (hζ.power_basis K).equiv_of_minpoly_gen ((hμ x).power_basis K) h,
+    rw hζ.power_basis_gen K at this,
+    rw [this, is_primitive_root.power_basis_gen] at key,
+    rw ← hζ.coe_to_roots_of_unity_coe at key {occs := occurrences.pos [1, 5]},
     simp only [←coe_coe, ←roots_of_unity.coe_pow] at key,
     replace key := roots_of_unity.coe_injective key,
     rw [pow_eq_pow_iff_modeq, ←order_of_subgroup, ←order_of_units, hζ.coe_to_roots_of_unity_coe,
@@ -131,33 +127,28 @@ let hn := of_no_zero_smul_divisors K L n in by exactI
   end,
   .. (zeta_primitive_root n K L).aut_to_pow K }
 
-end is_cyclotomic_extension
+include hμ
 
-open is_cyclotomic_extension
-
-namespace is_primitive_root
-
-variables (h : irreducible (cyclotomic n K)) {K L}
-
-include h hμ
+variables {L}
 
 /-- Maps `μ` to the `alg_equiv` that sends `is_cyclotomic_extension.zeta` to `μ`. -/
 noncomputable def from_zeta_aut [ne_zero ((n : ℕ) : K)] : L ≃ₐ[K] L :=
 have _ := of_no_zero_smul_divisors K L n, by exactI
 let hζ := (zeta_primitive_root n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos in
-(aut_equiv_pow n L h).symm $ zmod.unit_of_coprime hζ.some $
+(aut_equiv_pow L h).symm $ zmod.unit_of_coprime hζ.some $
 ((zeta_primitive_root n K L).pow_iff_coprime n.pos hζ.some).mp $ hζ.some_spec.some_spec.symm ▸ hμ
 
-lemma from_zeta_aut_spec [ne_zero ((n : ℕ) : K)] : from_zeta_aut n hμ h ζ = μ :=
+lemma from_zeta_aut_spec [ne_zero ((n : ℕ) : K)] : from_zeta_aut hμ h (zeta n K L) = μ :=
 begin
-  simp only [from_zeta_aut, exists_prop, aut_equiv_pow_symm_apply, ←zeta.power_basis_gen,
-             power_basis.equiv_of_minpoly_gen, zeta_pow_power_basis_gen, zmod.coe_unit_of_coprime],
-  generalize_proofs hζ,
-  convert hζ.some_spec.2,
-  exact zmod.val_cast_of_lt hζ.some_spec.1
+  simp_rw [from_zeta_aut, aut_equiv_pow_symm_apply],
+  generalize_proofs _ hζ h _ hμ _,
+  rw [←hζ.power_basis_gen K] {occs := occurrences.pos [4]},
+  rw [power_basis.equiv_of_minpoly_gen, hμ.power_basis_gen K],
+  convert h.some_spec.some_spec,
+  exact zmod.val_cast_of_lt h.some_spec.some
 end
 
-end is_primitive_root
+end is_cyclotomic_extension
 
 section gal
 
@@ -171,14 +162,14 @@ characteristic of `K`, and `cyclotomic n K` is irreducible in the base field. -/
 noncomputable def gal_cyclotomic_equiv_units_zmod [ne_zero ((n : ℕ) : K)] :
   (cyclotomic n K).gal ≃* (zmod n)ˣ :=
 (alg_equiv.aut_congr (is_splitting_field.alg_equiv _ _)).symm.trans
-(is_cyclotomic_extension.aut_equiv_pow n L h)
+(is_cyclotomic_extension.aut_equiv_pow L h)
 
 /-- `is_cyclotomic_extension.aut_equiv_pow` repackaged in terms of `gal`. Asserts that the
 Galois group of `X ^ n - 1` is equivalent to `(zmod n)ˣ` if `n` does not divide the characteristic
 of `K`, and `cyclotomic n K` is irreducible in the base field. -/
 noncomputable def gal_X_pow_equiv_units_zmod [ne_zero ((n : ℕ) : K)] :
   (X ^ (n : ℕ) - 1).gal ≃* (zmod n)ˣ :=
 (alg_equiv.aut_congr (is_splitting_field.alg_equiv _ _)).symm.trans
-(is_cyclotomic_extension.aut_equiv_pow n L h)
+(is_cyclotomic_extension.aut_equiv_pow L h)
 
 end gal

src/number_theory/cyclotomic/primitive_roots.lean

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2022 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Best, Riccardo Brasca, Eric Rodriguez
+-/
+
+import number_theory.cyclotomic.basic
+import ring_theory.adjoin.power_basis
+import ring_theory.norm
+
+/-!
+# Primitive roots in cyclotomic fields
+If `is_cyclotomic_extension {n} A B`, we define an element `zeta n A B : B` that is (under certain
+assumptions) a primitive `n`-root of unity in `B` and we study its properties. We also prove related
+theorems under the more general assumption of just being a primitive root, for reasons described
+in the implementation details section.
+
+## Main definitions
+* `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_primitive_root.power_basis`: if `K` and `L` are fields such that
+  `is_cyclotomic_extension {n} K L` and `ne_zero (↑n : K)`, then `is_primitive_root.power_basis`
+  gives a K-power basis for L given a primitive root `ζ`.
+* `is_primitive_root.embeddings_equiv_primitive_roots`: the equivalence between `L →ₐ[K] A`
+  and `primitive_roots n A` given by the choice of `ζ`.
+
+## Main results
+* `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_primitive_root.norm_eq_one`: If `K` is linearly ordered (in particular for `K = ℚ`), the norm
+  of a primitive root is `1` if `n` is odd.
+* `is_primitive_root.sub_one_norm_eq_eval_cyclotomic`: If `irreducible (cyclotomic n K)`, then
+  the norm of `ζ - 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)`.
+
+`zeta n A B` is defined using `exists.some`, which means we cannot control it.
+For example, in normal mathematics, we can demand that `(zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ))` is equal to
+`zeta p ℚ ℚ(ζₚ)`, as we are just choosing "an arbitrary primitive root" and we can internally
+specify that our choices agree. This is not the case here, and it is indeed impossible to prove that
+these two are equal. Therefore, whenever possible, we prove our results for any primitive root,
+and only at the "final step", when we need to provide an "explicit" primitive root, we use `zeta`.
+
+-/
+
+open polynomial algebra finset finite_dimensional is_cyclotomic_extension
+
+
+universes u v w z
+
+variables {n : ℕ+} (A : Type w) (B : Type z) (K : Type u) {L : Type v} (C : Type w)
+variables [comm_ring A] [comm_ring B] [algebra A B] [is_cyclotomic_extension {n} A B]
+
+section zeta
+
+namespace is_cyclotomic_extension
+
+variables (n)
+
+/-- If `B` is a `n`-th cyclotomic extension of `A`, then `zeta n A B` is any root of
+`cyclotomic n A` in L. -/
+noncomputable def zeta : B :=
+  (exists_root $ set.mem_singleton n : ∃ r : B, aeval r (cyclotomic n A) = 0).some
+
+@[simp] lemma zeta_spec : aeval (zeta n A B) (cyclotomic n A) = 0 :=
+classical.some_spec (exists_root (set.mem_singleton n) : ∃ r : B, aeval r (cyclotomic n A) = 0)
+
+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] }
+
+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)] :
+  is_primitive_root (zeta n A B) n :=
+by { rw ←is_root_cyclotomic_iff, exact zeta_spec' n A B }
+
+end is_cyclotomic_extension
+
+end zeta
+
+section no_order
+
+variables [field K] [field L] [comm_ring C] [algebra K L] [algebra K C]
+          [is_cyclotomic_extension {n} K L]
+          {ζ : L} (hζ : is_primitive_root ζ n)
+
+namespace is_primitive_root
+
+/-- The `power_basis` given by a primitive root `ζ`. -/
+@[simps] noncomputable def power_basis : power_basis K L :=
+power_basis.map (algebra.adjoin.power_basis $ integral {n} K L ζ) $
+(subalgebra.equiv_of_eq _ _ (is_cyclotomic_extension.adjoin_primitive_root_eq_top n _ hζ)).trans
+top_equiv
+
+variables {K}
+
+/-- The equivalence between `L →ₐ[K] A` and `primitive_roots n A` given by a primitive root `ζ`. -/
+@[simps] noncomputable def embeddings_equiv_primitive_roots [is_domain C] [ne_zero ((n : ℕ) : K)]
+  (hirr : irreducible (cyclotomic n K)) : (L →ₐ[K] C) ≃ primitive_roots n C :=
+((hζ.power_basis K).lift_equiv).trans
+{ to_fun    := λ x,
+  begin
+    haveI hn := ne_zero.of_no_zero_smul_divisors K C n,
+    refine ⟨x.1, _⟩,
+    cases x,
+    rwa [mem_primitive_roots n.pos, ←is_root_cyclotomic_iff, is_root.def,
+         ←map_cyclotomic _ (algebra_map K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
+         ←eval₂_eq_eval_map, ←aeval_def]
+  end,
+  inv_fun   := λ x,
+  begin
+    haveI hn := ne_zero.of_no_zero_smul_divisors K C n,
+    refine ⟨x.1, _⟩,
+    cases x,
+    rwa [aeval_def, eval₂_eq_eval_map, hζ.power_basis_gen K,
+         ←hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_cyclotomic, ←is_root.def,
+         is_root_cyclotomic_iff, ← mem_primitive_roots n.pos]
+  end,
+  left_inv  := λ x, subtype.ext rfl,
+  right_inv := λ x, subtype.ext rfl }
+
+end is_primitive_root
+
+namespace is_cyclotomic_extension
+
+variables {K} (L)
+
+/-- 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)) [ne_zero ((n : ℕ) : K)] :
+  finrank K L = (n : ℕ).totient :=
+begin
+  haveI := ne_zero.of_no_zero_smul_divisors K L n,
+  rw [((zeta_primitive_root n K L).power_basis K).finrank, is_primitive_root.power_basis_dim,
+      ←(zeta_primitive_root n K L).minpoly_eq_cyclotomic_of_irreducible hirr, nat_degree_cyclotomic]
+end
+
+end is_cyclotomic_extension
+
+end no_order
+
+namespace is_primitive_root
+
+section norm
+
+variables [field L] {ζ : L} (hζ : is_primitive_root ζ n)
+
+include hζ
+
+/-- If `K` is linearly ordered (in particular for `K = ℚ`), the norm of a primitive root is `1`
+if `n` is odd. -/
+lemma norm_eq_one [linear_ordered_field K] [algebra K L] (hodd : odd (n : ℕ)) : norm K ζ = 1 :=
+begin
+  haveI := ne_zero.of_no_zero_smul_divisors K L n,
+  have hz := congr_arg (norm K) ((is_primitive_root.iff_def _ n).1 hζ).1,
+  rw [←(algebra_map K L).map_one , norm_algebra_map, one_pow, map_pow, ←one_pow ↑n] at hz,
+  exact strict_mono.injective hodd.strict_mono_pow hz
+end
+
+variables {K}
+
+/-- 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 [field K] [algebra K L] [is_cyclotomic_extension {n} K L]
+  [ne_zero ((n : ℕ) : K)] (h : 2 < (n : ℕ)) (hirr : irreducible (cyclotomic n K)) :
+  norm K (ζ - 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, is_cyclotomic_extension.finrank L hirr,
+      nat.neg_one_pow_of_even (nat.totient_even h), one_mul],
+  have : univ.prod (λ (σ : L →ₐ[K] E), 1 - σ ζ) = eval 1 (cyclotomic' n E),
+  { rw [cyclotomic', eval_prod, ← @finset.prod_attach E E, ← univ_eq_attach],
+    refine fintype.prod_equiv (hζ.embeddings_equiv_primitive_roots 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 norm
+
+end is_primitive_root