The Kronecker symbol

Mathlib's Jacobi symbol jacobiSym a b is defined for a natural denominator b, and is the quadratic symbol only for odd b. The Kronecker symbol (a / b) extends it to every integer denominator b, multiplicatively in b, by fixing the values at the three denominators the Jacobi symbol does not cover:

• (a / 2) is χ₈ a: 0 for even a, 1 for a ≡ ±1 (mod 8) and -1 for a ≡ ±3 (mod 8);
• (a / -1) is -1 for a < 0 and 1 otherwise;
• (a / 0) is 1 for a = ±1 and 0 otherwise.

So for b ≠ 0, writing |b| = 2 ^ e * m with m odd, (a / b) = (a / -1)^[b < 0] * χ₈ a ^ e * J(a | m). The value at 0 is not the Jacobi symbol's J(a | 0) = 1: the two symbols agree on odd positive denominators only. That value also makes multiplicativity in the denominator fail exactly for the numerator -1, where (-1 / 0) = 1 but (-1 / 0) * (-1 / 3) = -1.

The point of the extension is the case of a discriminant D ≡ 0, 1 (mod 4). Then (D / ·) is periodic modulo |D| on all of ℤ, so it is a quadratic Dirichlet character kroneckerChar of modulus |D|, whose value at -1 is the sign of D. For D ≡ 1 (mod 4) this rests on quadratic reciprocity, in the form (D / n) = J(n | |D|); for D ≡ 0 (mod 4) it rests on the periodicity of J(D | ·) modulo |D| on odd numbers and on its reflection law under b ↦ -b. The character need not be primitive: (-12 / ·) is induced from (-3 / ·).

Main definitions

• TauCeti.kroneckerSym a b: the Kronecker symbol (a / b).
• TauCeti.kroneckerChar R D hD hD₀: for D ≡ 0, 1 (mod 4), D ≠ 0, the Dirichlet character (D / ·) of modulus |D| with values in a commutative ring R.

Main statements

• TauCeti.kroneckerSym_eq_jacobiSym, TauCeti.kroneckerSym_eq_legendreSym: agreement with the Jacobi symbol at odd positive denominators and with the Legendre symbol at odd primes.
• TauCeti.kroneckerSym_two_right, TauCeti.kroneckerSym_neg_one_right, TauCeti.kroneckerSym_zero_right: the values at 2, -1 and 0.
• TauCeti.kroneckerSym_mul_right, TauCeti.kroneckerSym_mul_right_of_ne_neg_one: multiplicativity in the denominator, over nonzero factors, and without restriction when the numerator is not -1.
• TauCeti.kroneckerSym_mul_left, TauCeti.kroneckerSym_pow_left, TauCeti.kroneckerSym_eq_one_of_isSquare: multiplicativity in the numerator, over nonzero factors, unrestricted power law, and value 1 on squares coprime to the denominator.
• TauCeti.kroneckerSym_eq_zero_iff: (a / b) = 0 exactly when gcd (a, b) ≠ 1.
• TauCeti.kroneckerSym_eq_jacobiSym_natAbs: (D / n) = J(n | |D|) for D ≡ 1 (mod 4).
• TauCeti.kroneckerSym_mod_right': for D ≡ 0, 1 (mod 4), (D / ·) is periodic modulo D.
• TauCeti.kroneckerChar_intCast, TauCeti.kroneckerChar_isQuadratic, TauCeti.kroneckerChar_neg_one: the character computes the Kronecker symbol, is quadratic, and has value sign D at -1.
• TauCeti.conductor_kroneckerChar_dvd_iff: the conductor of kroneckerChar divides N exactly when (D / a) = 1 for the odd a ≡ 1 (mod N) prime to D.
• TauCeti.changeLevel_kroneckerChar_sq_mul, TauCeti.kroneckerChar_eq_one_of_isSquare, TauCeti.conductor_kroneckerChar_eq_of_isSquare_mul, TauCeti.conductor_kroneckerChar_eq_natAbs_of_prime: (m² D / ·) is induced from (D / ·) for m ≠ 0, so discriminants in the same square class share their conductor and primitive character, a square discriminant gives the trivial character of conductor 1, and a prime discriminant (|D| prime) gives a primitive character of conductor |D|.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §1.4.2.
• H. Cohen, Number Theory, Volume I: Tools and Diophantine Equations, §2.2.

