This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 298
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(number_theory/legendre_symbol/jacobi_symbol): add new file with …
…the definition and properties of the Jacobi symbol (#16395) This PR consists of a new file, `number_theory.legendre_symbol.jacobi_symbol`, that contains a definition of the Jacobi symbol (and sets up notation `[a | b]ⱼ` for it) and then proves a number of results, e.g., multiplicativity in both arguments, expressions for the cases `a = -1`, `a = 2`, `a = -2`, and several versions of quadratic reciprocity. It also proves that the symbol depends on a only through its residue class `mod b` and that it depends on `b` only through its residue class `mod 4*a` (quadratic reciprocity is needed for the latter). The code has already been quite thoroughly reviewed while it was part of #16290 (which then was reduced to the auxiliary results needed for the Jacobi symbol code). Discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984)
- Loading branch information
1 parent
662786a
commit d2d6652
Showing
1 changed file
with
385 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,385 @@ | ||
/- | ||
Copyright (c) 2022 Michael Stoll. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Michael Stoll | ||
-/ | ||
import number_theory.legendre_symbol.quadratic_reciprocity | ||
import data.zmod.coprime | ||
|
||
/-! | ||
# The Jacobi Symbol | ||
We define the Jacobi symbol and prove its main properties. | ||
## Main definitions | ||
We define the Jacobi symbol, `jacobi_sym a b`, for integers `a` and natural numbers `b` | ||
as the product over the prime factors `p` of `b` of the Legendre symbols `zmod.legendre_sym p a`. | ||
This agrees with the mathematical definition when `b` is odd. | ||
The prime factors are obtained via `nat.factors`. Since `nat.factors 0 = []`, | ||
this implies in particular that `jacobi_sym a 0 = 1` for all `a`. | ||
## Main statements | ||
We prove the main properties of the Jacobi symbol, including the following. | ||
* Multiplicativity in both arguments (`jacobi_sym_mul_left`, `jacobi_sym_mul_right`) | ||
* The value of the symbol is `1` or `-1` when the arguments are coprime | ||
(`jacobi_sym_eq_one_or_neg_one`) | ||
* The symbol vanishes if and only if `b ≠ 0` and the arguments are not coprime | ||
(`jacobi_sym_eq_zero_iff`) | ||
* If the symbol has the value `-1`, then `a : zmod b` is not a square | ||
(`nonsquare_of_jacobi_sym_eq_neg_one`); the converse holds when `b = p` is a prime | ||
(`nonsquare_iff_jacobi_sym_eq_neg_one`); in particular, in this case `a` is a | ||
square mod `p` when the symbol has the value `1` (`is_square_of_jacobi_sym_eq_one`). | ||
* Quadratic reciprocity (`jacobi_sym_quadratic_reciprocity`, | ||
`jacobi_sym_quadratic_reciprocity_one_mod_four`, | ||
`jacobi_sym_quadratic_reciprocity_three_mod_four`) | ||
* The supplementary laws for `a = -1`, `a = 2`, `a = -2` (`jacobi_sym_neg_one`, `jacobi_sym_two`, | ||
`jacobi_sym_neg_two`) | ||
* The symbol depends on `a` only via its residue class mod `b` (`jacobi_sym_mod_left`) | ||
and on `b` only via its residue class mod `4*a` (`jacobi_sym_mod_right`) | ||
## Notations | ||
We define the notation `J(a | b)` for `jacobi_sym a b`, localized to `number_theory_symbols`. | ||
## Tags | ||
Jacobi symbol, quadratic reciprocity | ||
-/ | ||
|
||
section jacobi | ||
|
||
/-! | ||
### Definition of the Jacobi symbol | ||
We define the Jacobi symbol $\Bigl\frac{a}{b}\Bigr$ for integers `a` and natural numbers `b` as the | ||
product of the Legendre symbols $\Bigl\frac{a}{p}\Bigr$, where `p` runs through the prime divisors | ||
(with multiplicity) of `b`, as provided by `b.factors`. This agrees with the Jacobi symbol | ||
when `b` is odd and gives less meaningful values when it is not (e.g., the symbol is `1` | ||
when `b = 0`). This is called `jacobi_sym a b`. | ||
We define localized notation (locale `number_theory_symbols`) `J(a | b)` for the Jacobi | ||
symbol `jacobi_sym a b`. (Unfortunately, there is no subscript "J" in unicode.) | ||
-/ | ||
|
||
namespace zmod | ||
open nat | ||
|
||
/-- The Jacobi symbol of `a` and `b` -/ | ||
-- Since we need the fact that the factors are prime, we use `list.pmap`. | ||
def jacobi_sym (a : ℤ) (b : ℕ) : ℤ := | ||
(b.factors.pmap (λ p pp, @legendre_sym p ⟨pp⟩ a) (λ p pf, prime_of_mem_factors pf)).prod | ||
|
||
-- Notation for the Jacobi symbol. | ||
localized "notation `J(` a ` | ` b `)` := jacobi_sym a b" in number_theory_symbols | ||
|
||
/-! | ||
### Properties of the Jacobi symbol | ||
-/ | ||
|
||
/-- The symbol `J(a | 0)` has the value `1`. -/ | ||
@[simp] lemma jacobi_sym_zero_right (a : ℤ) : J(a | 0) = 1 := | ||
by simp only [jacobi_sym, factors_zero, list.prod_nil, list.pmap] | ||
|
||
/-- The symbol `J(a | 1)` has the value `1`. -/ | ||
@[simp] lemma jacobi_sym_one_right (a : ℤ) : J(a | 1) = 1 := | ||
by simp only [jacobi_sym, factors_one, list.prod_nil, list.pmap] | ||
|
||
/-- The Legendre symbol `legendre_sym p a` with an integer `a` and a prime number `p` | ||
is the same as the Jacobi symbol `J(a | p)`. -/ | ||
lemma legendre_sym.to_jacobi_sym {p : ℕ} [fp : fact p.prime] {a : ℤ} : | ||
legendre_sym p a = J(a | p) := | ||
by simp only [jacobi_sym, factors_prime fp.1, list.prod_cons, list.prod_nil, mul_one, list.pmap] | ||
|
||
/-- The Jacobi symbol is multiplicative in its second argument. -/ | ||
lemma jacobi_sym_mul_right' (a : ℤ) {b₁ b₂ : ℕ} (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) : | ||
J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂) := | ||
begin | ||
rw [jacobi_sym, ((perm_factors_mul hb₁ hb₂).pmap _).prod_eq, list.pmap_append, list.prod_append], | ||
exacts [rfl, λ p hp, (list.mem_append.mp hp).elim prime_of_mem_factors prime_of_mem_factors], | ||
end | ||
|
||
/-- The Jacobi symbol is multiplicative in its second argument. -/ | ||
lemma jacobi_sym_mul_right (a : ℤ) (b₁ b₂ : ℕ) [ne_zero b₁] [ne_zero b₂] : | ||
J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂) := | ||
jacobi_sym_mul_right' a (ne_zero.ne b₁) (ne_zero.ne b₂) | ||
|
||
/-- The Jacobi symbol takes only the values `0`, `1` and `-1`. -/ | ||
lemma jacobi_sym_trichotomy (a : ℤ) (b : ℕ) : J(a | b) = 0 ∨ J(a | b) = 1 ∨ J(a | b) = -1 := | ||
((@sign_type.cast_hom ℤ _ _).to_monoid_hom.mrange.copy {0, 1, -1} $ | ||
by {rw set.pair_comm, exact (sign_type.range_eq sign_type.cast_hom).symm}).list_prod_mem | ||
begin | ||
intros _ ha', | ||
rcases list.mem_pmap.mp ha' with ⟨p, hp, rfl⟩, | ||
haveI : fact p.prime := ⟨prime_of_mem_factors hp⟩, | ||
exact quadratic_char_is_quadratic (zmod p) a, | ||
end | ||
|
||
/-- The symbol `J(1 | b)` has the value `1`. -/ | ||
@[simp] lemma jacobi_sym_one_left (b : ℕ) : J(1 | b) = 1 := | ||
list.prod_eq_one (λ z hz, let ⟨p, hp, he⟩ := list.mem_pmap.1 hz in by rw [← he, legendre_sym_one]) | ||
|
||
/-- The Jacobi symbol is multiplicative in its first argument. -/ | ||
lemma jacobi_sym_mul_left (a₁ a₂ : ℤ) (b : ℕ) : J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b) := | ||
by { simp_rw [jacobi_sym, list.pmap_eq_map_attach, legendre_sym_mul], exact list.prod_map_mul } | ||
|
||
/-- The symbol `J(a | b)` vanishes iff `a` and `b` are not coprime (assuming `b ≠ 0`). -/ | ||
lemma jacobi_sym_eq_zero_iff_not_coprime {a : ℤ} {b : ℕ} [ne_zero b] : | ||
J(a | b) = 0 ↔ a.gcd b ≠ 1 := | ||
list.prod_eq_zero_iff.trans begin | ||
rw [list.mem_pmap, int.gcd_eq_nat_abs, ne, prime.not_coprime_iff_dvd], | ||
simp_rw [legendre_sym_eq_zero_iff, int_coe_zmod_eq_zero_iff_dvd, mem_factors (ne_zero.ne b), | ||
← int.coe_nat_dvd_left, int.coe_nat_dvd, exists_prop, and_assoc, and_comm], | ||
end | ||
|
||
/-- The symbol `J(a | b)` is nonzero when `a` and `b` are coprime. -/ | ||
lemma jacobi_sym_ne_zero {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a | b) ≠ 0 := | ||
begin | ||
casesI eq_zero_or_ne_zero b with hb, | ||
{ rw [hb, jacobi_sym_zero_right], | ||
exact one_ne_zero }, | ||
{ contrapose! h, exact jacobi_sym_eq_zero_iff_not_coprime.1 h }, | ||
end | ||
|
||
/-- The symbol `J(a | b)` vanishes if and only if `b ≠ 0` and `a` and `b` are not coprime. -/ | ||
lemma jacobi_sym_eq_zero_iff {a : ℤ} {b : ℕ} : J(a | b) = 0 ↔ b ≠ 0 ∧ a.gcd b ≠ 1 := | ||
⟨λ h, begin | ||
casesI eq_or_ne b 0 with hb hb, | ||
{ rw [hb, jacobi_sym_zero_right] at h, cases h }, | ||
exact ⟨hb, mt jacobi_sym_ne_zero $ not_not.2 h⟩, | ||
end, λ ⟨hb, h⟩, by { rw ← ne_zero_iff at hb, exactI jacobi_sym_eq_zero_iff_not_coprime.2 h }⟩ | ||
|
||
/-- The symbol `J(0 | b)` vanishes when `b > 1`. -/ | ||
lemma jacobi_sym_zero_left {b : ℕ} (hb : 1 < b) : J(0 | b) = 0 := | ||
(@jacobi_sym_eq_zero_iff_not_coprime 0 b ⟨ne_zero_of_lt hb⟩).mpr $ | ||
by { rw [int.gcd_zero_left, int.nat_abs_of_nat], exact hb.ne' } | ||
|
||
/-- The symbol `J(a | b)` takes the value `1` or `-1` if `a` and `b` are coprime. -/ | ||
lemma jacobi_sym_eq_one_or_neg_one {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : | ||
J(a | b) = 1 ∨ J(a | b) = -1 := | ||
(jacobi_sym_trichotomy a b).resolve_left $ jacobi_sym_ne_zero h | ||
|
||
/-- We have that `J(a^e | b) = J(a | b)^e`. -/ | ||
lemma jacobi_sym_pow_left (a : ℤ) (e b : ℕ) : J(a ^ e | b) = J(a | b) ^ e := | ||
nat.rec_on e (by rw [pow_zero, pow_zero, jacobi_sym_one_left]) $ | ||
λ _ ih, by rw [pow_succ, pow_succ, jacobi_sym_mul_left, ih] | ||
|
||
/-- We have that `J(a | b^e) = J(a | b)^e`. -/ | ||
lemma jacobi_sym_pow_right (a : ℤ) (b e : ℕ) : J(a | b ^ e) = J(a | b) ^ e := | ||
begin | ||
induction e with e ih, | ||
{ rw [pow_zero, pow_zero, jacobi_sym_one_right], }, | ||
{ casesI eq_zero_or_ne_zero b with hb, | ||
{ rw [hb, zero_pow (succ_pos e), jacobi_sym_zero_right, one_pow], }, | ||
{ rw [pow_succ, pow_succ, jacobi_sym_mul_right, ih], } } | ||
end | ||
|
||
/-- The square of `J(a | b)` is `1` when `a` and `b` are coprime. -/ | ||
lemma jacobi_sym_sq_one {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a | b) ^ 2 = 1 := | ||
by cases jacobi_sym_eq_one_or_neg_one h with h₁ h₁; rw h₁; refl | ||
|
||
/-- The symbol `J(a^2 | b)` is `1` when `a` and `b` are coprime. -/ | ||
lemma jacobi_sym_sq_one' {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a ^ 2 | b) = 1 := | ||
by rw [jacobi_sym_pow_left, jacobi_sym_sq_one h] | ||
|
||
/-- The symbol `J(a | b)` depends only on `a` mod `b`. -/ | ||
lemma jacobi_sym_mod_left (a : ℤ) (b : ℕ) : J(a | b) = J(a % b | b) := | ||
congr_arg list.prod $ list.pmap_congr _ begin | ||
rintro p hp _ _, | ||
conv_rhs { rw [legendre_sym_mod, int.mod_mod_of_dvd _ | ||
(int.coe_nat_dvd.2 $ dvd_of_mem_factors hp), ← legendre_sym_mod] }, | ||
end | ||
|
||
/-- The symbol `J(a | b)` depends only on `a` mod `b`. -/ | ||
lemma jacobi_sym_mod_left' {a₁ a₂ : ℤ} {b : ℕ} (h : a₁ % b = a₂ % b) : J(a₁ | b) = J(a₂ | b) := | ||
by rw [jacobi_sym_mod_left, h, ← jacobi_sym_mod_left] | ||
|
||
/-- If `J(a | b)` is `-1`, then `a` is not a square modulo `b`. -/ | ||
lemma nonsquare_of_jacobi_sym_eq_neg_one {a : ℤ} {b : ℕ} (h : J(a | b) = -1) : | ||
¬ is_square (a : zmod b) := | ||
λ ⟨r, ha⟩, begin | ||
rw [← r.coe_val_min_abs, ← int.cast_mul, int_coe_eq_int_coe_iff', ← sq] at ha, | ||
apply (by norm_num : ¬ (0 : ℤ) ≤ -1), | ||
rw [← h, jacobi_sym_mod_left, ha, ← jacobi_sym_mod_left, jacobi_sym_pow_left], | ||
apply sq_nonneg, | ||
end | ||
|
||
/-- If `p` is prime, then `J(a | p)` is `-1` iff `a` is not a square modulo `p`. -/ | ||
lemma nonsquare_iff_jacobi_sym_eq_neg_one {a : ℤ} {p : ℕ} [fact p.prime] : | ||
J(a | p) = -1 ↔ ¬ is_square (a : zmod p) := | ||
by { rw [← legendre_sym.to_jacobi_sym], exact legendre_sym_eq_neg_one_iff p } | ||
|
||
/-- If `p` is prime and `J(a | p) = 1`, then `a` is q square mod `p`. -/ | ||
lemma is_square_of_jacobi_sym_eq_one {a : ℤ} {p : ℕ} [fact p.prime] (h : J(a | p) = 1) : | ||
is_square (a : zmod p) := | ||
not_not.mp $ mt nonsquare_iff_jacobi_sym_eq_neg_one.mpr $ | ||
λ hf, one_ne_zero $ neg_eq_self_iff.mp $ hf.symm.trans h | ||
|
||
/-! | ||
### Values at `-1`, `2` and `-2` | ||
-/ | ||
|
||
/-- If `χ` is a multiplicative function such that `J(a | p) = χ p` for all odd primes `p`, | ||
then `J(a | b)` equals `χ b` for all odd natural numbers `b`. -/ | ||
lemma jacobi_sym_value (a : ℤ) {R : Type*} [comm_semiring R] (χ : R →* ℤ) | ||
(hp : ∀ (p : ℕ) (pp : p.prime) (h2 : p ≠ 2), @legendre_sym p ⟨pp⟩ a = χ p) {b : ℕ} (hb : odd b) : | ||
J(a | b) = χ b := | ||
begin | ||
conv_rhs { rw [← prod_factors hb.pos.ne', cast_list_prod, χ.map_list_prod] }, | ||
rw [jacobi_sym, list.map_map, ← list.pmap_eq_map nat.prime _ _ (λ _, prime_of_mem_factors)], | ||
congr' 1, apply list.pmap_congr, | ||
exact λ p h pp _, hp p pp (hb.factors_ne_two h), | ||
end | ||
|
||
/-- If `b` is odd, then `J(-1 | b)` is given by `χ₄ b`. -/ | ||
lemma jacobi_sym_neg_one {b : ℕ} (hb : odd b) : J(-1 | b) = χ₄ b := | ||
jacobi_sym_value (-1) χ₄ (λ p pp, @legendre_sym_neg_one p ⟨pp⟩) hb | ||
|
||
/-- If `b` is odd, then `J(-a | b) = χ₄ b * J(a | b)`. -/ | ||
lemma jacobi_sym_neg (a : ℤ) {b : ℕ} (hb : odd b) : J(-a | b) = χ₄ b * J(a | b) := | ||
by rw [neg_eq_neg_one_mul, jacobi_sym_mul_left, jacobi_sym_neg_one hb] | ||
|
||
/-- If `b` is odd, then `J(2 | b)` is given by `χ₈ b`. -/ | ||
lemma jacobi_sym_two {b : ℕ} (hb : odd b) : J(2 | b) = χ₈ b := | ||
jacobi_sym_value 2 χ₈ (λ p pp, @legendre_sym_two p ⟨pp⟩) hb | ||
|
||
/-- If `b` is odd, then `J(-2 | b)` is given by `χ₈' b`. -/ | ||
lemma jacobi_sym_neg_two {b : ℕ} (hb : odd b) : J(-2 | b) = χ₈' b := | ||
jacobi_sym_value (-2) χ₈' (λ p pp, @legendre_sym_neg_two p ⟨pp⟩) hb | ||
|
||
|
||
/-! | ||
### Quadratic Reciprocity | ||
-/ | ||
|
||
/-- The bi-multiplicative map giving the sign in the Law of Quadratic Reciprocity -/ | ||
def qr_sign (m n : ℕ) : ℤ := J(χ₄ m | n) | ||
|
||
/-- We can express `qr_sign m n` as a power of `-1` when `m` and `n` are odd. -/ | ||
lemma qr_sign_neg_one_pow {m n : ℕ} (hm : odd m) (hn : odd n) : | ||
qr_sign m n = (-1) ^ ((m / 2) * (n / 2)) := | ||
begin | ||
rw [qr_sign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)], | ||
cases odd_mod_four_iff.mp (odd_iff.mp hm) with h h, | ||
{ rw [χ₄_nat_one_mod_four h, jacobi_sym_one_left, one_pow], }, | ||
{ rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobi_sym_neg_one hn], } | ||
end | ||
|
||
/-- When `m` and `n` are odd, then the square of `qr_sign m n` is `1`. -/ | ||
lemma qr_sign_sq_eq_one {m n : ℕ} (hm : odd m) (hn : odd n) : (qr_sign m n) ^ 2 = 1 := | ||
by rw [qr_sign_neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow] | ||
|
||
/-- `qr_sign` is multiplicative in the first argument. -/ | ||
lemma qr_sign_mul_left (m₁ m₂ n : ℕ) : qr_sign (m₁ * m₂) n = qr_sign m₁ n * qr_sign m₂ n := | ||
by simp_rw [qr_sign, nat.cast_mul, map_mul, jacobi_sym_mul_left] | ||
|
||
/-- `qr_sign` is multiplicative in the second argument. -/ | ||
lemma qr_sign_mul_right (m n₁ n₂ : ℕ) [ne_zero n₁] [ne_zero n₂] : | ||
qr_sign m (n₁ * n₂) = qr_sign m n₁ * qr_sign m n₂ := | ||
jacobi_sym_mul_right (χ₄ m) n₁ n₂ | ||
|
||
/-- `qr_sign` is symmetric when both arguments are odd. -/ | ||
lemma qr_sign_symm {m n : ℕ} (hm : odd m) (hn : odd n) : qr_sign m n = qr_sign n m := | ||
by rw [qr_sign_neg_one_pow hm hn, qr_sign_neg_one_pow hn hm, mul_comm (m / 2)] | ||
|
||
/-- We can move `qr_sign m n` from one side of an equality to the other when `m` and `n` are odd. -/ | ||
lemma qr_sign_eq_iff_eq {m n : ℕ} (hm : odd m) (hn : odd n) (x y : ℤ) : | ||
qr_sign m n * x = y ↔ x = qr_sign m n * y := | ||
by refine ⟨λ h', let h := h'.symm in _, λ h, _⟩; | ||
rw [h, ← mul_assoc, ← pow_two, qr_sign_sq_eq_one hm hn, one_mul] | ||
|
||
/-- The Law of Quadratic Reciprocity for the Jacobi symbol, version with `qr_sign` -/ | ||
lemma jacobi_sym_quadratic_reciprocity' {a b : ℕ} (ha : odd a) (hb : odd b) : | ||
J(a | b) = qr_sign b a * J(b | a) := | ||
begin | ||
-- define the right hand side for fixed `a` as a `ℕ →* ℤ` | ||
let rhs : ℕ → ℕ →* ℤ := λ a, | ||
{ to_fun := λ x, qr_sign x a * J(x | a), | ||
map_one' := by { convert ← mul_one _, symmetry, all_goals { apply jacobi_sym_one_left } }, | ||
map_mul' := λ x y, by rw [qr_sign_mul_left, nat.cast_mul, jacobi_sym_mul_left, | ||
mul_mul_mul_comm] }, | ||
have rhs_apply : ∀ (a b : ℕ), rhs a b = qr_sign b a * J(b | a) := λ a b, rfl, | ||
refine jacobi_sym_value a (rhs a) (λ p pp hp, eq.symm _) hb, | ||
have hpo := pp.eq_two_or_odd'.resolve_left hp, | ||
rw [@legendre_sym.to_jacobi_sym p ⟨pp⟩, rhs_apply, nat.cast_id, | ||
qr_sign_eq_iff_eq hpo ha, qr_sign_symm hpo ha], | ||
refine jacobi_sym_value p (rhs p) (λ q pq hq, _) ha, | ||
have hqo := pq.eq_two_or_odd'.resolve_left hq, | ||
rw [rhs_apply, nat.cast_id, ← @legendre_sym.to_jacobi_sym p ⟨pp⟩, qr_sign_symm hqo hpo, | ||
qr_sign_neg_one_pow hpo hqo, @quadratic_reciprocity' p q ⟨pp⟩ ⟨pq⟩ hp hq], | ||
end | ||
|
||
/-- The Law of Quadratic Reciprocity for the Jacobi symbol -/ | ||
lemma jacobi_sym_quadratic_reciprocity {a b : ℕ} (ha : odd a) (hb : odd b) : | ||
J(a | b) = (-1) ^ ((a / 2) * (b / 2)) * J(b | a) := | ||
by rw [← qr_sign_neg_one_pow ha hb, qr_sign_symm ha hb, jacobi_sym_quadratic_reciprocity' ha hb] | ||
|
||
/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers | ||
with `a % 4 = 1` and `b` odd, then `J(a | b) = J(b | a)`. -/ | ||
theorem jacobi_sym_quadratic_reciprocity_one_mod_four {a b : ℕ} (ha : a % 4 = 1) (hb : odd b) : | ||
J(a | b) = J(b | a) := | ||
by rw [jacobi_sym_quadratic_reciprocity (odd_iff.mpr (odd_of_mod_four_eq_one ha)) hb, | ||
pow_mul, neg_one_pow_div_two_of_one_mod_four ha, one_pow, one_mul] | ||
|
||
/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers | ||
with `a` odd and `b % 4 = 1`, then `J(a | b) = J(b | a)`. -/ | ||
theorem jacobi_sym_quadratic_reciprocity_one_mod_four' {a b : ℕ} (ha : odd a) (hb : b % 4 = 1) : | ||
J(a | b) = J(b | a) := | ||
(jacobi_sym_quadratic_reciprocity_one_mod_four hb ha).symm | ||
|
||
/-- The Law of Quadratic Reciprocityfor the Jacobi symbol: if `a` and `b` are natural numbers | ||
both congruent to `3` mod `4`, then `J(a | b) = -J(b | a)`. -/ | ||
theorem jacobi_sym_quadratic_reciprocity_three_mod_four | ||
{a b : ℕ} (ha : a % 4 = 3) (hb : b % 4 = 3) : | ||
J(a | b) = - J(b | a) := | ||
let nop := @neg_one_pow_div_two_of_three_mod_four in begin | ||
rw [jacobi_sym_quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul]; | ||
rwa [odd_iff, odd_of_mod_four_eq_three], | ||
end | ||
|
||
/-- The Jacobi symbol `J(a | b)` depends only on `b` mod `4*a` (version for `a : ℕ`). -/ | ||
lemma jacobi_sym_mod_right' (a : ℕ) {b : ℕ} (hb : odd b) : J(a | b) = J(a | b % (4 * a)) := | ||
begin | ||
rcases eq_or_ne a 0 with rfl | ha₀, | ||
{ rw [mul_zero, mod_zero], }, | ||
have hb' : odd (b % (4 * a)) := hb.mod_even (even.mul_right (by norm_num) _), | ||
rcases exists_eq_pow_mul_and_not_dvd ha₀ 2 (by norm_num) with ⟨e, a', ha₁', ha₂⟩, | ||
have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp ha₁'), | ||
nth_rewrite 1 [ha₂], nth_rewrite 0 [ha₂], | ||
rw [nat.cast_mul, jacobi_sym_mul_left, jacobi_sym_mul_left, | ||
jacobi_sym_quadratic_reciprocity' ha₁ hb, jacobi_sym_quadratic_reciprocity' ha₁ hb', | ||
nat.cast_pow, jacobi_sym_pow_left, jacobi_sym_pow_left, | ||
(show ((2 : ℕ) : ℤ) = 2, by refl), jacobi_sym_two hb, jacobi_sym_two hb'], | ||
congr' 1, swap, congr' 1, | ||
{ simp_rw [qr_sign], | ||
rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a) ] }, | ||
{ rw [jacobi_sym_mod_left ↑(b % _), jacobi_sym_mod_left b, int.coe_nat_mod, | ||
int.mod_mod_of_dvd b], | ||
simp only [ha₂, nat.cast_mul, ← mul_assoc], | ||
exact dvd_mul_left a' _, }, | ||
cases e, { refl }, | ||
{ rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b], | ||
use 2 ^ e * a', rw [ha₂, pow_succ], ring, } | ||
end | ||
|
||
/-- The Jacobi symbol `J(a | b)` depends only on `b` mod `4*a`. -/ | ||
lemma jacobi_sym_mod_right (a : ℤ) {b : ℕ} (hb : odd b) : J(a | b) = J(a | b % (4 * a.nat_abs)) := | ||
begin | ||
cases int.nat_abs_eq a with ha ha; nth_rewrite 1 [ha]; nth_rewrite 0 [ha], | ||
{ exact jacobi_sym_mod_right' a.nat_abs hb, }, | ||
{ have hb' : odd (b % (4 * a.nat_abs)) := hb.mod_even (even.mul_right (by norm_num) _), | ||
rw [jacobi_sym_neg _ hb, jacobi_sym_neg _ hb', jacobi_sym_mod_right' _ hb, χ₄_nat_mod_four, | ||
χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)], } | ||
end | ||
|
||
end zmod | ||
|
||
end jacobi |