Mission: Motives — effective pure motives and the tannakian obstruction

Motivation

Grothendieck introduced the notion of a motive in a letter to Serre in 1964. Among all the objects he was privileged to discover, he wrote, this one appeared to him the most charged with mystery, and the yoga of motives perhaps the most powerful instrument of discovery he had brought to light. The source — James Milne's expository article "Motives — Grothendieck's Dream" — explains what motives are and why Grothendieck valued them so highly. The many good cohomology theories of algebraic geometry — singular, étale, de Rham, crystalline — cannot come from an algebraically defined Q-valued theory, yet they behave as though they did: traces of regular maps are rational and independent of the theory. Grothendieck's answer is a universal cohomology theory with values in a Q-linear category of motives: every good cohomology theory should factor uniquely through it. The construction passes through algebraic cycles modulo an adequate equivalence relation and correspondences; the category so obtained is additive and pseudo-abelian, carries a tensor product satisfying the Künneth formula, and its first computed decomposition is the motive of the projective line, h(P¹) = 𝟙 ⊕ 𝕃, whose endomorphism ring is as small as possible; the trace of the identity on a motive is the Euler-Poincaré characteristic, and the first zeta computations — the point and the projective line — exhibit the mechanism that the Weil conjectures later vindicated in general. The same trace calculus, however, contains the obstruction that Grothendieck's dream runs against: the trace of the identity on the motive of a curve of genus g is 2 − 2g, which is negative for g ≥ 2, so no fiber functor can exist on the category of effective motives and the category cannot be tannakian.

The mission formalizes the definitions and the proved structural theorems of Sections 4-7 of the source: the algebra of correspondences, the category of effective pure motives with its composition, addition, tensor structure, and pseudo-abelian splitting, Grothendieck's decomposition of the motive of the projective line, the trace of the identity as the Euler characteristic, the zeta functions of a point and of the projective line, and — as the goal — the tannakian obstruction: the category of effective motives admits no fiber functor in the presence of a curve of genus at least 2.

The fragment and its conventions

The source is an expository article; the mission formalizes the fragment consisting of the correspondence algebra and the category of effective pure motives (Sections 4-6), the trace calculus (Section 6, page 10), and the first two zeta computations (Section 7), under the following disclosed conventions.

Fourteen conventions deserve disclosure. First, the platform publishes definitions as modules, so the three definition bundles — the correspondence world, the effective motives, and the zeta coefficients — are published as platform definitions (Milne_world, Milne_motives, Milne_zeta) and attached to the proposal as reference items; the theorem drafts import them; and the creation script reads the definition code and the theorem statements directly from the repository modules that the CI has just compiled, so the code posted to the platform is byte-identical to the code whose compilation the CI verified. Second, algebraic geometry is abstract: no varieties, algebraic cycles, Chow groups, or cohomology theories are constructed, since Mathlib has none of this; the primitive datum is a world of correspondences (CorrWorld) — varieties with a product, a designated point, a projective line, and a curve of every genus, and for each pair of varieties a Q-vector space of correspondences carrying a degree function into the integers, composition, diagonals, transposes, exterior products, Künneth idempotents, and trace data — with the moving lemmas and the well-definedness of the products of cycle classes living in the interface fields, so that every theorem carries the world as a hypothesis. Third, correspondences are presented ungraded, with the grading recovered through the degree function: the graded pieces Corr^r(X, Y) are the degree-r elements, and morphisms of motives are the degree-zero correspondences of the source's f ∘ Corr⁰(X, Y)Q ∘ e. Fourth, rational coefficients are baked into the interface: the correspondence spaces are Q-vector spaces, the source's tensoring of cycle groups with Q is not repeated. Fifth, the mission lives in the effective category: the paper's second attempt of Section 5; the twist integer m of h(X, e, m), duals, and the full category M~(k) are out of scope. Sixth, morphisms are rendered as fixed points: the sandwiched image f ∘ Corr(X, Y)_Q ∘ e is the subtype of correspondences γ with f ∘ γ ∘ e = γ and degree zero, which coincides with the image when e and f are idempotent. Seventh, the closure of the sandwiched subspaces under the operations (composition, addition, zero, negation, scalar multiplication, exterior product) is imposed through interface axioms, since these are the stability statements that make the morphism spaces well defined. Eighth, direct sums are stated through the five biproduct identities rather than as an equality with a direct-sum object; the pseudo-abelian splitting is stated through the same identities, with the complement and image summands h(X, e − f) and h(X, f) as the explicit witnesses. Ninth, the tensor structure is defined on objects and morphisms through the exterior product, and the Künneth formula is stated at the level of motives: hX ⊗ hY = h(X × Y). Tenth, the Künneth idempotents of the projective line and of the curves of every genus, the diagonal decompositions Δ = e₀ + e₂ and Δ = π₀ + π₁ + π₂, and the trace values 1, −2g, 1 of the pieces — the signed Betti numbers, so that the trace of the identity is the Euler characteristic — are interface data: the source's computations from the intersection ring of the projective plane and of a curve are thereby carried as hypotheses. Eleventh, the trace of the identity on an idempotent motive is defined through the interface-supplied evaluation and coevaluation correspondences, its additivity over idempotent splits is an interface axiom, and the duality zigzag equations of the source are not stated. Twelfth, the fiber functor is rendered as a concrete structure FibFun — a dimension for each motive, an action on morphisms, preservation of identities and composition, multiplication of dimensions over tensor products, and the identification of the trace of the identity with the dimension of the fiber; exactness and faithfulness are deliberately not hypothesized, because the tannakian obstruction needs only the trace-dimension identity, so the goal theorem is formally stronger than the source's formulation — the strengthening is disclosed — and the fibers are Q-vector spaces, whereas the source allows any field F of characteristic zero. Thirteenth, the zeta function is rendered through its Taylor coefficients via a course-of-values prefix recursion equivalent to the source's logarithmic definition log Z(X, t) = Σ N_m t^m / m; the point counts 1 and 1 + p^m of the point and of the projective line are carried as data, and no finite fields are formalized. Fourteenth, everything is developed against the platform's Mathlib build (0df444a); the read-backs attached to the theorem drafts were authored by the same model that produced the statements (readback_model glm-5-latest-short); they are a self-check, not an independent audit, and human review of every item is required before submission.

