The diagonal equation: exact count

Proved

Weil.card_diagonal_eq_card_add

by tabbott · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Exact point count for a diagonal equation. Let $F$ be a finite field, $d, e \ge 1$ , and let $\chi$ and $\lambda$ be multiplicative characters of $F$ valued in $\mathbb{C}$ of orders exactly $m = \gcd(\#F^\times, d)$ and $n = \gcd(\#F^\times, e)$ . Then

\#\{(x,y) \in F^2 : x^d + y^e = 1\} = \#F + \sum_{i=1}^{m-1}\sum_{j=1}^{n-1} J(\chi^i,\lambda^j).

The main term is $\#F$ , the count one expects from a curve of this shape, and the deviation is a sum of $(m-1)(n-1)$ Jacobi sums. In particular the count is exactly $\#F$ when $m = 1$ or $n = 1$ .

Preamble

import Mathlib.NumberTheory.GaussSum
import Mathlib.NumberTheory.JacobiSum.Basic
import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
import Mathlib.NumberTheory.MulChar.Lemmas
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.GroupTheory.Index
import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Algebra.Field.GeomSum
import Mathlib.Algebra.Order.BigOperators.Group.Finset

set_option autoImplicit false
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

universe u_1 u_2

open AddChar MulChar Finset

Formal statement

namespace Weil
theorem card_diagonal_eq_card_add : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {d e : ℕ} {χ lam : MulChar F ℂ}, d ≠ 0 → e ≠ 0 → orderOf χ = Nat.gcd (Fintype.card Fˣ) d → orderOf lam = Nat.gcd (Fintype.card Fˣ) e → (↑(Finset.card {z : F × F | Prod.fst z ^ d + Prod.snd z ^ e = 1}) : ℂ) = (↑(Fintype.card F) : ℂ) + ∑ i ∈ Finset.Ico 1 (Nat.gcd (Fintype.card Fˣ) d), ∑ j ∈ Finset.Ico 1 (Nat.gcd (Fintype.card Fˣ) e), jacobiSum (χ ^ i) (lam ^ j) := by sorry
end Weil

Source

A. Weil, Numbers of solutions of equations in finite fields, Bull. Amer. Math. Soc. 55 (1949), 497-508 (diagonal equations are the worked example of the Weil conjectures)

View graph