Prove2Me

The diagonal equation as m+nm + n plus a double Jacobi sum

Proved
Weil.card_diagonal_complex

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let FF be a finite field, d,e≥1d, e \ge 1, and let χ\chi and λ\lambda be multiplicative characters of FF valued in C\mathbb{C} of orders exactly m=gcd⁡(#F×,d)m = \gcd(\#F^\times, d) and n=gcd⁡(#F×,e)n = \gcd(\#F^\times, e). Then

#{(x,y)∈F2:xd+ye=1}=m+n+∑i<m∑j<nJ(χi,λj).\#\{(x,y) \in F^2 : x^d + y^e = 1\} = m + n + \sum_{i<m}\sum_{j<n} J(\chi^i, \lambda^j).

The terms mm and nn are the corrections at u=1u = 1 and u=0u = 0, where the character expansion of the fibre count fails because a multiplicative character vanishes at 00.

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_complex : ∀ {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}) : ℂ) = (↑(Nat.gcd (Fintype.card Fˣ) d) : ℂ) + (↑(Nat.gcd (Fintype.card Fˣ) e) : ℂ) + ∑ i ∈ Finset.range (Nat.gcd (Fintype.card Fˣ) d), ∑ j ∈ Finset.range (Nat.gcd (Fintype.card Fˣ) e), jacobiSum (χ ^ i) (lam ^ j) := by sorry
end Weil
Source
Ireland & Rosen, A Classical Introduction to Modern Number Theory, 2nd ed., Springer GTM 84, Ch. 8 (Gauss and Jacobi Sums), Sections 8.3 and 8.5

View graph