mathlib3 documentation

number_theory.legendre_symbol.jacobi_symbol

The Jacobi Symbol #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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 (zmod.nonsquare_of_jacobi_sym_eq_neg_one); the converse holds when b = p is a prime (zmod.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 (zmod.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.at_neg_one, jacobi_sym.at_two, jacobi_sym.at_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

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.

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

The Jacobi symbol of a and b

Equations

jacobi_sym a b = (list.pmap (λ (p : ℕ) (pp : nat.prime p), legendre_sym p a) b.factors _).prod

Properties of the Jacobi symbol #

@[simp]

theorem jacobi_sym.zero_right (a : ℤ) :

jacobi_sym a 0 = 1

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

@[simp]

theorem jacobi_sym.one_right (a : ℤ) :

jacobi_sym a 1 = 1

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

theorem legendre_sym.to_jacobi_sym (p : ℕ) [fp : fact (nat.prime p)] (a : ℤ) :

legendre_sym p a = jacobi_sym a p

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).

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

jacobi_sym a (b₁ * b₂) = jacobi_sym a b₁ * jacobi_sym a b₂

The Jacobi symbol is multiplicative in its second argument.

theorem jacobi_sym.mul_right (a : ℤ) (b₁ b₂ : ℕ) [ne_zero b₁] [ne_zero b₂] :

jacobi_sym a (b₁ * b₂) = jacobi_sym a b₁ * jacobi_sym a b₂

The Jacobi symbol is multiplicative in its second argument.

theorem jacobi_sym.trichotomy (a : ℤ) (b : ℕ) :

jacobi_sym a b = 0 ∨ jacobi_sym a b = 1 ∨ jacobi_sym a b = -1

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

@[simp]

theorem jacobi_sym.one_left (b : ℕ) :

jacobi_sym 1 b = 1

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

theorem jacobi_sym.mul_left (a₁ a₂ : ℤ) (b : ℕ) :

jacobi_sym (a₁ * a₂) b = jacobi_sym a₁ b * jacobi_sym a₂ b

The Jacobi symbol is multiplicative in its first argument.

theorem jacobi_sym.eq_zero_iff_not_coprime {a : ℤ} {b : ℕ} [ne_zero b] :

jacobi_sym a b = 0 ↔ a.gcd ↑b ≠ 1

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

@[protected]

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

jacobi_sym a b ≠ 0

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

theorem jacobi_sym.eq_zero_iff {a : ℤ} {b : ℕ} :

jacobi_sym 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 jacobi_sym.zero_left {b : ℕ} (hb : 1 < b) :

jacobi_sym 0 b = 0

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

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

jacobi_sym a b = 1 ∨ jacobi_sym a b = -1

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

theorem jacobi_sym.pow_left (a : ℤ) (e b : ℕ) :

jacobi_sym (a ^ e) b = jacobi_sym a b ^ e

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

theorem jacobi_sym.pow_right (a : ℤ) (b e : ℕ) :

jacobi_sym a (b ^ e) = jacobi_sym a b ^ e

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

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

jacobi_sym a b ^ 2 = 1

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

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

jacobi_sym (a ^ 2) b = 1

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

theorem jacobi_sym.mod_left (a : ℤ) (b : ℕ) :

jacobi_sym a b = jacobi_sym (a % ↑b) b

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

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

jacobi_sym a₁ b = jacobi_sym a₂ b

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

