feat(number_theory/legendre_symbol/quadratic_char): add results on sp…

…ecial values (#15888)

This uses the new results on Gauss sums to prove results on the values of quadratic characters at 2, -2 and odd primes.
The next step will be to use these to prove Quadratic Reciprocity and the Second Supplementary Law for Legendre symbols.

[Here](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gauss.20sums/near/292231902) is the Zulip discussion on Gauss sums.

src/number_theory/legendre_symbol/gauss_sum.lean

@@ -252,7 +252,7 @@ in this way, the result is reduced to `card_pow_char_pow`.
 open zmod
 
 /-- For every finite field `F` of odd characteristic, we have `2^(#F/2) = χ₈(#F)` in `F`. -/
-lemma finite_field.two_pow_card {F : Type} [fintype F] [field F] (hF : ring_char F ≠ 2) :
+lemma finite_field.two_pow_card {F : Type*} [fintype F] [field F] (hF : ring_char F ≠ 2) :
   (2 : F) ^ (fintype.card F / 2) = χ₈ (fintype.card F) :=
 begin
   have hp2 : ∀ (n : ℕ), (2 ^ n : F) ≠ 0 := λ n, pow_ne_zero n (ring.two_ne_zero hF),

src/number_theory/legendre_symbol/mul_character.lean

@@ -15,6 +15,18 @@ that sends non-units to zero.
 
 We use the namespace `mul_char` for the definitions and results.
 
+## Main results
+
+We show that the multiplicative characters form a group (if `R'` is commutative);
+see `mul_char.comm_group`. We also provide an equivalence with the
+homomorphisms `Rˣ →* R'ˣ`; see `mul_char.equiv_to_unit_hom`.
+
+We define a multiplicative character to be *quadratic* if its values
+are among `0`, `1` and `-1`, and we prove some properties of quadratic characters.
+
+Finally, we show that the sum of all values of a nontrivial multiplicative
+character vanishes; see `mul_char.is_nontrivial.sum_eq_zero`.
+
 ## Tags
 
 multiplicative character
@@ -221,6 +233,11 @@ lemma map_zero {R : Type u} [comm_monoid_with_zero R] [nontrivial R] (χ : mul_c
   χ (0 : R) = 0 :=
 by rw [map_nonunit χ not_is_unit_zero]
 
+/-- If the domain is a ring `R`, then `χ (ring_char R) = 0`. -/
+lemma map_ring_char {R : Type u} [comm_ring R] [nontrivial R] (χ : mul_char R R') :
+  χ (ring_char R) = 0 :=
+by rw [ring_char.nat.cast_ring_char, χ.map_zero]
+
 noncomputable
 instance has_one : has_one (mul_char R R') := ⟨trivial R R'⟩
 
@@ -266,12 +283,14 @@ lemma inv_apply_eq_inv (χ : mul_char R R') (a : R) :
   χ⁻¹ a = ring.inverse (χ a) :=
 eq.refl $ inv χ a
 
-/-- Variant when the target is a field -/
+/-- The inverse of a multiplicative character `χ`, applied to `a`, is the inverse of `χ a`.
+Variant when the target is a field -/
 lemma inv_apply_eq_inv' {R' : Type v} [field R'] (χ : mul_char R R') (a : R) :
   χ⁻¹ a = (χ a)⁻¹ :=
 (inv_apply_eq_inv χ a).trans $ ring.inverse_eq_inv (χ a)
 
-/-- When the domain has a zero, we can as well take the inverse first. -/
+/-- When the domain has a zero, then the inverse of a multiplicative character `χ`,
+applied to `a`, is `χ` applied to the inverse of `a`. -/
 lemma inv_apply {R : Type u} [comm_monoid_with_zero R] (χ : mul_char R R') (a : R) :
   χ⁻¹ a = χ (ring.inverse a) :=
 begin
@@ -284,7 +303,8 @@ begin
     rw [map_nonunit _ ha, ring.inverse_non_unit a ha, mul_char.map_zero χ], },
 end
 
-/-- When the domain is a field, we can use the field inverse instead. -/
+/-- When the domain has a zero, then the inverse of a multiplicative character `χ`,
+applied to `a`, is `χ` applied to the inverse of `a`. -/
 lemma inv_apply' {R : Type u} [field R] (χ : mul_char R R') (a : R) : χ⁻¹ a = χ a⁻¹ :=
 (inv_apply χ a).trans $ congr_arg _ (ring.inverse_eq_inv a)
 
@@ -297,7 +317,7 @@ begin
       ring.inverse_mul_cancel _ (is_unit.map _ x.is_unit), one_apply_coe],
 end
 
-/-- Finally, the commutative group structure on `mul_char R R'`. -/
+/-- The commutative group structure on `mul_char R R'`. -/
 noncomputable
 instance comm_group : comm_group (mul_char R R') :=
 { one := 1,
@@ -360,6 +380,14 @@ by simp only [is_nontrivial, ne.def, ext_iff, not_forall, one_apply_coe]
 /-- A multiplicative character is *quadratic* if it takes only the values `0`, `1`, `-1`. -/
 def is_quadratic (χ : mul_char R R') : Prop := ∀ a, χ a = 0 ∨ χ a = 1 ∨ χ a = -1
 
+/-- If two values of quadratic characters with target `ℤ` agree after coercion into a ring
+of characteristic not `2`, then they agree in `ℤ`. -/
+lemma is_quadratic.eq_of_eq_coe {χ : mul_char R ℤ} (hχ : is_quadratic χ)
+  {χ' : mul_char R' ℤ} (hχ' : is_quadratic χ') [nontrivial R''] (hR'' : ring_char R'' ≠ 2)
+  {a : R} {a' : R'} (h : (χ a : R'') = χ' a') :
+  χ a = χ' a' :=
+int.cast_inj_on_of_ring_char_ne_two hR'' (hχ a) (hχ' a') h
+
 /-- We can post-compose a multiplicative character with a ring homomorphism. -/
 @[simps]
 def ring_hom_comp (χ : mul_char R R') (f : R' →+* R'') : mul_char R R'' :=

src/number_theory/legendre_symbol/quadratic_char.lean

@@ -5,6 +5,7 @@ Authors: Michael Stoll
 -/
 import number_theory.legendre_symbol.zmod_char
 import field_theory.finite.basic
+import number_theory.legendre_symbol.gauss_sum
 
 /-!
 # Quadratic characters of finite fields
@@ -17,8 +18,6 @@ some basic statements about it.
 quadratic character
 -/
 
-namespace char
-
 /-!
 ### Definition of the quadratic character
 
@@ -80,9 +79,7 @@ lemma quadratic_char_eq_one_of_char_two' (hF : ring_char F = 2) {a : F} (ha : a
   quadratic_char_fun F a = 1 :=
 begin
   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),
+  exact λ h, false.rec _ (h (finite_field.is_square_of_char_two hF a))
 end
 
 /-- If `ring_char F` is odd, then `quadratic_char_fun F a` can be computed in
@@ -159,7 +156,7 @@ lemma quadratic_char_dichotomy {a : F} (ha : a ≠ 0) :
   quadratic_char F a = 1 ∨ quadratic_char F a = -1 :=
 sq_eq_one_iff.1 $ quadratic_char_sq_one ha
 
-/-- A variant -/
+/-- The quadratic character is `1` or `-1` on nonzero arguments. -/
 lemma quadratic_char_eq_neg_one_iff_not_one {a : F} (ha : a ≠ 0) :
   quadratic_char F a = -1 ↔ ¬ quadratic_char F a = 1 :=
 begin
@@ -192,6 +189,20 @@ lemma quadratic_char_eq_pow_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha
   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
 
+lemma quadratic_char_eq_pow_of_char_ne_two'' (hF : ring_char F ≠ 2) (a : F) :
+  (quadratic_char F a : F) = a ^ (fintype.card F / 2) :=
+begin
+  by_cases ha : a = 0,
+  { have : 0 < fintype.card F / 2 := nat.div_pos fintype.one_lt_card two_pos,
+    simp only [ha, zero_pow this, quadratic_char_apply, quadratic_char_zero, int.cast_zero], },
+  { rw [quadratic_char_eq_pow_of_char_ne_two hF ha],
+    by_cases ha' : a ^ (fintype.card F / 2) = 1,
+    { simp only [ha', eq_self_iff_true, if_true, int.cast_one], },
+    { have ha'' := or.resolve_left (finite_field.pow_dichotomy hF ha) ha',
+      simp only [ha'', int.cast_ite, int.cast_one, int.cast_neg, ite_eq_right_iff],
+      exact eq.symm, } }
+end
+
 variables (F)
 
 /-- The quadratic character is quadratic as a multiplicative character. -/
@@ -261,8 +272,6 @@ is_nontrivial.sum_eq_zero (quadratic_char_is_nontrivial hF)
 
 end quadratic_char
 
-end char
-
 /-!
 ### Special values of the quadratic character
 
@@ -271,11 +280,9 @@ We express `quadratic_char F (-1)` in terms of `χ₄`.
 
 section special_values
 
-namespace char
+open zmod mul_char
 
-open zmod
-
-variables {F : Type*} [field F] [fintype F]
+variables {F : Type} [field F] [fintype F]
 
 /-- The value of the quadratic character at `-1` -/
 lemma quadratic_char_neg_one [decidable_eq F] (hF : ring_char F ≠ 2) :
@@ -290,27 +297,136 @@ begin
     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 :=
+/-- `-1` is a square in `F` iff `#F` is not congruent to `3` mod `4`. -/
+lemma finite_field.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,
   { 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 := 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₂],
-    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 (nat.odd_mod_four_iff.mp h₂)), },
+    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₁ := finite_field.odd_card_of_char_ne_two hF,
+    rw [← quadratic_char_one_iff_is_square (neg_ne_zero.mpr (@one_ne_zero F _ _)),
+        quadratic_char_neg_one hF, χ₄_nat_eq_if_mod_four, h₁],
+    simp only [nat.one_ne_zero, if_false, ite_eq_left_iff, ne.def, (dec_trivial : (-1 : ℤ) ≠ 1),
+               imp_false, not_not],
+    exact ⟨λ h, ne_of_eq_of_ne h (dec_trivial : 1 ≠ 3),
+           or.resolve_right (nat.odd_mod_four_iff.mp h₁)⟩, },
+end
+
+/-- The value of the quadratic character at `2` -/
+lemma quadratic_char_two [decidable_eq F] (hF : ring_char F ≠ 2) :
+  quadratic_char F 2 = χ₈ (fintype.card F) :=
+is_quadratic.eq_of_eq_coe (quadratic_char_is_quadratic F) is_quadratic_χ₈ hF
+  ((quadratic_char_eq_pow_of_char_ne_two'' hF 2).trans (finite_field.two_pow_card hF))
+
+/-- `2` is a square in `F` iff `#F` is not congruent to `3` or `5` mod `8`. -/
+lemma finite_field.is_square_two_iff :
+  is_square (2 : F) ↔ fintype.card F % 8 ≠ 3 ∧ fintype.card F % 8 ≠ 5 :=
+begin
+  classical,
+  by_cases hF : ring_char F = 2,
+  focus
+  { have h := finite_field.even_card_of_char_two hF,
+    simp only [finite_field.is_square_of_char_two hF, true_iff], },
+  rotate, focus
+  { have h := finite_field.odd_card_of_char_ne_two hF,
+    rw [← quadratic_char_one_iff_is_square (ring.two_ne_zero hF), quadratic_char_two hF,
+        χ₈_nat_eq_if_mod_eight],
+    simp only [h, nat.one_ne_zero, if_false, ite_eq_left_iff, ne.def, (dec_trivial : (-1 : ℤ) ≠ 1),
+               imp_false, not_not], },
+  all_goals
+  { rw [← nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h,
+    have h₁ := nat.mod_lt (fintype.card F) (dec_trivial : 0 < 8),
+    revert h₁ h,
+    generalize : fintype.card F % 8 = n,
+    dec_trivial!, }
+end
+
+/-- The value of the quadratic character at `-2` -/
+lemma quadratic_char_neg_two [decidable_eq F] (hF : ring_char F ≠ 2) :
+  quadratic_char F (-2) = χ₈' (fintype.card F) :=
+begin
+  rw [(by norm_num : (-2 : F) = (-1) * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadratic_char_neg_one hF,
+      quadratic_char_two hF, @cast_nat_cast _ (zmod 4) _ _ _ (by norm_num : 4 ∣ 8)],
+end
+
+/-- `-2` is a square in `F` iff `#F` is not congruent to `5` or `7` mod `8`. -/
+lemma finite_field.is_square_neg_two_iff :
+  is_square (-2 : F) ↔ fintype.card F % 8 ≠ 5 ∧ fintype.card F % 8 ≠ 7 :=
+begin
+  classical,
+  by_cases hF : ring_char F = 2,
+  focus
+  { have h := finite_field.even_card_of_char_two hF,
+    simp only [finite_field.is_square_of_char_two hF, true_iff], },
+  rotate, focus
+  { have h := finite_field.odd_card_of_char_ne_two hF,
+    rw [← quadratic_char_one_iff_is_square (neg_ne_zero.mpr (ring.two_ne_zero hF)),
+        quadratic_char_neg_two hF, χ₈'_nat_eq_if_mod_eight],
+    simp only [h, nat.one_ne_zero, if_false, ite_eq_left_iff, ne.def, (dec_trivial : (-1 : ℤ) ≠ 1),
+               imp_false, not_not], },
+  all_goals
+  { rw [← nat.mod_mod_of_dvd _ (by norm_num : 2 ∣ 8)] at h,
+    have h₁ := nat.mod_lt (fintype.card F) (dec_trivial : 0 < 8),
+    revert h₁ h,
+    generalize : fintype.card F % 8 = n,
+    dec_trivial! }
+end
+
+/-- The relation between the values of the quadratic character of one field `F` at the
+cardinality of another field `F'` and of the quadratic character of `F'` at the cardinality
+of `F`. -/
+lemma quadratic_char_card_card [decidable_eq F] (hF : ring_char F ≠ 2) {F' : Type} [field F']
+  [fintype F'] [decidable_eq F'] (hF' : ring_char F' ≠ 2) (h : ring_char F' ≠ ring_char F) :
+  quadratic_char F (fintype.card F') = quadratic_char F' (quadratic_char F (-1) * fintype.card F) :=
+begin
+  let χ := (quadratic_char F).ring_hom_comp (algebra_map ℤ F'),
+  have hχ₁ : χ.is_nontrivial,
+  { obtain ⟨a, ha⟩ := quadratic_char_exists_neg_one hF,
+    have hu : is_unit a,
+    { contrapose ha,
+      exact ne_of_eq_of_ne (map_nonunit (quadratic_char F) ha)
+             (mt zero_eq_neg.mp one_ne_zero), },
+    use hu.unit,
+    simp only [is_unit.unit_spec, ring_hom_comp_apply, ring_hom.eq_int_cast, ne.def, ha],
+    rw [int.cast_neg, int.cast_one],
+    exact ring.neg_one_ne_one_of_char_ne_two hF', },
+  have hχ₂ : χ.is_quadratic := is_quadratic.comp (quadratic_char_is_quadratic F) _,
+  have h := char.card_pow_card hχ₁ hχ₂ h hF',
+  rw [← quadratic_char_eq_pow_of_char_ne_two'' hF'] at h,
+  exact (is_quadratic.eq_of_eq_coe (quadratic_char_is_quadratic F')
+             (quadratic_char_is_quadratic F) hF' h).symm,
 end
 
-end char
+/-- The value of the quadratic character at an odd prime `p` different from `ring_char F`. -/
+lemma quadratic_char_odd_prime [decidable_eq F] (hF : ring_char F ≠ 2) {p : ℕ} [fact p.prime]
+  (hp₁ : p ≠ 2) (hp₂ : ring_char F ≠ p) :
+  quadratic_char F p = quadratic_char (zmod p) (χ₄ (fintype.card F) * fintype.card F) :=
+begin
+  rw [← quadratic_char_neg_one hF],
+  have h := quadratic_char_card_card hF (ne_of_eq_of_ne (ring_char_zmod_n p) hp₁)
+              (ne_of_eq_of_ne (ring_char_zmod_n p) hp₂.symm),
+  rwa [card p] at h,
+end
+
+/-- An odd prime `p` is a square in `F` iff the quadratic character of `zmod p` does not
+take the value `-1` on `χ₄(#F) * #F`. -/
+lemma finite_field.is_square_odd_prime_iff (hF : ring_char F ≠ 2) {p : ℕ} [fact p.prime]
+  (hp : p ≠ 2) :
+  is_square (p : F) ↔ quadratic_char (zmod p) (χ₄ (fintype.card F) * fintype.card F) ≠ -1 :=
+begin
+  classical,
+  by_cases hFp : ring_char F = p,
+  { rw [show (p : F) = 0, by { rw ← hFp, exact ring_char.nat.cast_ring_char }],
+    simp only [is_square_zero, ne.def, true_iff, map_mul],
+    obtain ⟨n, _, hc⟩ := finite_field.card F (ring_char F),
+    have hchar : ring_char F = ring_char (zmod p) := by {rw hFp, exact (ring_char_zmod_n p).symm},
+    conv {congr, to_lhs, congr, skip, rw [hc, nat.cast_pow, map_pow, hchar, map_ring_char], },
+    simp only [zero_pow n.pos, mul_zero, zero_eq_neg, one_ne_zero, not_false_iff], },
+  { rw [← iff.not_left (@quadratic_char_neg_one_iff_not_is_square F _ _ _ _),
+        quadratic_char_odd_prime hF hp],
+    exact hFp, },
+end
 
 end special_values

src/number_theory/legendre_symbol/quadratic_reciprocity.lean

@@ -64,7 +64,7 @@ end
 
 lemma exists_sq_eq_neg_one_iff : is_square (-1 : zmod p) ↔ p % 4 ≠ 3 :=
 begin
-  have h := @is_square_neg_one_iff (zmod p) _ _,
+  have h := @finite_field.is_square_neg_one_iff (zmod p) _ _,
   rw card p at h,
   exact h,
 end

src/number_theory/legendre_symbol/zmod_char.lean

@@ -120,13 +120,7 @@ lemma χ₈'_eq_χ₄_mul_χ₈ (a : zmod 8) : χ₈' a = χ₄ a * χ₈ a := b
 
 lemma χ₈'_int_eq_χ₄_mul_χ₈ (a : ℤ) : χ₈' a = χ₄ a * χ₈ a :=
 begin
-  have h : (a : zmod 4) = (a : zmod 8),
-  { have help : ∀ m : ℤ, 0 ≤ m → m < 8 → ((m % 4 : ℤ) : zmod 4) = (m : zmod 8) := dec_trivial,
-    rw [← zmod.int_cast_mod a 8, ← zmod.int_cast_mod a 4,
-        (by norm_cast : ((8 : ℕ) : ℤ) = 8), (by norm_cast : ((4 : ℕ) : ℤ) = 4),
-        ← int.mod_mod_of_dvd a (by norm_num : (4 : ℤ) ∣ 8)],
-    exact help (a % 8) (int.mod_nonneg a (by norm_num)) (int.mod_lt a (by norm_num)), },
-  rw h,
+  rw ← @cast_int_cast 8 (zmod 4) _ 4 _ (by norm_num) a,
   exact χ₈'_eq_χ₄_mul_χ₈ a,
 end