Formalization targets

Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.

• The correspondence world (reference): varieties with a product, a point, a projective line, curves of every genus, and Q-vector spaces of correspondences with composition, diagonals, transposes, exterior products, degrees, Künneth idempotents, and trace data (Sections 4-6).
• Effective pure motives (reference): objects h(X, e), morphisms as sandwich-fixed degree-zero correspondences, identity, composition, addition, zero, tensor products, the summands of the projective line, the splitting summands, and the fiber functor structure (Sections 5-6).
• Zeta functions (reference): the Taylor coefficients of the zeta function attached to a point-count sequence, through the prefix recursion (Section 7).
• Effective motives form a category: associativity of composition and the identity laws (Section 5) — milestone.
• Effective motives are pseudo-abelian: an idempotent endomorphism splits the motive into biproduct summands (Section 6) — milestone.
• The tensor product and the Künneth formula: the interchange law, the tensor identity, and hX ⊗ hY = h(X × Y) (Section 6) — milestone.
• The motive of the projective line: h(ℙ¹) = 𝟙 ⊕ 𝕃, and the endomorphism ring is the rational span of the two Künneth idempotents (Sections 5-6) — milestone.
• The trace of the identity on the motive of a curve is its Euler characteristic 2 − 2g (Section 6, p. 10) — milestone.
• The zeta function of a point: all Taylor coefficients are 1 (Section 7) — milestone.
• The zeta function of the projective line: the Taylor coefficients are the partial geometric sums (Section 7) — milestone.
• The tannakian obstruction: no fiber functor exists on the effective motives of a world containing a curve of genus at least 2 (Section 6, p. 10) — the goal.

Significance

The formalized fragment is the additive and tensor skeleton that every theory of motives shares, together with the trace calculus and the first two zeta computations, and it ends with the obstruction that gives the mission its point: as long as the trace of the identity on the motive of a curve is its Euler characteristic, no fiber functor can exist, so the category of effective motives is not tannakian and cannot be the representation category of an affine group scheme — the reason the source gives for passing to larger categories of motives. Formalizing the skeleton with every geometric input isolated as an explicit interface hypothesis produces a reusable shape: the same statements admit any future Mathlib development of algebraic cycles as an instantiation.

Difficulty

The categorical skeleton is pure algebra: associativity, units, biproduct identities, the interchange law, and the splitting of idempotents follow from the interface axioms by equational reasoning; the trace computation is additivity over the Künneth decomposition together with the supplied trace values; the zeta computations are inductions on the coefficient recurrence; the goal is the contradiction between a negative trace and the nonnegativity of a dimension. The difficulty is the discipline of the interface — no statement may silently use a geometric fact that has not been assumed — and the bookkeeping of the course-of-values recursion against the geometric expansion of the reciprocal of (1 − t)(1 − p t).

Formalization scope

Every item quantifies only over the objects it needs — worlds, motives, morphisms, idempotents, genera, point-count sequences. The goal carries a genus parameter together with the hypothesis that the genus is at least two; every world contains a curve of every genus by the interface, so the hypothesis is satisfiable, and it states the source of the obstruction — the middle Künneth summand of a curve of genus at least two has negative trace. This binder is disclosed here rather than left unstated. The negation-free statements produce witnesses: biproducts, splittings, and decompositions produce their morphisms; the zeta identities are equalities of coefficients; the goal is a negation, as is proper for an obstruction. The fragment excludes the twist m ∈ ℤ, duals, rigidity, and tannakianity as a positive property (Sections 5-6), the abelian category M_num and its semisimplicity, Conjectures C and D and the standard conjectures (Section 6), the zeta function of a motive via characteristic polynomials of Frobenius and the Hasse-Weil bound (Sections 2, 7-8), motivic L-functions, the big modularity conjecture, and the conjecture of Birch and Swinnerton-Dyer (Sections 8-9), and mixed motives (Section 10) — everything the source conjectures rather than proves, and everything requiring cohomological realization, is out of scope. The mission formalizes what the source proves.

Selected references

• J. S. Milne, Motives — Grothendieck's Dream, v2.04, April 24, 2012 — the mission's source.
• A. Grothendieck, letter to J.-P. Serre, 1964 — the introduction of the notion of motif.
• S. L. Kleiman, Motives, in Algebraic Geometry, Oslo 1970 — the first detailed exposition of the standard conjectures.
• U. Jannsen, S. L. Kleiman, J.-P. Serre (eds.), Motives, Proceedings of Symposia in Pure Mathematics 55, American Mathematical Society, 1994 — the standard reference, including Scholl's detailed construction of the category of motives.