Gauss sums of quadratic forms in even rank

Let A be a symmetric matrix indexed by a type with 2k elements. This file evaluates the Gauss sum of the quadratic form x ↦ xᵀ A x in two settings, both in terms of the quadratic character of the signed determinant (-1)^k det A.

Over a finite field F of odd characteristic with q elements, for det A ≠ 0 and a primitive additive character ψ of F,

∑_x ψ(xᵀ A x) = χ((-1)^k det A) q^k,

where χ is the quadratic character of F. Group the terms by the value c = xᵀ A x. For k > 0 the number of solutions of xᵀ A x = c is q^{2k-1} + χ((-1)^k det A) q^{k-1} ν(c), with ν(0) = q - 1 and ν(c) = -1 otherwise (Matrix.IsSymm.card_dotProduct_mulVec_eq_of_card_eq_two_mul_add_two), and ψ sums to zero over F.

For an integer matrix A, an odd modulus a prime to det A, and e(t) = exp (2πi t),

∑_{x ∈ (ℤ/a)^{2k}} e(xᵀ A x / a) = ((-1)^k det A / a) a^k,

with the Jacobi symbol on the right. The sign of the classical quadratic Gauss sum never enters. The proof reduces to prime moduli in two steps.

• Coprime moduli. If u n + v m = 1, then 1 / (m n) = u / m + v / n, and the Chinese remainder theorem splits the sum modulo m n into the sums of u A modulo m and of v A modulo n. Since det (u A) = u^{2k} det A, this does not change the Jacobi symbols.
• Removing a square. If N = p² M with p odd and prime to det A, the sum modulo N is p^{2k} times the sum modulo M. Translating x by c z with c = p M changes xᵀ A x by 2c (A x) ⬝ᵥ z, because c² ≡ 0 (mod N); averaging over z kills every x with c x ≠ 0, since c x = 0 exactly when x ≡ 0 (mod p) and 2A is invertible modulo p. The surviving x are the multiples p w of the classes w ∈ ℤ/pM, and on them e(p² wᵀ A w / N) = e(wᵀ A w / M).

At a prime p the sum is the Gauss sum over the field ZMod p with the standard character.

Since 2 is invertible modulo an odd a, the integral quadratic form x ↦ xᵀ B x / 2 of an even symmetric matrix B is x ↦ xᵀ A x modulo a for an integer matrix A ≡ B / 2, so the second evaluation covers the Gauss sums of integral quadratic forms that are unimodular modulo a. These are the sums that arise when theta series of even lattices are transformed under Γ₀(N).

Main statements

• Matrix.IsSymm.sum_addChar_dotProduct_mulVec_of_card_eq_two_mul: the Gauss sum of a nondegenerate quadratic form of even rank over a finite field of odd characteristic.
• Matrix.sum_stdAddChar_dotProduct_mulVec_mul: the Gauss sums modulo coprime m and n multiply.
• Matrix.IsSymm.sum_stdAddChar_dotProduct_mulVec_of_eq_sq_mul: the Gauss sum modulo p² M is p^{#ι} times the Gauss sum modulo M.
• Matrix.IsSymm.sum_stdAddChar_dotProduct_mulVec_eq_jacobiSym: the evaluation modulo an odd a prime to det A.

References

• R. Lidl and H. Niederreiter, Finite Fields, Encyclopedia of Mathematics and its Applications 20, Cambridge University Press (1997), Chapter 6, §2.
• B. Schoeneberg, Elliptic Modular Functions, Springer (1974), Chapter IX.

Over a finite field

theorem Matrix.IsSymm.sum_addChar_dotProduct_mulVec_of_card_eq_two_mul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι F} (hA : A.IsSymm) (hF : ringChar F ≠ 2) (hdet : A.det ≠ 0) {k : ℕ} (hι : Fintype.card ι = 2 * k) {R : Type u_3} [CommRing R] [IsDomain R] {ψ : AddChar F R} (hψ : ψ.IsPrimitive) : ∑ x : ι → F, ψ (x ⬝ᵥ A.mulVec x) = ↑((quadraticChar F) ((-1) ^ k * A.det)) * ↑(Fintype.card F) ^ k

The Gauss sum of a nondegenerate quadratic form of even rank over a finite field F of odd characteristic with q elements: if A is a symmetric matrix with det A ≠ 0 indexed by a type with 2k elements and ψ is a primitive additive character of F, then ∑_x ψ(xᵀ A x) = χ((-1)^k det A) q^k, where χ is the quadratic character of F.

Modulo an odd integer

theorem Matrix.IsSymm.sum_stdAddChar_dotProduct_mulVec_of_eq_sq_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℤ} (hA : A.IsSymm) {N M p : ℕ} [NeZero N] [NeZero M] (hN : N = p ^ 2 * M) (hodd : Odd p) (hdet : IsCoprime A.det ↑p) : ∑ x : ι → ZMod N, ZMod.stdAddChar (x ⬝ᵥ (A.map Int.cast).mulVec x) = ↑p ^ Fintype.card ι * ∑ y : ι → ZMod M, ZMod.stdAddChar (y ⬝ᵥ (A.map Int.cast).mulVec y)

Removing a square from the modulus. Let A be a symmetric integer matrix, p an odd natural number prime to det A, and N = p ^ 2 * M. With e(t) = exp (2πi t), the Gauss sum ∑_{x ∈ (ℤ/N)^ι} e(xᵀ A x / N) is p ^ #ι times the Gauss sum ∑_{y ∈ (ℤ/M)^ι} e(yᵀ A y / M).

theorem Matrix.sum_stdAddChar_dotProduct_mulVec_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℤ) {m n : ℕ} [NeZero m] [NeZero n] {u v : ℤ} (huv : u * ↑n + v * ↑m = 1) : ∑ x : ι → ZMod (m * n), ZMod.stdAddChar (x ⬝ᵥ (A.map Int.cast).mulVec x) = (∑ y : ι → ZMod m, ZMod.stdAddChar (y ⬝ᵥ ((u • A).map Int.cast).mulVec y)) * ∑ z : ι → ZMod n, ZMod.stdAddChar (z ⬝ᵥ ((v • A).map Int.cast).mulVec z)

Coprime moduli. For natural numbers m, n and integers u, v with u n + v m = 1, the Gauss sum ∑_{x ∈ (ℤ/mn)^ι} e(xᵀ A x / (m n)), with e(t) = exp (2πi t), is the product of the Gauss sums of u A modulo m and of v A modulo n.

theorem Matrix.IsSymm.sum_stdAddChar_dotProduct_mulVec_eq_jacobiSym {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℤ} (hA : A.IsSymm) {k : ℕ} (hι : Fintype.card ι = 2 * k) {a : ℕ} [NeZero a] (ha : Odd a) (hdet : IsCoprime A.det ↑a) : ∑ x : ι → ZMod a, ZMod.stdAddChar (x ⬝ᵥ (A.map Int.cast).mulVec x) = ↑(jacobiSym ((-1) ^ k * A.det) a) * ↑a ^ k

The Gauss sum of a quadratic form modulo an odd integer. Let A be a symmetric integer matrix indexed by a type with 2k elements, and a an odd modulus prime to det A. With e(t) = exp (2πi t), ∑_{x ∈ (ℤ/a)^ι} e(xᵀ A x / a) = ((-1)^k det A / a) a^k, with the Jacobi symbol (· / a).