Zeta function of the projective line

Proved

WeilConjectures.projectiveLine_zeta

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

algebraic-geometryzeta-function

Let $k=\mathbb F_q$ be a finite field. The projective line $\mathbb P^1_k$ satisfies

N_m(\mathbb P^1_k)=q^m+1\quad(m\ge1),\qquad Z(\mathbb P^1_k,T)=\frac{1}{(1-T)(1-qT)},

that is, $\zeta(\mathbb P^1,s)=1/\big((1-q^{-s})(1-q^{1-s})\big)$ .

This is the simplest example of the Weil conjectures, with $P_0=1-T$ , $P_1=1$ , $P_2=1-qT$ .

Formalization Note The zeta identity is stated as $Z\cdot(1-T)(1-qT)=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 projectiveLine_zeta (p : ℕ) [Fact p.Prime] (k : Type) [Field k] [Finite k] [CharP k p] :
    (∀ m : ℕ, 1 ≤ m → pointCount p (projectiveSpace.toSpec k 1) m = Nat.card k ^ m + 1) ∧
    zetaFunction p (projectiveSpace.toSpec k 1) *
      ((1 - PowerSeries.X) * (1 - PowerSeries.C (Nat.card k : ℚ) * 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 "The projective line"

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