The Jacobi symbol under reflection of the denominator

Mathlib's jacobiSym.mod_right says that for odd b the Jacobi symbol J(a | b) depends only on b modulo 4 |a|. This file adds the companion statement for the reflected class -b: if b and b' are odd and 4 |a| divides b + b', then J(a | b') = sign a * J(a | b). Together the two say that b ↦ J(a | b), extended to negative odd b by J(a | -b) = sign a * J(a | b), is periodic modulo 4 |a| on all odd integers; this is the input that makes the Kronecker symbol (D / ·) of a discriminant a Dirichlet character whose value at -1 is the sign of D.

It also records the form of quadratic reciprocity for an integer numerator a ≡ 1 (mod 4), of either sign: J(a | b) = J(b | |a|) for odd b, and that a square factor prime to b can be dropped from the numerator.

The proof of the reflection law for a natural numerator is adapted from the proof of Mathlib's jacobiSym.mod_right': both split off the power of 2 and apply quadratic reciprocity to the odd part.

Main statements

• TauCeti.jacobiSym_eq_sign_mul_of_dvd_add: J(a | b') = sign a * J(a | b) when b is odd and 4 |a| ∣ b + b'.
• TauCeti.jacobiSym_eq_sign_mul_of_emod_four_eq_zero, TauCeti.jacobiSym_mod_natAbs_of_emod_four_eq_zero: for a ≡ 0 (mod 4) the modulus 4 |a| in both statements can be lowered to |a|.
• TauCeti.jacobiSym_eq_jacobiSym_natAbs_of_emod_four_eq_one: J(a | b) = J(b | |a|) for a ≡ 1 (mod 4) and odd b.
• TauCeti.jacobiSym_sq_mul_of_isCoprime: J(x² y | b) = J(y | b) for x prime to b, and TauCeti.jacobiSym_mul_pow_two_mul_mul_of_isCoprime, its form J(s x^(2k) y | b) = J(s y | b).

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §1.4.

theorem TauCeti.jacobiSym_eq_sign_mul_of_dvd_add (a : ℤ) {b b' : ℕ} (hb : Odd b) (h : 4 * a.natAbs ∣ b + b') : jacobiSym a b' = a.sign * jacobiSym a b

Reflection of the denominator of the Jacobi symbol. If b is odd and 4 |a| divides b + b', so that b' ≡ -b (mod 4 |a|), then J(a | b') = sign a * J(a | b). Together with jacobiSym.mod_right, this says that J(a | ·) is an odd or even function on the odd residues modulo 4 |a| according to the sign of a.

theorem TauCeti.jacobiSym_eq_jacobiSym_natAbs_of_emod_four_eq_one {a : ℤ} (ha : a % 4 = 1) {b : ℕ} (hb : Odd b) : jacobiSym a b = jacobiSym (↑b) a.natAbs

Quadratic reciprocity for a numerator a ≡ 1 (mod 4), of either sign: for odd b, J(a | b) = J(b | |a|). For a > 0 this is jacobiSym.quadratic_reciprocity_one_mod_four; for a < 0 the supplementary factor J(-1 | b) = χ₄ b cancels the sign of reciprocity, since then |a| ≡ 3 (mod 4).

theorem TauCeti.jacobiSym_mod_natAbs_of_emod_four_eq_zero {a : ℤ} (ha : a % 4 = 0) {b : ℕ} (hb : Odd b) : jacobiSym a b = jacobiSym a (b % a.natAbs)

For a ≡ 0 (mod 4), the Jacobi symbol J(a | b) at odd b depends only on b modulo |a|, not merely modulo 4 |a| as in jacobiSym.mod_right: the factor J(4 | b) = 1 may be dropped.

theorem TauCeti.jacobiSym_eq_sign_mul_of_emod_four_eq_zero {a : ℤ} (ha : a % 4 = 0) {b b' : ℕ} (hb : Odd b) (h : a.natAbs ∣ b + b') : jacobiSym a b' = a.sign * jacobiSym a b

The reflection law jacobiSym_eq_sign_mul_of_dvd_add for a ≡ 0 (mod 4), where it needs only |a| ∣ b + b'.

theorem TauCeti.jacobiSym_sq_mul_of_isCoprime {x : ℤ} {b : ℕ} (hx : IsCoprime x ↑b) (y : ℤ) : jacobiSym (x ^ 2 * y) b = jacobiSym y b

A square factor prime to the denominator does not change the Jacobi symbol: J(x² y | b) = J(y | b) when x is prime to b.

theorem TauCeti.jacobiSym_mul_pow_two_mul_mul_of_isCoprime {x : ℤ} {b : ℕ} (hx : IsCoprime x ↑b) (s y : ℤ) (k : ℕ) : jacobiSym (s * (x ^ (2 * k) * y)) b = jacobiSym (s * y) b

An even power of a factor prime to the denominator does not change the Jacobi symbol: J(s x^(2k) y | b) = J(s y | b) when x is prime to b.