feat(number_theory/legendre_symbol/*): redefine quadratic characters …

…as `mul_char`s (#15418) This is a follow-up to #14768; it defines quadratic characters (and also the characters on `zmod 4` and `zmod 8`) to be of type `mul_char F int` (where `F` is a finite field). Some content of `number_theory/legendre_symbol/quadratic_char` is moved within the file; one proof is replaced by directly using the corresponding more general result. See here on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters/near/289635166).
leanprover-community · Jul 18, 2022 · b29f384 · b29f384
1 parent f51aaae
commit b29f384
Show file tree

Hide file tree

Showing 3 changed files with 113 additions and 75 deletions.
diff --git a/src/number_theory/legendre_symbol/quadratic_char.lean b/src/number_theory/legendre_symbol/quadratic_char.lean
@@ -33,8 +33,11 @@ if `a` is a square, otherwise it is `-1`.
 
 This only deserves the name "character" when it is multiplicative,
 e.g., when `α` is a finite field. See `quadratic_char_mul`.
+
+We will later define `quadratic_char` to be a multiplicative character
+of type `mul_char F ℤ`, when the domain is a finite field `F`.
 -/
-def quadratic_char (α : Type*) [monoid_with_zero α] [decidable_eq α]
+def quadratic_char_fun (α : Type*) [monoid_with_zero α] [decidable_eq α]
   [decidable_pred (is_square : α → Prop)] (a : α) : ℤ :=
 if a = 0 then 0 else if is_square a then 1 else -1
 
@@ -50,58 +53,50 @@ The interesting case is when the characteristic of `F` is odd.
 
 section quadratic_char
 
+open mul_char
+
 variables {F : Type*} [field F] [fintype F] [decidable_eq F]
 
 /-- Some basic API lemmas -/
-lemma quadratic_char_eq_zero_iff (a : F) : quadratic_char F a = 0 ↔ a = 0 :=
+lemma quadratic_char_eq_zero_iff' {a : F} : quadratic_char_fun F a = 0 ↔ a = 0 :=
 begin
-  simp only [quadratic_char],
+  simp only [quadratic_char_fun],
   by_cases ha : a = 0,
   { simp only [ha, eq_self_iff_true, if_true], },
   { simp only [ha, if_false, iff_false],
     split_ifs; simp only [neg_eq_zero, one_ne_zero, not_false_iff], },
 end
 
 @[simp]
-lemma quadratic_char_zero : quadratic_char F 0 = 0 :=
-by simp only [quadratic_char, eq_self_iff_true, if_true, id.def]
+lemma quadratic_char_zero : quadratic_char_fun F 0 = 0 :=
+by simp only [quadratic_char_fun, eq_self_iff_true, if_true, id.def]
 
 @[simp]
-lemma quadratic_char_one : quadratic_char F 1 = 1 :=
-by simp only [quadratic_char, one_ne_zero, is_square_one, if_true, if_false, id.def]
-
-/-- For nonzero `a : F`, `quadratic_char F a = 1 ↔ is_square a`. -/
-lemma quadratic_char_one_iff_is_square {a : F} (ha : a ≠ 0) :
-  quadratic_char F a = 1 ↔ is_square a :=
-by { simp only [quadratic_char, ha, (dec_trivial : (-1 : ℤ) ≠ 1), if_false, ite_eq_left_iff],
-     tauto, }
+lemma quadratic_char_one : quadratic_char_fun F 1 = 1 :=
+by simp only [quadratic_char_fun, one_ne_zero, is_square_one, if_true, if_false, id.def]
 
-/-- The quadratic character takes the value `1` on nonzero squares. -/
-lemma quadratic_char_sq_one' {a : F} (ha : a ≠ 0) : quadratic_char F (a ^ 2) = 1 :=
-by simp only [quadratic_char, ha, pow_eq_zero_iff, nat.succ_pos', is_square_sq, if_true, if_false]
-
-/-- If `ring_char F = 2`, then `quadratic_char F` takes the value `1` on nonzero elements. -/
-lemma quadratic_char_eq_one_of_char_two (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :
-  quadratic_char F a = 1 :=
+/-- If `ring_char F = 2`, then `quadratic_char_fun F` takes the value `1` on nonzero elements. -/
+lemma quadratic_char_eq_one_of_char_two' (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :
+  quadratic_char_fun F a = 1 :=
 begin
-  simp only [quadratic_char, ha, if_false, ite_eq_left_iff],
+  simp only [quadratic_char_fun, ha, if_false, ite_eq_left_iff],
   intro h,
   exfalso,
   exact h (finite_field.is_square_of_char_two hF a),
 end
 
-/-- If `ring_char F` is odd, then `quadratic_char F a` can be computed in
+/-- If `ring_char F` is odd, then `quadratic_char_fun F a` can be computed in
 terms of `a ^ (fintype.card F / 2)`. -/
-lemma quadratic_char_eq_pow_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
-  quadratic_char F a = if a ^ (fintype.card F / 2) = 1 then 1 else -1 :=
+lemma quadratic_char_eq_pow_of_char_ne_two' (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
+  quadratic_char_fun F a = if a ^ (fintype.card F / 2) = 1 then 1 else -1 :=
 begin
-  simp only [quadratic_char, ha, if_false],
+  simp only [quadratic_char_fun, ha, if_false],
   simp_rw finite_field.is_square_iff hF ha,
 end
 
 /-- The quadratic character is multiplicative. -/
 lemma quadratic_char_mul (a b : F) :
-  quadratic_char F (a * b) = quadratic_char F a * quadratic_char F b :=
+  quadratic_char_fun F (a * b) = quadratic_char_fun F a * quadratic_char_fun F b :=
 begin
   by_cases ha : a = 0,
   { rw [ha, zero_mul, quadratic_char_zero, zero_mul], },
@@ -112,14 +107,14 @@ begin
   have hab := mul_ne_zero ha hb,
   by_cases hF : ring_char F = 2,
   { -- case `ring_char F = 2`
-    rw [quadratic_char_eq_one_of_char_two hF ha,
-        quadratic_char_eq_one_of_char_two hF hb,
-        quadratic_char_eq_one_of_char_two hF hab,
+    rw [quadratic_char_eq_one_of_char_two' hF ha,
+        quadratic_char_eq_one_of_char_two' hF hb,
+        quadratic_char_eq_one_of_char_two' hF hab,
         mul_one], },
   { -- case of odd characteristic
-    rw [quadratic_char_eq_pow_of_char_ne_two hF ha,
-        quadratic_char_eq_pow_of_char_ne_two hF hb,
-        quadratic_char_eq_pow_of_char_ne_two hF hab,
+    rw [quadratic_char_eq_pow_of_char_ne_two' hF ha,
+        quadratic_char_eq_pow_of_char_ne_two' hF hb,
+        quadratic_char_eq_pow_of_char_ne_two' hF hab,
         mul_pow],
     cases finite_field.pow_dichotomy hF hb with hb' hb',
     { simp only [hb', mul_one, eq_self_iff_true, if_true], },
@@ -129,16 +124,35 @@ begin
         simp only [ha', h, neg_neg, eq_self_iff_true, if_true, if_false], }, },
 end
 
-/-- The quadratic character is a homomorphism of monoids with zero. -/
-@[simps] def quadratic_char_hom : F →*₀ ℤ :=
-{ to_fun := quadratic_char F,
-  map_zero' := quadratic_char_zero,
+variables (F)
+
+/-- The quadratic character as a multiplicative character. -/
+@[simps] def quadratic_char : mul_char F ℤ :=
+{ to_fun := quadratic_char_fun F,
   map_one' := quadratic_char_one,
-  map_mul' := quadratic_char_mul }
+  map_mul' := quadratic_char_mul,
+  map_nonunit' := λ a ha, by { rw of_not_not (mt ne.is_unit ha), exact quadratic_char_zero, } }
+
+variables {F}
+
+/-- The value of the quadratic character on `a` is zero iff `a = 0`. -/
+lemma quadratic_char_eq_zero_iff {a : F} : quadratic_char F a = 0 ↔ a = 0 :=
+quadratic_char_eq_zero_iff'
+
+/-- For nonzero `a : F`, `quadratic_char F a = 1 ↔ is_square a`. -/
+lemma quadratic_char_one_iff_is_square {a : F} (ha : a ≠ 0) :
+  quadratic_char F a = 1 ↔ is_square a :=
+by simp only [quadratic_char_apply, quadratic_char_fun, ha, (dec_trivial : (-1 : ℤ) ≠ 1),
+              if_false, ite_eq_left_iff, imp_false, not_not]
+
+/-- The quadratic character takes the value `1` on nonzero squares. -/
+lemma quadratic_char_sq_one' {a : F} (ha : a ≠ 0) : quadratic_char F (a ^ 2) = 1 :=
+by simp only [quadratic_char_fun, ha, pow_eq_zero_iff, nat.succ_pos', is_square_sq, if_true,
+              if_false, quadratic_char_apply]
 
 /-- The square of the quadratic character on nonzero arguments is `1`. -/
 lemma quadratic_char_sq_one {a : F} (ha : a ≠ 0) : (quadratic_char F a) ^ 2 = 1 :=
-by rwa [pow_two, ← quadratic_char_mul, ← pow_two, quadratic_char_sq_one']
+by rwa [pow_two, ← map_mul, ← pow_two, quadratic_char_sq_one']
 
 /-- The quadratic character is `1` or `-1` on nonzero arguments. -/
 lemma quadratic_char_dichotomy {a : F} (ha : a ≠ 0) :
@@ -159,22 +173,57 @@ lemma quadratic_char_neg_one_iff_not_is_square {a : F} :
   quadratic_char F a = -1 ↔ ¬ is_square a :=
 begin
   by_cases ha : a = 0,
-  { simp only [ha, is_square_zero, quadratic_char_zero, zero_eq_neg, one_ne_zero, not_true], },
+  { simp only [ha, is_square_zero, mul_char.map_zero, zero_eq_neg, one_ne_zero, not_true], },
   { rw [quadratic_char_eq_neg_one_iff_not_one ha, quadratic_char_one_iff_is_square ha] },
 end
 
 /-- If `F` has odd characteristic, then `quadratic_char F` takes the value `-1`. -/
 lemma quadratic_char_exists_neg_one (hF : ring_char F ≠ 2) : ∃ a, quadratic_char F a = -1 :=
-(finite_field.exists_nonsquare hF).imp (λ b h₁, quadratic_char_neg_one_iff_not_is_square.mpr h₁)
+(finite_field.exists_nonsquare hF).imp $ λ b h₁, quadratic_char_neg_one_iff_not_is_square.mpr h₁
+
+/-- If `ring_char F = 2`, then `quadratic_char F` takes the value `1` on nonzero elements. -/
+lemma quadratic_char_eq_one_of_char_two (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :
+  quadratic_char F a = 1 :=
+quadratic_char_eq_one_of_char_two' hF ha
+
+/-- If `ring_char F` is odd, then `quadratic_char F a` can be computed in
+terms of `a ^ (fintype.card F / 2)`. -/
+lemma quadratic_char_eq_pow_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
+  quadratic_char F a = if a ^ (fintype.card F / 2) = 1 then 1 else -1 :=
+quadratic_char_eq_pow_of_char_ne_two' hF ha
+
+variables (F)
+
+/-- The quadratic character is quadratic as a multiplicative character. -/
+lemma quadratic_char_is_quadratic : (quadratic_char F).is_quadratic :=
+begin
+  intro a,
+  by_cases ha : a = 0,
+  { left, rw ha, exact quadratic_char_zero, },
+  { right, exact quadratic_char_dichotomy ha, },
+end
+
+variables {F}
+
+/-- The quadratic character is nontrivial as a multiplicative character
+when the domain has odd characteristic. -/
+lemma quadratic_char_is_nontrivial (hF : ring_char F ≠ 2) : (quadratic_char F).is_nontrivial :=
+begin
+  rcases quadratic_char_exists_neg_one hF with ⟨a, ha⟩,
+  have hu : is_unit a := by { by_contra hf, rw map_nonunit _ hf at ha, norm_num at ha, },
+  refine ⟨hu.unit, (_ : quadratic_char F a ≠ 1)⟩,
+  rw ha,
+  norm_num,
+end
 
 /-- The number of solutions to `x^2 = a` is determined by the quadratic character. -/
 lemma quadratic_char_card_sqrts (hF : ring_char F ≠ 2) (a : F) :
   ↑{x : F | x^2 = a}.to_finset.card = quadratic_char F a + 1 :=
 begin
   -- we consider the cases `a = 0`, `a` is a nonzero square and `a` is a nonsquare in turn
   by_cases h₀ : a = 0,
-  { simp only [h₀, pow_eq_zero_iff, nat.succ_pos', int.coe_nat_succ, int.coe_nat_zero, zero_add,
-               quadratic_char_zero, add_zero, set.set_of_eq_eq_singleton, set.to_finset_card,
+  { simp only [h₀, pow_eq_zero_iff, nat.succ_pos', int.coe_nat_succ, int.coe_nat_zero,
+               mul_char.map_zero, set.set_of_eq_eq_singleton, set.to_finset_card,
                set.card_singleton], },
   { set s := {x : F | x^2 = a}.to_finset with hs,
     by_cases h : is_square a,
@@ -208,18 +257,7 @@ open_locale big_operators
 
 /-- The sum over the values of the quadratic character is zero when the characteristic is odd. -/
 lemma quadratic_char_sum_zero (hF : ring_char F ≠ 2) : ∑ (a : F), quadratic_char F a = 0 :=
-begin
-  cases (quadratic_char_exists_neg_one hF) with b hb,
-  have h₀ : b ≠ 0 := by
-  { intro hf,
-    rw [hf, quadratic_char_zero, zero_eq_neg] at hb,
-    exact one_ne_zero hb, },
-  have h₁ : ∑ (a : F), quadratic_char F (b * a) = ∑ (a : F), quadratic_char F a :=
-    fintype.sum_bijective _ (mul_left_bijective₀ b h₀) _ _ (λ x, rfl),
-  simp only [quadratic_char_mul] at h₁,
-  rw [← finset.mul_sum, hb, neg_mul, one_mul] at h₁,
-  exact eq_zero_of_neg_eq h₁,
-end
+is_nontrivial.sum_eq_zero (quadratic_char_is_nontrivial hF)
 
 end quadratic_char
 
@@ -243,37 +281,34 @@ variables {F : Type*} [field F] [fintype F]
 lemma quadratic_char_neg_one [decidable_eq F] (hF : ring_char F ≠ 2) :
   quadratic_char F (-1) = χ₄ (fintype.card F) :=
 begin
-  have h₁ : (-1 : F) ≠ 0 := by { rw neg_ne_zero, exact one_ne_zero },
-  have h := quadratic_char_eq_pow_of_char_ne_two hF h₁,
+  have h := quadratic_char_eq_pow_of_char_ne_two hF (neg_ne_zero.mpr one_ne_zero),
   rw [h, χ₄_eq_neg_one_pow (finite_field.odd_card_of_char_ne_two hF)],
   set n := fintype.card F / 2,
   cases (nat.even_or_odd n) with h₂ h₂,
   { simp only [even.neg_one_pow h₂, eq_self_iff_true, if_true], },
   { simp only [odd.neg_one_pow h₂, ite_eq_right_iff],
-    exact λ (hf : -1 = 1),
-            false.rec (1 = -1) (ring.neg_one_ne_one_of_char_ne_two hF hf), },
+    exact λ hf, false.rec (1 = -1) (ring.neg_one_ne_one_of_char_ne_two hF hf), },
 end
 
 /-- The interpretation in terms of whether `-1` is a square in `F` -/
 lemma is_square_neg_one_iff : is_square (-1 : F) ↔ fintype.card F % 4 ≠ 3 :=
 begin
   classical, -- suggested by the linter (instead of `[decidable_eq F]`)
-  by_cases hF : (ring_char F = 2),
+  by_cases hF : ring_char F = 2,
   { simp only [finite_field.is_square_of_char_two hF, ne.def, true_iff],
     exact (λ hf, one_ne_zero ((nat.odd_of_mod_four_eq_three hf).symm.trans
                                 (finite_field.even_card_of_char_two hF)))},
-  { have h₁ : (-1 : F) ≠ 0 := by { rw neg_ne_zero, exact one_ne_zero },
+  { have h₁ : (-1 : F) ≠ 0 := neg_ne_zero.mpr one_ne_zero,
     have h₂ := finite_field.odd_card_of_char_ne_two hF,
     rw [← quadratic_char_one_iff_is_square h₁, quadratic_char_neg_one hF,
         χ₄_nat_eq_if_mod_four, h₂],
-    have h₃ := nat.odd_mod_four_iff.mp h₂,
     simp only [nat.one_ne_zero, if_false, ite_eq_left_iff, ne.def],
     norm_num,
     split,
     { intros h h',
       have t := (of_not_not h).symm.trans h',
       norm_num at t, },
-    exact λ h h', h' ((or_iff_left h).mp h₃), },
+    exact λ h h', h' ((or_iff_left h).mp (nat.odd_mod_four_iff.mp h₂)), },
 end
 
 end char

diff --git a/src/number_theory/legendre_symbol/quadratic_reciprocity.lean b/src/number_theory/legendre_symbol/quadratic_reciprocity.lean
@@ -117,7 +117,7 @@ lemma legendre_sym_eq_pow (p : ℕ) (a : ℤ) [hp : fact p.prime] :
 begin
   rw legendre_sym,
   by_cases ha : (a : zmod p) = 0,
-  { simp only [ha, zero_pow (nat.div_pos (hp.1.two_le) (succ_pos 1)), quadratic_char_zero,
+  { simp only [ha, zero_pow (nat.div_pos (hp.1.two_le) (succ_pos 1)), mul_char.map_zero,
                int.cast_zero], },
   by_cases hp₁ : p = 2,
   { substI p,
@@ -143,13 +143,13 @@ quadratic_char_eq_neg_one_iff_not_one ha
 /-- The Legendre symbol of `p` and `a` is zero iff `p ∣ a`. -/
 lemma legendre_sym_eq_zero_iff (p : ℕ) [fact p.prime] (a : ℤ) :
   legendre_sym p a = 0 ↔ (a : zmod p) = 0 :=
-quadratic_char_eq_zero_iff a
+quadratic_char_eq_zero_iff
 
 @[simp] lemma legendre_sym_zero (p : ℕ) [fact p.prime] : legendre_sym p 0 = 0 :=
-by rw [legendre_sym, int.cast_zero, quadratic_char_zero]
+by rw [legendre_sym, int.cast_zero, mul_char.map_zero]
 
 @[simp] lemma legendre_sym_one (p : ℕ) [fact p.prime] : legendre_sym p 1 = 1 :=
-by rw [legendre_sym, int.cast_one, quadratic_char_one]
+by rw [legendre_sym, int.cast_one, mul_char.map_one]
 
 /-- The Legendre symbol is multiplicative in `a` for `p` fixed. -/
 lemma legendre_sym_mul (p : ℕ) [fact p.prime] (a b : ℤ) :

diff --git a/src/number_theory/legendre_symbol/zmod_char.lean b/src/number_theory/legendre_symbol/zmod_char.lean
@@ -6,12 +6,15 @@ Authors: Michael Stoll
 import tactic.basic
 import data.int.range
 import data.zmod.basic
+import number_theory.legendre_symbol.mul_character
 
 /-!
 # Quadratic characters on ℤ/nℤ
 
 This file defines some quadratic characters on the rings ℤ/4ℤ and ℤ/8ℤ.
 
+We set them up to be of type `mul_char (zmod n) ℤ`, where `n` is `4` or `8`.
+
 ## Tags
 
 quadratic character, zmod
@@ -30,12 +33,12 @@ section quad_char_mod_p
 
 /-- Define the nontrivial quadratic character on `zmod 4`, `χ₄`.
 It corresponds to the extension `ℚ(√-1)/ℚ`. -/
-@[simps] def χ₄ : (zmod 4) →*₀ ℤ :=
+@[simps] def χ₄ : mul_char (zmod 4) ℤ :=
 { to_fun := (![0,1,0,-1] : (zmod 4 → ℤ)),
-  map_zero' := rfl, map_one' := rfl, map_mul' := dec_trivial }
+  map_one' := rfl, map_mul' := dec_trivial, map_nonunit' := dec_trivial }
 
 /-- `χ₄` takes values in `{0, 1, -1}` -/
-lemma χ₄_trichotomy (a : zmod 4) : χ₄ a = 0 ∨ χ₄ a = 1 ∨ χ₄ a = -1 := by dec_trivial!
+lemma is_quadratic_χ₄ : χ₄.is_quadratic := by { intro a, dec_trivial!, }
 
 /-- An explicit description of `χ₄` on integers / naturals -/
 lemma χ₄_int_eq_if_mod_four (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
@@ -66,12 +69,12 @@ end
 
 /-- Define the first primitive quadratic character on `zmod 8`, `χ₈`.
 It corresponds to the extension `ℚ(√2)/ℚ`. -/
-@[simps] def χ₈ : (zmod 8) →*₀ ℤ :=
+@[simps] def χ₈ : mul_char (zmod 8) ℤ :=
 { to_fun := (![0,1,0,-1,0,-1,0,1] : (zmod 8 → ℤ)),
-  map_zero' := rfl, map_one' := rfl, map_mul' := dec_trivial }
+  map_one' := rfl, map_mul' := dec_trivial, map_nonunit' := dec_trivial }
 
 /-- `χ₈` takes values in `{0, 1, -1}` -/
-lemma χ₈_trichotomy (a : zmod 8) : χ₈ a = 0 ∨ χ₈ a = 1 ∨ χ₈ a = -1 := by dec_trivial!
+lemma is_quadratic_χ₈ : χ₈.is_quadratic := by { intro a, dec_trivial!, }
 
 /-- An explicit description of `χ₈` on integers / naturals -/
 lemma χ₈_int_eq_if_mod_eight (n : ℤ) :
@@ -90,12 +93,12 @@ by exact_mod_cast χ₈_int_eq_if_mod_eight n
 
 /-- Define the second primitive quadratic character on `zmod 8`, `χ₈'`.
 It corresponds to the extension `ℚ(√-2)/ℚ`. -/
-@[simps] def χ₈' : (zmod 8) →*₀ ℤ :=
+@[simps] def χ₈' : mul_char (zmod 8) ℤ :=
 { to_fun := (![0,1,0,1,0,-1,0,-1] : (zmod 8 → ℤ)),
-  map_zero' := rfl, map_one' := rfl, map_mul' := dec_trivial }
+  map_one' := rfl, map_mul' := dec_trivial, map_nonunit' := dec_trivial }
 
 /-- `χ₈'` takes values in `{0, 1, -1}` -/
-lemma χ₈'_trichotomy (a : zmod 8) : χ₈' a = 0 ∨ χ₈' a = 1 ∨ χ₈' a = -1 := by dec_trivial!
+lemma is_quadratic_χ₈' : χ₈'.is_quadratic := by { intro a, dec_trivial!, }
 
 /-- An explicit description of `χ₈'` on integers / naturals -/
 lemma χ₈'_int_eq_if_mod_eight (n : ℤ) :