Definition and the values at 0, -1, 2 and odd denominators

def TauCeti.kroneckerSym (a b : ℤ) : ℤ

The Kronecker symbol (a / b): the extension of the Jacobi symbol jacobiSym a b to all integer denominators b, multiplicative in b (over nonzero factors, kroneckerSym_mul_right) and with the standard values at 2, -1 and 0: (a / 2) = χ₈ a, (a / -1) is the sign of a with (0 / -1) = 1, and (a / 0) is 1 for a = ±1 and 0 otherwise. For b ≠ 0 with |b| = 2 ^ e * m, m odd, it is (a / -1)^[b < 0] * χ₈ a ^ e * J(a | m).

@[simp]

theorem TauCeti.kroneckerSym_zero_right (a : ℤ) : kroneckerSym a 0 = if a = 1 ∨ a = -1 then 1 else 0

(a / 0) is 1 for a = ±1 and 0 otherwise. It is not jacobiSym a 0 = 1.

theorem TauCeti.kroneckerSym_of_ne_zero (a : ℤ) {b : ℤ} (hb : b ≠ 0) : kroneckerSym a b = (if a < 0 ∧ b < 0 then -1 else 1) * ZMod.χ₈ ↑a ^ b.natAbs.factorization 2 * jacobiSym a (b.natAbs / 2 ^ b.natAbs.factorization 2)

The Kronecker symbol at a nonzero denominator b, with |b| = 2 ^ e * m and m odd.

theorem TauCeti.kroneckerSym_of_odd (a : ℤ) {b : ℤ} (hb : Odd b) : kroneckerSym a b = (if a < 0 ∧ b < 0 then -1 else 1) * jacobiSym a b.natAbs

At an odd denominator b, of either sign, the Kronecker symbol is the Jacobi symbol at |b|, times -1 when both a < 0 and b < 0.

theorem TauCeti.kroneckerSym_eq_jacobiSym (a : ℤ) {b : ℕ} (hb : Odd b) : kroneckerSym a ↑b = jacobiSym a b

At an odd positive denominator the Kronecker symbol is the Jacobi symbol.

theorem TauCeti.kroneckerSym_eq_legendreSym (a : ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) : kroneckerSym a ↑p = legendreSym p a

At an odd prime the Kronecker symbol is the Legendre symbol.

@[simp]

theorem TauCeti.kroneckerSym_one_right (a : ℤ) : kroneckerSym a 1 = 1

(a / 1) = 1.

@[simp]

theorem TauCeti.kroneckerSym_neg_one_right (a : ℤ) : kroneckerSym a (-1) = if a < 0 then -1 else 1

(a / -1) is -1 for a < 0 and 1 otherwise.

@[simp]

theorem TauCeti.kroneckerSym_two_right (a : ℤ) : kroneckerSym a 2 = ZMod.χ₈ ↑a

(a / 2) = χ₈ a: it is 0 for even a, 1 for a ≡ ±1 (mod 8) and -1 for a ≡ ±3 (mod 8) (ZMod.χ₈_int_eq_if_mod_eight).

@[simp]

theorem TauCeti.kroneckerSym_one_left (b : ℤ) : kroneckerSym 1 b = 1

(1 / b) = 1, including at b = 0.

Multiplicativity in the denominator

theorem TauCeti.kroneckerSym_mul_right (a : ℤ) {b c : ℤ} (hb : b ≠ 0) (hc : c ≠ 0) : kroneckerSym a (b * c) = kroneckerSym a b * kroneckerSym a c

Multiplicativity of the Kronecker symbol in the denominator, over nonzero factors, as in jacobiSym.mul_right'. The hypotheses cannot be dropped: for a = -1, b = 0, c = 3 the left side is (-1 / 0) = 1 and the right side is -1 (kroneckerSym_zero_right).

theorem TauCeti.kroneckerSym_mul_right_of_ne_neg_one {a : ℤ} (ha : a ≠ -1) (b c : ℤ) : kroneckerSym a (b * c) = kroneckerSym a b * kroneckerSym a c

