refactor(number_theory/cyclotomic/*): refactor the definition of is_c…

…yclotomic_extension (#14463)

We modify the definition of `is_cyclotomic_extension`, requiring the existence of a primitive root of unity rather than a root of the cyclotomic polynomial. This removes almost all the `ne_zero` assumptions.

src/algebra/char_p/basic.lean

@@ -360,6 +360,25 @@ char_ne_zero_of_fintype R (ring_char R)
 
 end
 
+section comm_ring
+
+variables [comm_ring R] [is_reduced R] {R}
+
+@[simp]
+lemma pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [fact p.prime]
+  [char_p R p] (x : R) :
+  x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 :=
+begin
+  induction k with k hk,
+  { rw [pow_zero, one_mul] },
+  { refine ⟨λ h, _, λ h, _⟩,
+    { rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h,
+      exact hk.1 (frobenius_inj R p h) },
+    { rw [pow_mul', h, one_pow] } }
+end
+
+end comm_ring
+
 section semiring
 open nat
 

src/algebra/ne_zero.lean

@@ -56,6 +56,13 @@ lemma trans [has_zero M] [has_coe R S] [has_coe_t S M] (h : ne_zero ((r : S) : M
 lemma of_map [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) [ne_zero (f r)] :
   ne_zero r := ⟨λ h, ne (f r) $ by convert map_zero f⟩
 
+lemma nat_of_ne_zero [semiring R] [semiring S] [ring_hom_class F R S] (f : F)
+  [hn : ne_zero (n : S)] : ne_zero (n : R) :=
+begin
+  apply ne_zero.of_map f,
+  simp [hn]
+end
+
 lemma of_injective [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M]
   {f : F} (hf : function.injective f) : ne_zero (f r) :=
 ⟨by { rw ←map_zero f, exact hf.ne (ne r) }⟩

src/number_theory/cyclotomic/discriminant.lean

@@ -35,13 +35,14 @@ discriminant of the power basis given by `ζ - 1`. -/
 lemma discr_zeta_eq_discr_zeta_sub_one (hζ : is_primitive_root ζ n) :
   discr ℚ (hζ.power_basis ℚ).basis = discr ℚ (hζ.sub_one_power_basis ℚ).basis :=
 begin
+  haveI : number_field K := number_field.mk,
   have H₁ : (aeval (hζ.power_basis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.sub_one_power_basis ℚ).gen :=
     by simp,
   have H₂ : (aeval (hζ.sub_one_power_basis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.power_basis ℚ).gen :=
     by simp,
   refine discr_eq_discr_of_to_matrix_coeff_is_integral _
-    (λ i j, to_matrix_is_integral H₁ _  _ _ _)
-    (λ i j, to_matrix_is_integral H₂ _  _ _ _),
+    (λ i j, to_matrix_is_integral H₁ _ _ _ _)
+    (λ i j, to_matrix_is_integral H₂ _ _ _ _),
   { exact hζ.is_integral n.pos },
   { refine minpoly.gcd_domain_eq_field_fractions _ (hζ.is_integral n.pos) },
   { exact is_integral_sub (hζ.is_integral n.pos) is_integral_one },
@@ -60,16 +61,12 @@ variables [algebra K L]
 `hζ.power_basis K` is `(-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
 if `irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/
 lemma discr_prime_pow_ne_two [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
+  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
   (hk : p ^ (k + 1) ≠ 2) :
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p ^ (k + 1) : ℕ).totient) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) :=
 begin
-  haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
-  { refine ⟨λ hzero, _⟩,
-    rw [pnat.pow_coe] at hzero,
-    simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
+  haveI hne := is_cyclotomic_extension.ne_zero' (p ^ (k + 1)) K L,
   have hp2 : p = 2 → 1 ≤ k,
   { intro hp,
     refine one_le_iff_ne_zero.2 (λ h, _),
@@ -128,7 +125,7 @@ begin
       { simpa only [← pnat.pow_coe, H, mul_comm _ (k + 1)] },
       { replace h := pow_eq_zero h,
         rw [coe_coe] at h,
-        exact ne_zero.ne _ h } },
+        simpa using hne.1 } },
     all_goals { apply_instance } },
   all_goals { apply_instance }
 end
@@ -137,8 +134,8 @@ end
 `hζ.power_basis K` is `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
 if `irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/
 lemma discr_prime_pow_ne_two' [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ (k + 1)))
-  (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hk : p ^ (k + 1) ≠ 2) :
+  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
+  (hk : p ^ (k + 1) ≠ 2) :
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p : ℕ) ^ k  * (p - 1)) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) :=
 by simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk
@@ -149,14 +146,12 @@ if `irreducible (cyclotomic (p ^ k) K))`. Beware that in the cases `p ^ k = 1` a
 the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform result.
 See also `is_cyclotomic_extension.discr_prime_pow_eq_unit_mul_pow`. -/
 lemma discr_prime_pow [hcycl : is_cyclotomic_extension {p ^ k} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ k))
-  (hirr : irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
+  (hζ : is_primitive_root ζ ↑(p ^ k)) (hirr : irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
   discr K (hζ.power_basis K).basis =
   (-1) ^ (((p ^ k : ℕ).totient) / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1)) :=
 begin
   unfreezingI { cases k },
-  { haveI : ne_zero ((↑(p ^ 0) : ℕ) : K) := ⟨by simp⟩,
-    simp only [coe_basis, pow_zero, power_basis_gen, totient_one, mul_zero, mul_one, show 1 / 2 = 0,
+  { simp only [coe_basis, pow_zero, power_basis_gen, totient_one, mul_zero, mul_one, show 1 / 2 = 0,
       by refl, discr, trace_matrix],
     have hζone : ζ = 1 := by simpa using hζ,
     rw [hζ.power_basis_dim _, hζone, ← (algebra_map K L).map_one,
@@ -167,11 +162,7 @@ begin
     { apply_instance },
     { exact hcycl } },
   { by_cases hk : p ^ (k + 1) = 2,
-    { haveI : ne_zero ((↑(p ^ (k + 1)) : ℕ) : K),
-      { refine ⟨λ hzero, _⟩,
-        rw [pnat.pow_coe] at hzero,
-        simpa [ne_zero.ne ((p : ℕ) : K)] using hzero },
-      have hp : p = 2,
+    { have hp : p = 2,
       { rw [← pnat.coe_inj, pnat.coe_bit0, pnat.one_coe, pnat.pow_coe, ← pow_one 2] at hk,
       replace hk := eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 nat.prime_two)
         (succ_pos _) hk,
@@ -199,7 +190,7 @@ end
 `n : ℕ` such that the discriminant of `hζ.power_basis K` is `u * p ^ n`. Often this is enough and
 less cumbersome to use than `is_cyclotomic_extension.discr_prime_pow`. -/
 lemma discr_prime_pow_eq_unit_mul_pow [is_cyclotomic_extension {p ^ k} K L]
-  [hp : fact (p : ℕ).prime] [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ ↑(p ^ k))
+  [hp : fact (p : ℕ).prime] (hζ : is_primitive_root ζ ↑(p ^ k))
   (hirr : irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
   ∃ (u : ℤˣ) (n : ℕ), discr K (hζ.power_basis K).basis = u * p ^ n :=
 begin
@@ -214,8 +205,7 @@ end
 `discr K (hζ.power_basis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)` if
 `irreducible (cyclotomic p K)`. -/
 lemma discr_odd_prime [is_cyclotomic_extension {p} K L] [hp : fact (p : ℕ).prime]
-  [ne_zero ((p : ℕ) : K)] (hζ : is_primitive_root ζ p) (hirr : irreducible (cyclotomic p K))
-  (hodd : p ≠ 2) :
+  (hζ : is_primitive_root ζ p) (hirr : irreducible (cyclotomic p K)) (hodd : p ≠ 2) :
   discr K (hζ.power_basis K).basis = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) :=
 begin
   haveI : is_cyclotomic_extension {p ^ (0 + 1)} K L,

src/number_theory/cyclotomic/gal.lean

@@ -16,10 +16,9 @@ it is always a subgroup, and if the `n`th cyclotomic polynomial is irreducible,
 ## Main results
 
 * `is_primitive_root.aut_to_pow_injective`: `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.
-* `is_cyclotomic_extension.aut_equiv_pow`: If, additionally, the `n`th cyclotomic polynomial is
-  irreducible in K, then `aut_to_pow` is a `mul_equiv` (for example, in ℚ and certain 𝔽ₚ).
+  in the case that it's considered over a cyclotomic field extension.
+* `is_cyclotomic_extension.aut_equiv_pow`: If the `n`th cyclotomic polynomial is irreducible
+  in `K`, then `aut_to_pow` is a `mul_equiv` (for example, in `ℚ` and certain `𝔽ₚ`).
 * `gal_X_pow_equiv_units_zmod`, `gal_cyclotomic_equiv_units_zmod`: Repackage `aut_equiv_pow` in
   terms of `polynomial.gal`.
 * `is_cyclotomic_extension.aut.comm_group`: Cyclotomic extensions are abelian.
@@ -43,14 +42,14 @@ local attribute [instance] pnat.fact_pos
 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]
 
-open polynomial ne_zero is_cyclotomic_extension
+open polynomial is_cyclotomic_extension
 
 open_locale cyclotomic
 
 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. -/
+field extension. -/
 lemma aut_to_pow_injective : function.injective $ hμ.aut_to_pow K :=
 begin
   intros f g hfg,
@@ -80,9 +79,8 @@ 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) :=
-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 _
+noncomputable def aut.comm_group : comm_group (L ≃ₐ[K] L) :=
+((zeta_spec n K L).aut_to_pow_injective K).comm_group _
   (map_one _) (map_mul _) (map_inv _) (map_div _) (map_pow _) (map_zpow _)
 
 variables (h : irreducible (cyclotomic n K)) {K} (L)
@@ -91,17 +89,16 @@ include h
 
 /-- 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
-let hζ := zeta_primitive_root n K L,
+@[simps] noncomputable def aut_equiv_pow : (L ≃ₐ[K] L) ≃* (zmod n)ˣ :=
+let hζ := zeta_spec 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
+    haveI := is_cyclotomic_extension.ne_zero' n K L,
     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
+               ((zeta_spec n K L).pow_of_coprime _ (zmod.val_coe_unit_coprime t)) h,
+    exact ((zeta_spec 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],
@@ -123,24 +120,23 @@ let hζ := zeta_primitive_root n K L,
     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,
-        ←(zeta_primitive_root n K L).eq_order_of, ←zmod.eq_iff_modeq_nat] at key,
+        ←(zeta_spec n K L).eq_order_of, ←zmod.eq_iff_modeq_nat] at key,
     simp only [zmod.nat_cast_val, zmod.cast_id', id.def] at key,
     exact units.ext key
   end,
-  .. (zeta_primitive_root n K L).aut_to_pow K }
+  .. (zeta_spec n K L).aut_to_pow K }
 
 include 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
+noncomputable def from_zeta_aut : L ≃ₐ[K] L :=
+let hζ := (zeta_spec n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one n.pos in
 (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μ
+((zeta_spec 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 hμ h (zeta n K L) = μ :=
+lemma from_zeta_aut_spec : from_zeta_aut hμ h (zeta n K L) = μ :=
 begin
   simp_rw [from_zeta_aut, aut_equiv_pow_symm_apply],
   generalize_proofs _ _ hζ h _ hμ _,
@@ -157,17 +153,17 @@ section gal
 variables (h : irreducible (cyclotomic n K)) {K}
 
 /-- `is_cyclotomic_extension.aut_equiv_pow` repackaged in terms of `gal`. Asserts that the
-Galois group of `cyclotomic n K` 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_cyclotomic_equiv_units_zmod [ne_zero ((n : ℕ) : K)] :
+Galois group of `cyclotomic n K` is equivalent to `(zmod n)ˣ` if `cyclotomic n K` is irreducible in
+the base field. -/
+noncomputable def gal_cyclotomic_equiv_units_zmod :
   (cyclotomic n K).gal ≃* (zmod n)ˣ :=
 (alg_equiv.aut_congr (is_splitting_field.alg_equiv _ _)).symm.trans
 (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)] :
+Galois group of `X ^ n - 1` is equivalent to `(zmod n)ˣ` if `cyclotomic n K` is irreducible in the
+base field. -/
+noncomputable def gal_X_pow_equiv_units_zmod :
   (X ^ (n : ℕ) - 1).gal ≃* (zmod n)ˣ :=
 (alg_equiv.aut_congr (is_splitting_field.alg_equiv _ _)).symm.trans
 (is_cyclotomic_extension.aut_equiv_pow L h)