chore(number_theory/legendre_symbol/quadratic_reciprocity): split som…

…e files (#19193)

The best split here is separating `quadratic_reciprocity` into that and `legendre_symbol`.

I was looking at this because the olean analyser in the port-progress-bot made an unlikely claim about unnecessary dependencies, and I wanted to make sure we weren't missing something in doubting it. We weren't. :-)



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

src/number_theory/legendre_symbol/basic.lean

@@ -0,0 +1,298 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Michael Stoll
+-/
+import number_theory.legendre_symbol.quadratic_char.basic
+
+/-!
+# Legendre symbol
+
+This file contains results about Legendre symbols.
+
+We define the Legendre symbol $\Bigl(\frac{a}{p}\Bigr)$ as `legendre_sym p a`.
+Note the order of arguments! The advantage of this form is that then `legendre_sym p`
+is a multiplicative map.
+
+The Legendre symbol is used to define the Jacobi symbol, `jacobi_sym a b`, for integers `a`
+and (odd) natural numbers `b`, which extends the Legendre symbol.
+
+## Main results
+
+We also prove the supplementary laws that give conditions for when `-1`
+is a square modulo a prime `p`:
+`legendre_sym.at_neg_one` and `zmod.exists_sq_eq_neg_one_iff` for `-1`.
+
+See `number_theory.legendre_symbol.quadratic_reciprocity` for the conditions when `2` and `-2`
+are squares:
+`legendre_sym.at_two` and `zmod.exists_sq_eq_two_iff` for `2`,
+`legendre_sym.at_neg_two` and `zmod.exists_sq_eq_neg_two_iff` for `-2`.
+
+## Tags
+
+quadratic residue, quadratic nonresidue, Legendre symbol
+-/
+
+open nat
+
+section euler
+
+namespace zmod
+
+variables (p : ℕ) [fact p.prime]
+
+/-- Euler's Criterion: A unit `x` of `zmod p` is a square if and only if `x ^ (p / 2) = 1`. -/
+lemma euler_criterion_units (x : (zmod p)ˣ) : (∃ y : (zmod p)ˣ, y ^ 2 = x) ↔ x ^ (p / 2) = 1 :=
+begin
+  by_cases hc : p = 2,
+  { substI hc,
+    simp only [eq_iff_true_of_subsingleton, exists_const], },
+  { have h₀ := finite_field.unit_is_square_iff (by rwa ring_char_zmod_n) x,
+    have hs : (∃ y : (zmod p)ˣ, y ^ 2 = x) ↔ is_square(x) :=
+    by { rw is_square_iff_exists_sq x,
+         simp_rw eq_comm, },
+    rw hs,
+    rwa card p at h₀, },
+end
+
+/-- Euler's Criterion: a nonzero `a : zmod p` is a square if and only if `x ^ (p / 2) = 1`. -/
+lemma euler_criterion {a : zmod p} (ha : a ≠ 0) : is_square (a : zmod p) ↔ a ^ (p / 2) = 1 :=
+begin
+  apply (iff_congr _ (by simp [units.ext_iff])).mp (euler_criterion_units p (units.mk0 a ha)),
+  simp only [units.ext_iff, sq, units.coe_mk0, units.coe_mul],
+  split, { rintro ⟨y, hy⟩, exact ⟨y, hy.symm⟩ },
+  { rintro ⟨y, rfl⟩,
+    have hy : y ≠ 0, { rintro rfl, simpa [zero_pow] using ha, },
+    refine ⟨units.mk0 y hy, _⟩, simp, }
+end
+
+/-- If `a : zmod p` is nonzero, then `a^(p/2)` is either `1` or `-1`. -/
+lemma pow_div_two_eq_neg_one_or_one {a : zmod p} (ha : a ≠ 0) :
+  a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1 :=
+begin
+  cases prime.eq_two_or_odd (fact.out p.prime) with hp2 hp_odd,
+  { substI p, revert a ha, dec_trivial },
+  rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd],
+  exact pow_card_sub_one_eq_one ha
+end
+
+end zmod
+
+end euler
+
+section legendre
+
+/-!
+### Definition of the Legendre symbol and basic properties
+-/
+
+open zmod
+
+variables (p : ℕ) [fact p.prime]
+
+/-- The Legendre symbol of `a : ℤ` and a prime `p`, `legendre_sym p a`,
+is an integer defined as
+
+* `0` if `a` is `0` modulo `p`;
+* `1` if `a` is a nonzero square modulo `p`
+* `-1` otherwise.
+
+Note the order of the arguments! The advantage of the order chosen here is
+that `legendre_sym p` is a multiplicative function `ℤ → ℤ`.
+-/
+def legendre_sym (a : ℤ) : ℤ := quadratic_char (zmod p) a
+
+namespace legendre_sym
+
+/-- We have the congruence `legendre_sym p a ≡ a ^ (p / 2) mod p`. -/
+lemma eq_pow (a : ℤ) : (legendre_sym p a : zmod p) = a ^ (p / 2) :=
+begin
+  cases eq_or_ne (ring_char (zmod p)) 2 with hc hc,
+  { by_cases ha : (a : zmod p) = 0,
+    { rw [legendre_sym, ha, quadratic_char_zero,
+          zero_pow (nat.div_pos (fact.out p.prime).two_le (succ_pos 1))],
+      norm_cast, },
+    { have := (ring_char_zmod_n p).symm.trans hc, -- p = 2
+      substI p,
+      rw [legendre_sym, quadratic_char_eq_one_of_char_two hc ha],
+      revert ha,
+      generalize : (a : zmod 2) = b, revert b, dec_trivial } },
+  { convert quadratic_char_eq_pow_of_char_ne_two' hc (a : zmod p),
+    exact (card p).symm },
+end
+
+/-- If `p ∤ a`, then `legendre_sym p a` is `1` or `-1`. -/
+lemma eq_one_or_neg_one {a : ℤ} (ha : (a : zmod p) ≠ 0) :
+  legendre_sym p a = 1 ∨ legendre_sym p a = -1 :=
+quadratic_char_dichotomy ha
+
+lemma eq_neg_one_iff_not_one {a : ℤ} (ha : (a : zmod p) ≠ 0) :
+  legendre_sym p a = -1 ↔ ¬ legendre_sym p a = 1 :=
+quadratic_char_eq_neg_one_iff_not_one ha
+
+/-- The Legendre symbol of `p` and `a` is zero iff `p ∣ a`. -/
+lemma eq_zero_iff (a : ℤ) : legendre_sym p a = 0 ↔ (a : zmod p) = 0 :=
+quadratic_char_eq_zero_iff
+
+@[simp] lemma at_zero : legendre_sym p 0 = 0 :=
+by rw [legendre_sym, int.cast_zero, mul_char.map_zero]
+
+@[simp] lemma at_one : legendre_sym p 1 = 1 :=
+by rw [legendre_sym, int.cast_one, mul_char.map_one]
+
+/-- The Legendre symbol is multiplicative in `a` for `p` fixed. -/
+protected
+lemma mul (a b : ℤ) : legendre_sym p (a * b) = legendre_sym p a * legendre_sym p b :=
+by simp only [legendre_sym, int.cast_mul, map_mul]
+
+/-- The Legendre symbol is a homomorphism of monoids with zero. -/
+@[simps] def hom : ℤ →*₀ ℤ :=
+{ to_fun := legendre_sym p,
+  map_zero' := at_zero p,
+  map_one' := at_one p,
+  map_mul' := legendre_sym.mul p }
+
+/-- The square of the symbol is 1 if `p ∤ a`. -/
+theorem sq_one {a : ℤ} (ha : (a : zmod p) ≠ 0) : (legendre_sym p a) ^ 2 = 1 :=
+quadratic_char_sq_one ha
+
+/-- The Legendre symbol of `a^2` at `p` is 1 if `p ∤ a`. -/
+theorem sq_one' {a : ℤ} (ha : (a : zmod p) ≠ 0) : legendre_sym p (a ^ 2) = 1 :=
+by exact_mod_cast quadratic_char_sq_one' ha
+
+/-- The Legendre symbol depends only on `a` mod `p`. -/
+protected
+theorem mod (a : ℤ) : legendre_sym p a = legendre_sym p (a % p) :=
+by simp only [legendre_sym, int_cast_mod]
+
+/-- When `p ∤ a`, then `legendre_sym p a = 1` iff `a` is a square mod `p`. -/
+lemma eq_one_iff {a : ℤ} (ha0 : (a : zmod p) ≠ 0) :
+  legendre_sym p a = 1 ↔ is_square (a : zmod p) :=
+quadratic_char_one_iff_is_square ha0
+
+lemma eq_one_iff' {a : ℕ} (ha0 : (a : zmod p) ≠ 0) :
+  legendre_sym p a = 1 ↔ is_square (a : zmod p) :=
+by {rw eq_one_iff, norm_cast, exact_mod_cast ha0}
+
+/-- `legendre_sym p a = -1` iff `a` is a nonsquare mod `p`. -/
+lemma eq_neg_one_iff {a : ℤ} : legendre_sym p a = -1 ↔ ¬ is_square (a : zmod p) :=
+quadratic_char_neg_one_iff_not_is_square
+
+lemma eq_neg_one_iff' {a : ℕ} : legendre_sym p a = -1 ↔ ¬ is_square (a : zmod p) :=
+by {rw eq_neg_one_iff, norm_cast}
+
+/-- The number of square roots of `a` modulo `p` is determined by the Legendre symbol. -/
+lemma card_sqrts (hp : p ≠ 2) (a : ℤ) :
+  ↑{x : zmod p | x^2 = a}.to_finset.card = legendre_sym p a + 1 :=
+quadratic_char_card_sqrts ((ring_char_zmod_n p).substr hp) a
+
+end legendre_sym
+
+end legendre
+
+section quadratic_form
+
+/-!
+### Applications to binary quadratic forms
+-/
+
+namespace legendre_sym
+
+/-- The Legendre symbol `legendre_sym p a = 1` if there is a solution in `ℤ/pℤ`
+of the equation `x^2 - a*y^2 = 0` with `y ≠ 0`. -/
+lemma eq_one_of_sq_sub_mul_sq_eq_zero {p : ℕ} [fact p.prime]
+  {a : ℤ} (ha : (a : zmod p) ≠ 0) {x y : zmod p} (hy : y ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) :
+  legendre_sym p a = 1 :=
+begin
+  apply_fun (* y⁻¹ ^ 2) at hxy,
+  simp only [zero_mul] at hxy,
+  rw [(by ring : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - a * (y * y⁻¹) ^ 2),
+      mul_inv_cancel hy, one_pow, mul_one, sub_eq_zero, pow_two] at hxy,
+  exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩,
+end
+
+/-- The Legendre symbol `legendre_sym p a = 1` if there is a solution in `ℤ/pℤ`
+of the equation `x^2 - a*y^2 = 0` with `x ≠ 0`. -/
+lemma eq_one_of_sq_sub_mul_sq_eq_zero' {p : ℕ} [fact p.prime]
+  {a : ℤ} (ha : (a : zmod p) ≠ 0) {x y : zmod p} (hx : x ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) :
+  legendre_sym p a = 1 :=
+begin
+  have hy : y ≠ 0,
+  { rintro rfl,
+    rw [zero_pow' 2 (by norm_num), mul_zero, sub_zero, pow_eq_zero_iff (by norm_num : 0 < 2)]
+      at hxy,
+    exacts [hx hxy, infer_instance], }, -- why is the instance not inferred automatically?
+  exact eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy,
+end
+
+/-- If `legendre_sym p a = -1`, then the only solution of `x^2 - a*y^2 = 0` in `ℤ/pℤ`
+is the trivial one. -/
+lemma eq_zero_mod_of_eq_neg_one {p : ℕ} [fact p.prime] {a : ℤ}
+  (h : legendre_sym p a = -1) {x y : zmod p} (hxy : x ^ 2 - a * y ^ 2 = 0) : x = 0 ∧ y = 0 :=
+begin
+  have ha : (a : zmod p) ≠ 0,
+  { intro hf,
+    rw (eq_zero_iff p a).mpr hf at h,
+    exact int.zero_ne_neg_of_ne zero_ne_one h, },
+  by_contra hf,
+  cases not_and_distrib.mp hf with hx hy,
+  { rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, eq_neg_self_iff] at h,
+    exact one_ne_zero h, },
+  { rw [eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy, eq_neg_self_iff] at h,
+    exact one_ne_zero h, }
+end
+
+/-- If `legendre_sym p a = -1` and `p` divides `x^2 - a*y^2`, then `p` must divide `x` and `y`. -/
+lemma prime_dvd_of_eq_neg_one {p : ℕ} [fact p.prime] {a : ℤ}
+  (h : legendre_sym p a = -1) {x y : ℤ} (hxy : ↑p ∣ x ^ 2 - a * y ^ 2) : ↑p ∣ x ∧ ↑p ∣ y :=
+begin
+  simp_rw ← zmod.int_coe_zmod_eq_zero_iff_dvd at hxy ⊢,
+  push_cast at hxy,
+  exact eq_zero_mod_of_eq_neg_one h hxy,
+end
+
+end legendre_sym
+
+end quadratic_form
+
+section values
+
+/-!
+### The value of the Legendre symbol at `-1`
+
+See `jacobi_sym.at_neg_one` for the corresponding statement for the Jacobi symbol.
+-/
+
+variables {p : ℕ} [fact p.prime]
+
+open zmod
+
+/-- `legendre_sym p (-1)` is given by `χ₄ p`. -/
+lemma legendre_sym.at_neg_one (hp : p ≠ 2) : legendre_sym p (-1) = χ₄ p :=
+by simp only [legendre_sym, card p, quadratic_char_neg_one ((ring_char_zmod_n p).substr hp),
+              int.cast_neg, int.cast_one]
+
+namespace zmod
+
+/-- `-1` is a square in `zmod p` iff `p` is not congruent to `3` mod `4`. -/
+lemma exists_sq_eq_neg_one_iff : is_square (-1 : zmod p) ↔ p % 4 ≠ 3 :=
+by rw [finite_field.is_square_neg_one_iff, card p]
+
+lemma mod_four_ne_three_of_sq_eq_neg_one {y : zmod p} (hy : y ^ 2 = -1) : p % 4 ≠ 3 :=
+exists_sq_eq_neg_one_iff.1 ⟨y, hy ▸ pow_two y⟩
+
+/-- If two nonzero squares are negatives of each other in `zmod p`, then `p % 4 ≠ 3`. -/
+lemma mod_four_ne_three_of_sq_eq_neg_sq' {x y : zmod p} (hy : y ≠ 0) (hxy : x ^ 2 = - y ^ 2) :
+  p % 4 ≠ 3 :=
+@mod_four_ne_three_of_sq_eq_neg_one p _ (x / y) begin
+  apply_fun (λ z, z / y ^ 2) at hxy,
+  rwa [neg_div, ←div_pow, ←div_pow, div_self hy, one_pow] at hxy
+end
+
+lemma mod_four_ne_three_of_sq_eq_neg_sq {x y : zmod p} (hx : x ≠ 0) (hxy : x ^ 2 = - y ^ 2) :
+  p % 4 ≠ 3 :=
+mod_four_ne_three_of_sq_eq_neg_sq' hx (neg_eq_iff_eq_neg.mpr hxy).symm
+
+end zmod
+
+end values