The Jacobi Symbol

We define the Jacobi symbol and prove its main properties.

Main definitions

We define the Jacobi symbol, jacobiSym a b, for integers a and natural numbers b as the product over the prime factors p of b of the Legendre symbols legendreSym 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 jacobiSym a 0 = 1 for all a.

Main statements

We prove the main properties of the Jacobi symbol, including the following.

• Multiplicativity in both arguments (jacobiSym.mul_left, jacobiSym.mul_right)

• The value of the symbol is 1 or -1 when the arguments are coprime (jacobiSym.eq_one_or_neg_one)

• The symbol vanishes if and only if b ≠ 0 and the arguments are not coprime (jacobiSym.eq_zero_iff_not_coprime)

• If the symbol has the value -1, then a : ZMod b is not a square (ZMod.nonsquare_of_jacobiSym_eq_neg_one); the converse holds when b = p is a prime (ZMod.nonsquare_iff_jacobiSym_eq_neg_one); in particular, in this case a is a square mod p when the symbol has the value 1 (ZMod.isSquare_of_jacobiSym_eq_one).

• Quadratic reciprocity (jacobiSym.quadratic_reciprocity, jacobiSym.quadratic_reciprocity_one_mod_four, jacobiSym.quadratic_reciprocity_three_mod_four)

• The supplementary laws for a = -1, a = 2, a = -2 (jacobiSym.at_neg_one, jacobiSym.at_two, jacobiSym.at_neg_two)

• The symbol depends on a only via its residue class mod b (jacobiSym.mod_left) and on b only via its residue class mod 4*a (jacobiSym.mod_right)

• A csimp rule for jacobiSym and legendreSym that evaluates J(a | b) efficiently by reducing to the case 0 ≤ a < b and a, b odd, and then swaps a, b and recurses using quadratic reciprocity.

Notation

We define the notation J(a | b) for jacobiSym a b, localized to NumberTheorySymbols.

Tags

Jacobi symbol, quadratic reciprocity

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 jacobiSym a b.

We define localized notation (scope NumberTheorySymbols) J(a | b) for the Jacobi symbol jacobiSym a b.

def jacobiSym (a : ℤ) (b : ℕ) : ℤ

The Jacobi symbol of a and b

def NumberTheorySymbols.«termJ(_|_)» : Lean.ParserDescr

The Jacobi symbol of a and b

Properties of the Jacobi symbol

@[simp]

theorem jacobiSym.zero_right (a : ℤ) : jacobiSym a 0 = 1

The symbol J(a | 0) has the value 1.

@[simp]

theorem jacobiSym.one_right (a : ℤ) : jacobiSym a 1 = 1

The symbol J(a | 1) has the value 1.

theorem jacobiSym.legendreSym.to_jacobiSym (p : ℕ) [fp : Fact (Nat.Prime p)] (a : ℤ) : legendreSym p a = jacobiSym a p

The Legendre symbol legendreSym p a with an integer a and a prime number p is the same as the Jacobi symbol J(a | p).

theorem jacobiSym.mul_right' (a : ℤ) {b₁ b₂ : ℕ} (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) : jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂

The Jacobi symbol is multiplicative in its second argument.

theorem jacobiSym.mul_right (a : ℤ) (b₁ b₂ : ℕ) [NeZero b₁] [NeZero b₂] : jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂

The Jacobi symbol is multiplicative in its second argument.

theorem jacobiSym.trichotomy (a : ℤ) (b : ℕ) : jacobiSym a b = 0 ∨ jacobiSym a b = 1 ∨ jacobiSym a b = -1

The Jacobi symbol takes only the values 0, 1 and -1.

@[simp]

theorem jacobiSym.one_left (b : ℕ) : jacobiSym 1 b = 1

The symbol J(1 | b) has the value 1.

theorem jacobiSym.mul_left (a₁ a₂ : ℤ) (b : ℕ) : jacobiSym (a₁ * a₂) b = jacobiSym a₁ b * jacobiSym a₂ b

The Jacobi symbol is multiplicative in its first argument.

theorem jacobiSym.eq_zero_iff_not_coprime {a : ℤ} {b : ℕ} [NeZero b] : jacobiSym a b = 0 ↔ a.gcd ↑b ≠ 1

The symbol J(a | b) vanishes iff a and b are not coprime (assuming b ≠ 0).

theorem jacobiSym.ne_zero {a : ℤ} {b : ℕ} (h : a.gcd ↑b = 1) : jacobiSym a b ≠ 0

The symbol J(a | b) is nonzero when a and b are coprime.

