Points on nondegenerate quadrics over a finite field

Let F be a finite field of odd characteristic with q elements and quadratic character χ. For a nondegenerate quadratic form Q in n variables over F with discriminant Δ, the number N(c) of solutions of Q(x) = c depends only on n, on χ of the signed discriminant, and on c only through χ(c) in odd rank and through whether c vanishes in even rank:

n = 2m + 1:  N(c) = q^{2m} + χ((-1)^m Δ c) q^m,
n = 2m + 2:  N(c) = q^{2m+1} + χ((-1)^{m+1} Δ) q^m ν(c),  where ν(0) = q - 1, ν(c) = -1 for c ≠ 0.

For n = 1 this is the count 1 + χ(c / a) of the square roots of c / a, which is Mathlib's quadraticChar_card_sqrts. In general the formulas are proved for diagonal forms ∑ wᵢ xᵢ² with all wᵢ ≠ 0, with Δ = ∏ wᵢ, by adding one variable at a time: adding the term a t² turns the count N into c ↦ qⁿ + ∑ᵤ χ(a u) N(c - u), and the two parities alternate, the odd-to-even step evaluating the Jacobi sum ∑ᵤ χ(u (c - u)) with TauCeti.sum_quadraticChar_mul_sub. Since every symmetric matrix is congruent to a diagonal one when 2 is invertible, the same formulas count the solutions of xᵀ A x = c for a symmetric matrix A with det A ≠ 0, with Δ = det A.

These are the point counts from which the orders of the finite orthogonal groups, and with them the local densities of an integral lattice at the primes not dividing twice its determinant, are computed.

Main results

• TauCeti.card_sum_mul_sq_eq_of_card_eq_two_mul_add_one, TauCeti.card_sum_mul_sq_eq_of_card_eq_two_mul_add_two: the number of solutions of ∑ wᵢ xᵢ² = c in odd and in even rank.
• Matrix.IsSymm.card_dotProduct_mulVec_eq_of_card_eq_two_mul_add_one, Matrix.IsSymm.card_dotProduct_mulVec_eq_of_card_eq_two_mul_add_two: the number of solutions of xᵀ A x = c for a nondegenerate symmetric matrix A, in odd and in even rank.

References

• R. Lidl and H. Niederreiter, Finite Fields, Encyclopedia of Mathematics and its Applications 20, Cambridge University Press (1997), Theorems 6.26 and 6.27.
• K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Graduate Texts in Mathematics 84, Springer (1990), Chapter 8, §6.

theorem TauCeti.card_sum_mul_sq_eq_of_card_eq_two_mul_add_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {ι : Type u_2} [Fintype ι] [DecidableEq ι] {m : ℕ} (hι : Fintype.card ι = 2 * m + 1) {w : ι → F} (hw : ∀ (i : ι), w i ≠ 0) (c : F) : ↑{x : ι → F | ∑ i : ι, w i * x i ^ 2 = c}.card = ↑(Fintype.card F) ^ (2 * m) + (quadraticChar F) (((-1) ^ m * ∏ i : ι, w i) * c) * ↑(Fintype.card F) ^ m

Points on a diagonal quadric in odd rank. Over a finite field of odd characteristic with q elements, if w : ι → F has nonzero entries and ι has 2m + 1 elements, then ∑ wᵢ xᵢ² = c has q^{2m} + χ((-1)^m (∏ wᵢ) c) q^m solutions.

theorem TauCeti.card_sum_mul_sq_eq_of_card_eq_two_mul_add_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {ι : Type u_2} [Fintype ι] [DecidableEq ι] {m : ℕ} (hι : Fintype.card ι = 2 * m + 2) {w : ι → F} (hw : ∀ (i : ι), w i ≠ 0) (c : F) : ↑{x : ι → F | ∑ i : ι, w i * x i ^ 2 = c}.card = ↑(Fintype.card F) ^ (2 * m + 1) + (quadraticChar F) ((-1) ^ (m + 1) * ∏ i : ι, w i) * ↑(Fintype.card F) ^ m * if c = 0 then ↑(Fintype.card F) - 1 else -1

Points on a diagonal quadric in even rank. Over a finite field of odd characteristic with q elements, if w : ι → F has nonzero entries and ι has 2m + 2 elements, then ∑ wᵢ xᵢ² = c has q^{2m+1} + χ((-1)^{m+1} ∏ wᵢ) q^m ν(c) solutions, where ν(0) = q - 1 and ν(c) = -1 for c ≠ 0.

theorem Matrix.IsSymm.card_dotProduct_mulVec_eq_of_card_eq_two_mul_add_one {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) {m : ℕ} (hι : Fintype.card ι = 2 * m + 1) (c : F) : ↑{x : ι → F | x ⬝ᵥ A.mulVec x = c}.card = ↑(Fintype.card F) ^ (2 * m) + (quadraticChar F) ((-1) ^ m * A.det * c) * ↑(Fintype.card F) ^ m

Points on a nondegenerate quadric in odd rank. Over a finite field of odd characteristic with q elements, if A is a symmetric matrix with det A ≠ 0 indexed by a type with 2m + 1 elements, then xᵀ A x = c has q^{2m} + χ((-1)^m det A · c) q^m solutions.

theorem Matrix.IsSymm.card_dotProduct_mulVec_eq_of_card_eq_two_mul_add_two {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) {m : ℕ} (hι : Fintype.card ι = 2 * m + 2) (c : F) : ↑{x : ι → F | x ⬝ᵥ A.mulVec x = c}.card = ↑(Fintype.card F) ^ (2 * m + 1) + (quadraticChar F) ((-1) ^ (m + 1) * A.det) * ↑(Fintype.card F) ^ m * if c = 0 then ↑(Fintype.card F) - 1 else -1

Points on a nondegenerate quadric in even rank. Over a finite field of odd characteristic with q elements, if A is a symmetric matrix with det A ≠ 0 indexed by a type with 2m + 2 elements, then xᵀ A x = c has q^{2m+1} + χ((-1)^{m+1} det A) q^m ν(c) solutions, where ν(0) = q - 1 and ν(c) = -1 for c ≠ 0.