theorem jacobi_sym.prime_dvd_of_eq_neg_one {p : ℕ} [fact (nat.prime p)] {a : ℤ} (h : jacobi_sym 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 jacobi_sym.list_prod_left {l : list ℤ} {n : ℕ} :

jacobi_sym l.prod n = (list.map (λ (a : ℤ), jacobi_sym a n) l).prod

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

theorem jacobi_sym.list_prod_right {a : ℤ} {l : list ℕ} (hl : ∀ (n : ℕ), n ∈ l → n ≠ 0) :

jacobi_sym a l.prod = (list.map (λ (n : ℕ), jacobi_sym a n) l).prod

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

theorem jacobi_sym.eq_neg_one_at_prime_divisor_of_eq_neg_one {a : ℤ} {n : ℕ} (h : jacobi_sym a n = -1) :

∃ (p : ℕ) (hp : nat.prime p), p ∣ n ∧ jacobi_sym 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_jacobi_sym_eq_neg_one {a : ℤ} {b : ℕ} (h : jacobi_sym a b = -1) :

¬is_square ↑a

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

theorem zmod.nonsquare_iff_jacobi_sym_eq_neg_one {a : ℤ} {p : ℕ} [fact (nat.prime p)] :

jacobi_sym a p = -1 ↔ ¬is_square ↑a

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

theorem zmod.is_square_of_jacobi_sym_eq_one {a : ℤ} {p : ℕ} [fact (nat.prime p)] (h : jacobi_sym a p = 1) :

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

Values at `-1`, `2` and `-2` #

theorem jacobi_sym.value_at (a : ℤ) {R : Type u_1} [comm_semiring R] (χ : R →* ℤ) (hp : ∀ (p : ℕ) (pp : nat.prime p), p ≠ 2 → legendre_sym p a = ⇑χ ↑p) {b : ℕ} (hb : odd b) :

jacobi_sym 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 jacobi_sym.at_neg_one {b : ℕ} (hb : odd b) :

jacobi_sym (-1) b = ⇑zmod.χ₄ ↑b

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

@[protected]

theorem jacobi_sym.neg (a : ℤ) {b : ℕ} (hb : odd b) :

jacobi_sym (-a) b = ⇑zmod.χ₄ ↑b * jacobi_sym a b

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

theorem jacobi_sym.at_two {b : ℕ} (hb : odd b) :

jacobi_sym 2 b = ⇑zmod.χ₈ ↑b

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

theorem jacobi_sym.at_neg_two {b : ℕ} (hb : odd b) :

jacobi_sym (-2) b = ⇑zmod.χ₈' ↑b

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

Quadratic Reciprocity #

def qr_sign (m n : ℕ) :

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

Equations

qr_sign m n = jacobi_sym (⇑zmod.χ₄ ↑m) n

theorem qr_sign.neg_one_pow {m n : ℕ} (hm : odd m) (hn : odd n) :

qr_sign m n = (-1) ^ (m / 2 * (n / 2))

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

theorem qr_sign.sq_eq_one {m n : ℕ} (hm : odd m) (hn : odd n) :

qr_sign m n ^ 2 = 1

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

theorem qr_sign.mul_left (m₁ m₂ n : ℕ) :

qr_sign (m₁ * m₂) n = qr_sign m₁ n * qr_sign m₂ n

qr_sign is multiplicative in the first argument.

theorem 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₂

qr_sign is multiplicative in the second argument.

@[protected]

theorem qr_sign.symm {m n : ℕ} (hm : odd m) (hn : odd n) :

qr_sign m n = qr_sign n m

qr_sign is symmetric when both arguments are odd.

theorem 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

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

theorem jacobi_sym.quadratic_reciprocity' {a b : ℕ} (ha : odd a) (hb : odd b) :

jacobi_sym ↑a b = qr_sign b a * jacobi_sym ↑b a

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

theorem jacobi_sym.quadratic_reciprocity {a b : ℕ} (ha : odd a) (hb : odd b) :

jacobi_sym ↑a b = (-1) ^ (a / 2 * (b / 2)) * jacobi_sym ↑b a

The Law of Quadratic Reciprocity for the Jacobi symbol

theorem jacobi_sym.quadratic_reciprocity_one_mod_four {a b : ℕ} (ha : a % 4 = 1) (hb : odd b) :

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

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

jacobi_sym ↑a b = -jacobi_sym ↑b a

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.mod_right' (a : ℕ) {b : ℕ} (hb : odd b) :

jacobi_sym ↑a b = jacobi_sym ↑a (b % (4 * a))

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

theorem jacobi_sym.mod_right (a : ℤ) {b : ℕ} (hb : odd b) :

jacobi_sym a b = jacobi_sym a (b % (4 * a.nat_abs))

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