For a numerator other than -1, the Kronecker symbol is completely multiplicative in the denominator: (a / 0) is 1 when a = 1, where every value is 1, and 0 otherwise, where it absorbs the product. Every discriminant D ≡ 0, 1 (mod 4) is such a numerator.

theorem TauCeti.kroneckerSym_pow_right (a b : ℤ) (k : ℕ) : kroneckerSym a (b ^ k) = kroneckerSym a b ^ k

The Kronecker symbol of a power is the power of the symbol. Unlike multiplicativity, this holds without restriction: at b = 0 the value (a / 0) ∈ {0, 1} is idempotent.

Vanishing and the values 0, 1, -1

theorem TauCeti.kroneckerSym_eq_zero_iff {a b : ℤ} : kroneckerSym a b = 0 ↔ a.gcd b ≠ 1

The Kronecker symbol (a / b) vanishes exactly when a and b have a common factor, as for jacobiSym.eq_zero_iff. At b = 0 this says that (a / 0) ≠ 0 exactly for a = ±1.

@[simp]

theorem TauCeti.kroneckerSym_zero_left (b : ℤ) : kroneckerSym 0 b = if b = 1 ∨ b = -1 then 1 else 0

(0 / b) is 1 for b = ±1 and 0 otherwise.

theorem TauCeti.kroneckerSym_trichotomy (a b : ℤ) : kroneckerSym a b = 0 ∨ kroneckerSym a b = 1 ∨ kroneckerSym a b = -1

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

Multiplicativity in the numerator

theorem TauCeti.kroneckerSym_mul_left {a a' : ℤ} (ha : a ≠ 0) (ha' : a' ≠ 0) (b : ℤ) : kroneckerSym (a * a') b = kroneckerSym a b * kroneckerSym a' b

Multiplicativity of the Kronecker symbol in the numerator, over nonzero factors, as in jacobiSym.mul_left. The hypotheses cannot be dropped: for a = 0, a' = -1, b = -1 the left side is (0 / -1) = 1 and the right side is -1 (kroneckerSym_neg_one_right).

theorem TauCeti.kroneckerSym_pow_left (a b : ℤ) (k : ℕ) : kroneckerSym (a ^ k) b = kroneckerSym a b ^ k

The Kronecker symbol of a power in the numerator is the power of the symbol. Unlike kroneckerSym_mul_left, this holds without restriction: at a = 0 the value (0 / b) ∈ {0, 1} is idempotent.

theorem TauCeti.kroneckerSym_sq_one {a b : ℤ} (h : a.gcd b = 1) : kroneckerSym (a ^ 2) b = 1

(a² / b) = 1 when a and b are coprime, including at a = 0 (where b = ±1).

theorem TauCeti.kroneckerSym_eq_one_of_isSquare {a b : ℤ} (ha : IsSquare a) (h : a.gcd b = 1) : kroneckerSym a b = 1

For a square integer a coprime to b, (a / b) = 1.

theorem TauCeti.kroneckerSym_mul_sq {a u b : ℤ} (hu : u ≠ 0) (hub : u.gcd b = 1) : kroneckerSym (a * u ^ 2) b = kroneckerSym a b

Multiplying a numerator a by a nonzero square u² coprime to b leaves (a / b) unchanged. The hypothesis u ≠ 0 cannot be dropped: at a = -1, u = 0, b = -1 the left side is (0 / -1) = 1 and the right side is -1.

The Kronecker symbol of a discriminant