theorem jacobiSym.eq_zero_iff {a : ℤ} {b : ℕ} : jacobiSym a b = 0 ↔ b ≠ 0 ∧ a.gcd ↑b ≠ 1

The symbol J(a | b) vanishes if and only if b ≠ 0 and a and b are not coprime.

theorem jacobiSym.zero_left {b : ℕ} (hb : 1 < b) : jacobiSym 0 b = 0

The symbol J(0 | b) vanishes when b > 1.

theorem jacobiSym.eq_one_or_neg_one {a : ℤ} {b : ℕ} (h : a.gcd ↑b = 1) : jacobiSym a b = 1 ∨ jacobiSym a b = -1

The symbol J(a | b) takes the value 1 or -1 if a and b are coprime.

theorem jacobiSym.pow_left (a : ℤ) (e b : ℕ) : jacobiSym (a ^ e) b = jacobiSym a b ^ e

We have that J(a^e | b) = J(a | b)^e.

theorem jacobiSym.pow_right (a : ℤ) (b e : ℕ) : jacobiSym a (b ^ e) = jacobiSym a b ^ e

We have that J(a | b^e) = J(a | b)^e.

theorem jacobiSym.sq_one {a : ℤ} {b : ℕ} (h : a.gcd ↑b = 1) : jacobiSym a b ^ 2 = 1

The square of J(a | b) is 1 when a and b are coprime.

theorem jacobiSym.sq_one' {a : ℤ} {b : ℕ} (h : a.gcd ↑b = 1) : jacobiSym (a ^ 2) b = 1

The symbol J(a^2 | b) is 1 when a and b are coprime.

theorem jacobiSym.mod_left (a : ℤ) (b : ℕ) : jacobiSym a b = jacobiSym (a % ↑b) b

The symbol J(a | b) depends only on a mod b.

theorem jacobiSym.mod_left' {a₁ a₂ : ℤ} {b : ℕ} (h : a₁ % ↑b = a₂ % ↑b) : jacobiSym a₁ b = jacobiSym a₂ b

The symbol J(a | b) depends only on a mod b.

theorem jacobiSym.prime_dvd_of_eq_neg_one {p : ℕ} [Fact (Nat.Prime p)] {a : ℤ} (h : jacobiSym a p = -1) {x y : ℤ} (hxy : ↑p ∣ x ^ 2 - a * y ^ 2) : ↑p ∣ x ∧ ↑p ∣ y

If p is prime, J(a | p) = -1 and p divides x^2 - a*y^2, then p must divide x and y.

theorem jacobiSym.list_prod_left {l : List ℤ} {n : ℕ} : jacobiSym l.prod n = (List.map (fun (a : ℤ) => jacobiSym a n) l).prod

We can pull out a product over a list in the first argument of the Jacobi symbol.

theorem jacobiSym.list_prod_right {a : ℤ} {l : List ℕ} (hl : ∀ n ∈ l, n ≠ 0) : jacobiSym a l.prod = (List.map (fun (n : ℕ) => jacobiSym a n) l).prod

We can pull out a product over a list in the second argument of the Jacobi symbol.

theorem jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one {a : ℤ} {n : ℕ} (h : jacobiSym a n = -1) : ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ jacobiSym a p = -1

If J(a | n) = -1, then n has a prime divisor p such that J(a | p) = -1.

theorem ZMod.nonsquare_of_jacobiSym_eq_neg_one {a : ℤ} {b : ℕ} (h : jacobiSym a b = -1) : ¬IsSquare ↑a

If J(a | b) is -1, then a is not a square modulo b.

