Rationality and functional equation (Grothendieck)

Open

WeilConjectures.rationality_functional_equation

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynumber-theoryzeta-function

Let $k=\mathbb F_q$ be a finite field with $q$ elements, of characteristic $p$ , and let $X$ be a non-singular projective variety of dimension $n$ over $k$ , i.e. $f: X\to\operatorname{Spec}k$ is smooth of relative dimension $n$ , geometrically irreducible and projective. Let $N_m=\#X(\mathbb F_{q^m})$ and $Z(X,T)=\exp\big(\sum_{m\ge1}N_mT^m/m\big)\in\mathbb Q[[T]]$ . Then there are integer polynomials $P_0,\dots,P_{2n}\in\mathbb Z[T]$ and finite multisets $\{\alpha_{ij}\}_j$ of nonzero complex numbers with

Z(X,T)\cdot P_0(T)P_2(T)\cdots P_{2n}(T)=P_1(T)P_3(T)\cdots P_{2n-1}(T),

$P_0(T)=1-T$ , $P_{2n}(T)=1-q^nT$ , and $P_i(T)=\prod_j(1-\alpha_{ij}T)$ in $\mathbb C[T]$ for $1\le i\le 2n-1$ ;

Functional equation: with $E=\sum_{i=0}^{2n}(-1)^i\deg P_i$ and $Z(T)=\prod_{i\text{ odd}}P_i(T)/\prod_{i\text{ even}}P_i(T)$ , there is a sign $\varepsilon=\pm1$ such that

Z\big(q^{-n}t^{-1}\big)=\varepsilon\,q^{nE/2}\,t^{E}\,Z(t)

for every complex $t\ne0$ at which both sides are defined; and for $1\le i\le 2n-1$ the multiset $\{\alpha_{2n-i,j}\}_j$ equals $\{q^n/\alpha_{i,j}\}_j$ .

These are parts 1 and 2 of the Weil conjectures, proved by Grothendieck (1965) with Artin and Verdier via the Lefschetz trace formula and Poincaré duality in $\ell$ -adic cohomology.

Formalization Note The finite field is a type k with [Field k] [Finite k] [CharP k p], $q$ = Nat.card k; $\mathbb F_{q^m}$ is FiniteField.Extension k p m; $N_m$ counts $k$ -morphisms $\operatorname{Spec}\mathbb F_{q^m}\to X$ ; $Z(X,T)$ is zetaFunction p f. Projectivity is a closed immersion into projectiveSpace k N over $k$ . The Euler characteristic $E$ is encoded as the alternating sum of the degrees of the $P_i$ .

Preamble

import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial

Formal statement

namespace WeilConjectures

theorem rationality_functional_equation (p : ℕ) [Fact p.Prime] (k : Type) [Field k] [Finite k] [CharP k p]
    (n : ℕ) (X : Scheme.{0}) (f : X ⟶ Spec (.of k))
    [SmoothOfRelativeDimension n f] [GeometricallyIrreducible f]
    (hproj : IsProjectiveOver k f) :
    ∃ (P : ℕ → ℤ[X]) (α : ℕ → Multiset ℂ),
      zetaFunction p f *
          (∏ i ∈ (Finset.range (2 * n + 1)).filter Even,
            ((P i).map (Int.castRingHom ℚ) : PowerSeries ℚ)) =
        ∏ i ∈ (Finset.range (2 * n + 1)).filter Odd,
            ((P i).map (Int.castRingHom ℚ) : PowerSeries ℚ) ∧
      P 0 = 1 - Polynomial.X ∧
      P (2 * n) = 1 - C ((Nat.card k : ℤ) ^ n) * Polynomial.X ∧
      (∀ i, 1 ≤ i → i ≤ 2 * n - 1 →
        (P i).map (Int.castRingHom ℂ) = ((α i).map fun a => 1 - C a * Polynomial.X).prod ∧
        ∀ a ∈ α i, a ≠ 0) ∧
      (∃ ε : ℂ, (ε = 1 ∨ ε = -1) ∧
        ∀ t : ℂ, t ≠ 0 →
          (∏ i ∈ (Finset.range (2 * n + 1)).filter Even, aeval t (P i)) ≠ 0 →
          (∏ i ∈ (Finset.range (2 * n + 1)).filter Even,
              aeval (((Nat.card k : ℂ) ^ n * t)⁻¹) (P i)) ≠ 0 →
          (∏ i ∈ (Finset.range (2 * n + 1)).filter Odd,
                aeval (((Nat.card k : ℂ) ^ n * t)⁻¹) (P i)) /
              (∏ i ∈ (Finset.range (2 * n + 1)).filter Even,
                aeval (((Nat.card k : ℂ) ^ n * t)⁻¹) (P i)) =
            ε * (((Nat.card k : ℝ) ^ ((n : ℝ) *
                ((∑ i ∈ Finset.range (2 * n + 1), (-1 : ℤ) ^ i * ((P i).natDegree : ℤ) : ℤ) : ℝ)
                  / 2) : ℝ) : ℂ) *
              t ^ (∑ i ∈ Finset.range (2 * n + 1), (-1 : ℤ) ^ i * ((P i).natDegree : ℤ)) *
              ((∏ i ∈ (Finset.range (2 * n + 1)).filter Odd, aeval t (P i)) /
                (∏ i ∈ (Finset.range (2 * n + 1)).filter Even, aeval t (P i)))) ∧
      (∀ i, 1 ≤ i → i ≤ 2 * n - 1 →
        α (2 * n - i) = (α i).map fun a => (Nat.card k : ℂ) ^ n / a) := by sorry

end WeilConjectures

Source

Wikipedia, "Weil conjectures", https://en.wikipedia.org/wiki/Weil_conjectures (PDF snapshot supplied by the proposer, 14 pp.), section "Statement of the Weil conjectures", items 1 and 2; section "Grothendieck's proofs of three of the four conjectures"

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph