The trace of the identity on the motive of a curve is its Euler characteristic
ProvedMilne.curve_trace_eulerFor a curve of genus g, the three Künneth idempotents decompose the motive, the trace is additive over the decomposition, and the pieces carry the signed Betti numbers 1, −2g, 1; the trace of the identity endomorphism of the motive of the curve is therefore 2 − 2g, the Euler-Poincaré characteristic (Section 6, page 10 of the source: Tr(id | hX) = Σ (−1)ⁱ bᵢ).
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
universe u v
namespace Milne
/-- The trace of the identity on the motive of a curve is the
Euler-Poincaré characteristic (section 6 of the paper, page 10): for a
curve of genus g, the Künneth idempotents of the curve decompose the
motive, the trace is additive over the decomposition, and the pieces carry
the signed Betti numbers 1, −2g, 1, so the trace of the identity of
the motive of the curve is 2 − 2g. -/
theorem curve_trace_euler (W : CorrWorld.{u, v}) (g : ℕ) :
W.trId (W.curve g) (W.delta (W.curve g)) = (2 : ℚ) - 2 * (g : ℚ) := by
sorry
end Milne
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for any world of correspondences W and any genus g, the trace of the identity on the motive of the curve of genus g — the interface value of the trace functional on the pair (the curve, its diagonal) — equals the rational number 2 − 2g. The intended proof applies the additivity of the trace over the Künneth decomposition of the diagonal into the three idempotents twice, and then uses the supplied trace values of the pieces: 1, −2g, and 1. A reviewer should check the sign convention — the middle piece contributes −2g, so the total is 2 − 2g, which is negative exactly for genus at least 2 — and that the statement is about the trace attached to the motive of the curve, with the cohomological reading (Betti numbers) only in the commentary, not in the statement.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.