theorem ZMod.nonsquare_iff_jacobiSym_eq_neg_one {a : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : jacobiSym a p = -1 ↔ ¬IsSquare ↑a

If p is prime, then J(a | p) is -1 iff a is not a square modulo p.

theorem ZMod.isSquare_of_jacobiSym_eq_one {a : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (h : jacobiSym a p = 1) : IsSquare ↑a

If p is prime and J(a | p) = 1, then a is a square mod p.

Values at -1, 2 and -2

theorem jacobiSym.value_at (a : ℤ) {R : Type u_1} [Semiring R] (χ : R →* ℤ) (hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p) {b : ℕ} (hb : Odd b) : jacobiSym a b = χ ↑b

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.

theorem jacobiSym.at_neg_one {b : ℕ} (hb : Odd b) : jacobiSym (-1) b = ZMod.χ₄ ↑b

If b is odd, then J(-1 | b) is given by χ₄ b.

theorem jacobiSym.neg (a : ℤ) {b : ℕ} (hb : Odd b) : jacobiSym (-a) b = ZMod.χ₄ ↑b * jacobiSym a b

If b is odd, then J(-a | b) = χ₄ b * J(a | b).

theorem jacobiSym.at_two {b : ℕ} (hb : Odd b) : jacobiSym 2 b = ZMod.χ₈ ↑b

If b is odd, then J(2 | b) is given by χ₈ b.

theorem jacobiSym.at_neg_two {b : ℕ} (hb : Odd b) : jacobiSym (-2) b = ZMod.χ₈' ↑b

If b is odd, then J(-2 | b) is given by χ₈' b.

theorem jacobiSym.div_four_left {a : ℤ} {b : ℕ} (ha4 : a % 4 = 0) (hb2 : b % 2 = 1) : jacobiSym (a / 4) b = jacobiSym a b

theorem jacobiSym.even_odd {a : ℤ} {b : ℕ} (ha2 : a % 2 = 0) (hb2 : b % 2 = 1) : (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (a / 2) b else jacobiSym (a / 2) b) = jacobiSym a b

Quadratic Reciprocity

def qrSign (m n : ℕ) : ℤ

The bi-multiplicative map giving the sign in the Law of Quadratic Reciprocity

theorem qrSign.neg_one_pow {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n = (-1) ^ (m / 2 * (n / 2))

We can express qrSign m n as a power of -1 when m and n are odd.

theorem qrSign.sq_eq_one {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n ^ 2 = 1

When m and n are odd, then the square of qrSign m n is 1.

theorem qrSign.mul_left (m₁ m₂ n : ℕ) : qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n

qrSign is multiplicative in the first argument.

theorem qrSign.mul_right (m n₁ n₂ : ℕ) [NeZero n₁] [NeZero n₂] : qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂

qrSign is multiplicative in the second argument.

theorem qrSign.symm {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n = qrSign n m

qrSign is symmetric when both arguments are odd.

theorem qrSign.eq_iff_eq {m n : ℕ} (hm : Odd m) (hn : Odd n) (x y : ℤ) : qrSign m n * x = y ↔ x = qrSign m n * y

We can move qrSign m n from one side of an equality to the other when m and n are odd.

theorem jacobiSym.quadratic_reciprocity' {a b : ℕ} (ha : Odd a) (hb : Odd b) : jacobiSym (↑a) b = qrSign b a * jacobiSym (↑b) a

The Law of Quadratic Reciprocity for the Jacobi symbol, version with qrSign

theorem jacobiSym.quadratic_reciprocity {a b : ℕ} (ha : Odd a) (hb : Odd b) : jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a

The Law of Quadratic Reciprocity for the Jacobi symbol

theorem jacobiSym.quadratic_reciprocity_one_mod_four {a b : ℕ} (ha : a % 4 = 1) (hb : Odd b) : jacobiSym (↑a) b = jacobiSym (↑b) a

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 jacobiSym.quadratic_reciprocity_one_mod_four' {a b : ℕ} (ha : Odd a) (hb : b % 4 = 1) : jacobiSym (↑a) b = jacobiSym (↑b) a

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 jacobiSym.quadratic_reciprocity_three_mod_four {a b : ℕ} (ha : a % 4 = 3) (hb : b % 4 = 3) : jacobiSym (↑a) b = -jacobiSym (↑b) a

The Law of Quadratic Reciprocity for the Jacobi symbol: if a and b are natural numbers both congruent to 3 mod 4, then J(a | b) = -J(b | a).

theorem jacobiSym.quadratic_reciprocity_if {a b : ℕ} (ha2 : a % 2 = 1) (hb2 : b % 2 = 1) : (if a % 4 = 3 ∧ b % 4 = 3 then -jacobiSym (↑b) a else jacobiSym (↑b) a) = jacobiSym (↑a) b

theorem jacobiSym.mod_right' (a : ℕ) {b : ℕ} (hb : Odd b) : jacobiSym (↑a) b = jacobiSym (↑a) (b % (4 * a))

The Jacobi symbol J(a | b) depends only on b mod 4*a (version for a : ℕ).

theorem jacobiSym.mod_right (a : ℤ) {b : ℕ} (hb : Odd b) : jacobiSym a b = jacobiSym a (b % (4 * a.natAbs))

The Jacobi symbol J(a | b) depends only on b mod 4*a.

Fast computation of the Jacobi symbol

We follow the implementation as in Mathlib/Tactic/NormNum/LegendreSymbol.lean.