Zeta function of projective space

Proved

WeilConjectures.projectiveSpace_zeta

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

algebraic-geometryzeta-function

Let $k=\mathbb F_q$ and $n\ge0$ . Projective $n$ -space satisfies

N_m(\mathbb P^n_k)=1+q^m+q^{2m}+\cdots+q^{nm}\quad(m\ge1),\qquad Z(\mathbb P^n_k,T)=\frac{1}{(1-T)(1-qT)\cdots(1-q^nT)}.

Projective space is the basic example in which all parts of the Weil conjectures can be checked directly.

Formalization Note The zeta identity is stated as $Z\cdot\prod_{i=0}^n(1-q^iT)=1$ in $\mathbb Q[[T]]$ .

Preamble

import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial

Formal statement

namespace WeilConjectures

theorem projectiveSpace_zeta (p : ℕ) [Fact p.Prime] (k : Type) [Field k] [Finite k] [CharP k p] (n : ℕ) :
    (∀ m : ℕ, 1 ≤ m →
      pointCount p (projectiveSpace.toSpec k n) m = ∑ i ∈ Finset.range (n + 1), Nat.card k ^ (i * m)) ∧
    zetaFunction p (projectiveSpace.toSpec k n) *
      ∏ i ∈ Finset.range (n + 1), (1 - PowerSeries.C ((Nat.card k : ℚ) ^ i) * PowerSeries.X) = 1 := by sorry

end WeilConjectures

Source

Wikipedia, "Weil conjectures", https://en.wikipedia.org/wiki/Weil_conjectures (PDF snapshot supplied by the proposer, 14 pp.), section "Examples", subsection "Projective space"

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