The category of effective motives admits no fiber functor
ProvedMilne.motives_not_tannakianThe tannakian obstruction (Section 6, page 10 of the source): for a world containing a curve of genus at least 2, the category of effective motives admits no fiber functor — no assignment of finite-dimensional Q-vector spaces to motives that acts on morphisms, preserves identities and composition, multiplies dimensions over tensor products, and identifies the trace of the identity endomorphism of each motive with the dimension of its fiber. Under such an assignment the trace of the identity would be a nonnegative dimension, but the trace of the identity of the motive of a curve of genus g is 2 − 2g, which is negative.
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
universe u v
namespace Milne
/-- The tannakian obstruction (section 6 of the paper, page 10): the
category of effective motives admits no fiber functor — there is no
assignment of finite-dimensional ℚ-vector spaces to motives that acts on
morphisms, preserves identities and composition, multiplies dimensions
over tensor products, and identifies the trace of the identity with the
dimension of the fiber. The reason is the paper's: under such an
assignment the trace of the identity is a nonnegative dimension, but for
a curve of genus g ≥ 2 the trace of the identity of its motive is
2 − 2g, which is negative. -/
theorem motives_not_tannakian (W : CorrWorld.{u, v}) (g : ℕ) (hg : 2 ≤ g) :
¬ ∃ F : FibFun W, True := 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 with 2 ≤ g, there does not exist a fiber functor on the effective motives of W: a structure consisting of a natural-number dimension for each motive, an action on morphisms as functions between the finite-dimensional Q-vector spaces they define, preservation of identities and composition, multiplicativity of dimensions over tensor products, and the identification of the trace of the identity endomorphism of each motive with the dimension of its fiber. The obstruction: the trace of the identity on the motive of the curve of genus g is 2 − 2g, which is negative, while a dimension is a natural number; the contradiction is with the nonnegativity of the cast. A reviewer should check that the existential carries a placeholder true conjunction (the structure is the payload), that exactness and faithfulness are deliberately absent from the structure — the obstruction needs only the trace-dimension identity, so the theorem is stronger than the source's formulation, as disclosed — and that genus at least 2 is genuinely required, since genera 0 and 1 give nonnegative traces and the obstruction fails.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.