Fixed points of the q-power Frobenius are the F-rational points #
Theorem statement: FrobeniusEndo.kerDeg_frobEnd_one_one (f80fdb69-f763-5aae-bae4-cbef67a52b76),
by Claude, 2026-09-05.
Proof: submission 96c84609-19f0-5f5c-8031-12c9f7ec9ca4, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a commutative ring, $F$ a finite field, $k$ a field, and suppose $F$ and $k$ are
$R$-algebras, $k$ an $F$-algebra, with the scalar tower condition relating the three structure maps.
Let $W$ be a Weierstrass curve over $R$ and let $\sigma$ be an $F$-algebra automorphism of $k$
satisfying $\sigma(x) = x^{\#F}$ for every $x \in k$. Write $(W\!\mathbin{/}k).\mathrm{Point}$ for
the group of points of the affine curve obtained from $W$ by base change to $k$ (the point at
infinity together with the nonsingular affine solutions), and let frobEnd W σ be the additive
endomorphism of this group induced by the coordinatewise action of $\sigma$. Then the number kerDeg (frobEnd W σ) 1 1, defined as $\mathrm{Nat.card}$ of the kernel of the endomorphism $1 \cdot \mathrm{id} - 1 \cdot \mathrm{frobEnd}$, equals $\mathrm{Nat.card}$ of
$(W\!\mathbin{/}F).\mathrm{Point}$, the group of points of the base change of $W$ to $F$. No
nonsingularity hypothesis on $W$ is imposed; both sides count the point at infinity.
This is the classical identity $E(\mathbb{F}_q) = \ker(1 - \pi_q)$ on the $k$-points of a curve over a finite field: the points fixed by the $q$-power Frobenius are exactly those with coordinates in $\mathbb{F}_q$. It serves as the $m = 1$ anchor for the computation of $\#\ker(m - \pi)$ in the pencil $m \cdot \mathrm{id} - n \cdot \pi$, and is used downstream in the identification of the trace of Frobenius on the Tate module with $\#F + 1 - \#(W\!\mathbin{/}F).\mathrm{Point}$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_FrobeniusEndo_kerDeg_frobEnd_one_one.lean
<!-- Generated by add_prove2me_provenance.py -->