theorem TauCeti.sq_mul_modEq_four {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (m : ℤ) : m ^ 2 * D ≡ 0 [ZMOD 4] ∨ m ^ 2 * D ≡ 1 [ZMOD 4]

Multiplying a discriminant D ≡ 0, 1 (mod 4) by a square preserves the congruence condition ≡ 0, 1 (mod 4).

theorem TauCeti.kroneckerSym_eq_jacobiSym_natAbs {D : ℤ} (hD : D ≡ 1 [ZMOD 4]) (n : ℤ) : kroneckerSym D n = jacobiSym n D.natAbs

For D ≡ 1 (mod 4), the Kronecker symbol (D / n) is the Jacobi symbol J(n | |D|), for every integer n. At odd n > 0 this is quadratic reciprocity, at n = 2 the supplementary law χ₈ D = J(2 | |D|), and at n = -1 the supplementary law sign D = J(-1 | |D|). In particular (D / ·) is periodic modulo |D|.

theorem TauCeti.kroneckerSym_mod_right' {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) {m n : ℤ} (h : m % D = n % D) : kroneckerSym D m = kroneckerSym D n

For a discriminant D ≡ 0, 1 (mod 4), the Kronecker symbol (D / ·) is periodic modulo D.

theorem TauCeti.kroneckerSym_mod_right {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (n : ℤ) : kroneckerSym D n = kroneckerSym D (n % D)

For a discriminant D ≡ 0, 1 (mod 4), (D / n) = (D / (n % D)).

The Kronecker character of a discriminant

def TauCeti.kroneckerChar (R : Type u_1) [CommRing R] (D : ℤ) (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) : DirichletCharacter R D.natAbs

The Kronecker character of a discriminant D ≡ 0, 1 (mod 4), D ≠ 0: the Dirichlet character (D / ·) of modulus |D|, with values in a commutative ring R. It is well defined because (D / ·) is periodic modulo |D| (kroneckerSym_mod_right') and multiplicative (kroneckerSym_mul_right_of_ne_neg_one, as D ≠ -1), and it vanishes off the units because (D / n) = 0 when gcd (D, n) ≠ 1 (kroneckerSym_eq_zero_iff). It need not be primitive.

theorem TauCeti.kroneckerChar_apply {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) (x : ZMod D.natAbs) : (kroneckerChar R D hD hD₀) x = ↑(kroneckerSym D ↑x.val)

The Kronecker character at x : ZMod |D| is the Kronecker symbol (D / x.val), by definition.

@[simp]

theorem TauCeti.kroneckerChar_intCast {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) (a : ℤ) : (kroneckerChar R D hD hD₀) ↑a = ↑(kroneckerSym D a)

The Kronecker character at the class of an integer a is the Kronecker symbol (D / a).

@[simp]

theorem TauCeti.kroneckerChar_natCast {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) (n : ℕ) : (kroneckerChar R D hD hD₀) ↑n = ↑(kroneckerSym D ↑n)

The Kronecker character at the class of a natural number n is the Kronecker symbol (D / n).

theorem TauCeti.kroneckerChar_isQuadratic {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) : MulChar.IsQuadratic (kroneckerChar R D hD hD₀)

The Kronecker character is quadratic: it takes only the values 0, 1 and -1.

@[simp]

theorem TauCeti.kroneckerChar_neg_one {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) : (kroneckerChar R D hD hD₀) (-1) = ↑D.sign

The Kronecker character takes the value sign D at -1: it is even for D > 0 and odd for D < 0.

theorem TauCeti.conductor_kroneckerChar_dvd_iff {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) [NeZero 2] {N : ℕ} : (kroneckerChar R D hD hD₀).conductor ∣ N ↔ ∀ (a : ℕ), Odd a → a.Coprime D.natAbs → a ≡ 1 [MOD N] → kroneckerSym D ↑a = 1

The conductor of the Kronecker character. The conductor of (D / ·) divides N exactly when (D / a) = 1 for every odd natural number a prime to D with a ≡ 1 (mod N). The modulus N need not divide D, so this is how (D / ·) is shown to be induced from a character modulo N when only the values at odd a ≡ 1 (mod N) are known. The coefficient ring only needs 2 ≠ 0, so that the values 0, 1 and -1 stay distinct.

theorem TauCeti.changeLevel_kroneckerChar_sq_mul {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) {m : ℤ} (hm : m ≠ 0) : (DirichletCharacter.changeLevel ⋯) (kroneckerChar R D hD hD₀) = kroneckerChar R (m ^ 2 * D) ⋯ ⋯

Multiplying a discriminant by a nonzero square induces its Kronecker character: for m ≠ 0, the Kronecker character (m² D / ·) of modulus |m² D| is DirichletCharacter.changeLevel of (D / ·). For instance (-12 / ·) is induced from (-3 / ·).

theorem TauCeti.conductor_kroneckerChar_sq_mul {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) {m : ℤ} (hm : m ≠ 0) : (kroneckerChar R (m ^ 2 * D) ⋯ ⋯).conductor = (kroneckerChar R D hD hD₀).conductor

Multiplying a discriminant D by a nonzero square m² leaves the conductor of its Kronecker character unchanged.

theorem TauCeti.primitiveCharacter_kroneckerChar_sq_mul_apply {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) {m : ℤ} (hm : m ≠ 0) (a : ℤ) : (kroneckerChar R (m ^ 2 * D) ⋯ ⋯).primitiveCharacter ↑a = (kroneckerChar R D hD hD₀).primitiveCharacter ↑a

Multiplying a discriminant D by a nonzero square m² leaves the values of the associated primitive character unchanged.

theorem TauCeti.kroneckerChar_eq_one_of_isSquare {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) (hsq : IsSquare D) : kroneckerChar R D hD hD₀ = 1

For a nonzero square discriminant D, the Kronecker character (D / ·) is the trivial Dirichlet character modulo |D|.

theorem TauCeti.conductor_kroneckerChar_eq_one_of_isSquare {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) (hsq : IsSquare D) : (kroneckerChar R D hD hD₀).conductor = 1

For a nonzero square discriminant D, the Kronecker character (D / ·) has conductor 1.

theorem TauCeti.primitiveCharacter_kroneckerChar_of_isSquare {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) (hsq : IsSquare D) : (kroneckerChar R D hD hD₀).primitiveCharacter = 1

For a nonzero square discriminant D, the primitive character associated to (D / ·) is the trivial character modulo 1.

theorem TauCeti.conductor_kroneckerChar_eq_of_isSquare_mul {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) {D' : ℤ} (hD' : D' ≡ 0 [ZMOD 4] ∨ D' ≡ 1 [ZMOD 4]) (hD'₀ : D' ≠ 0) (hsq : IsSquare (D * D')) : (kroneckerChar R D hD hD₀).conductor = (kroneckerChar R D' hD' hD'₀).conductor

Square-class invariance of the Kronecker conductor. Two nonzero discriminants D and D' whose product D * D' is a square have Kronecker characters of the same conductor.

theorem TauCeti.primitiveCharacter_kroneckerChar_apply_of_isSquare_mul {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) {D' : ℤ} (hD' : D' ≡ 0 [ZMOD 4] ∨ D' ≡ 1 [ZMOD 4]) (hD'₀ : D' ≠ 0) (hsq : IsSquare (D * D')) (a : ℤ) : (kroneckerChar R D hD hD₀).primitiveCharacter ↑a = (kroneckerChar R D' hD' hD'₀).primitiveCharacter ↑a

Square-class invariance of the primitive Kronecker character. Two nonzero discriminants D and D' whose product D * D' is a square have the same primitive character values at every integer a.

theorem TauCeti.conductor_kroneckerChar_ne_one_of_neg {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) [NeZero 2] (hDneg : D < 0) : (kroneckerChar R D hD hD₀).conductor ≠ 1

For a negative discriminant D < 0 and a coefficient ring with 2 ≠ 0, the Kronecker character (D / ·) is odd (kroneckerChar_neg_one) and therefore has conductor different from 1.

theorem TauCeti.conductor_kroneckerChar_eq_natAbs_of_prime {R : Type u_1} [CommRing R] {D : ℤ} (hD : D ≡ 0 [ZMOD 4] ∨ D ≡ 1 [ZMOD 4]) (hD₀ : D ≠ 0) [NeZero 2] (hp : Nat.Prime D.natAbs) : (kroneckerChar R D hD hD₀).conductor = D.natAbs

For a prime discriminant, meaning that |D| is prime (such as D = -3, -7, -11, 5, 13), and 2 ≠ 0 in R, the Kronecker character (D / ·) is primitive, of conductor |D|. It is nontrivial because |D| is odd, D ≡ 1 (mod 4), so (D / ·) is the Legendre symbol modulo |D|, which takes the value -1 at a nonresidue.