Effective motives form a category
ProvedMilne.mot_category_axiomsThe category axioms for the category of effective pure motives (Section 5 of the source: "Correspondences compose, and so this is a category"): composition of morphisms — sandwich-fixed degree-zero correspondences — is associative, and the idempotent correspondence of a motive is a two-sided identity for composition.
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
universe u v
namespace Milne
/-- The category axioms for the category of effective motives (section 5
of the paper: "Correspondences compose, and so this is a category"):
composition of morphisms is associative, and the idempotent correspondence
of a motive is a two-sided identity for composition. -/
theorem mot_category_axioms (W : CorrWorld.{u, v}) (M N P Q : MotElem W)
(f : Hom W M N) (g : Hom W N P) (h : Hom W P Q) :
homComp W (homComp W f g) h = homComp W f (homComp W g h)
∧ homComp W (idM W M) f = f
∧ homComp W f (idM W N) = f := 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, any four effective motives M, N, P, Q and any morphisms f from M to N, g from N to P, and h from P to Q, the composite of the composite of f and g with h equals the composite of f with the composite of g and h; and composing the identity morphism of M with f, or f with the identity morphism of N, returns f. The identity morphism of a motive is its idempotent correspondence, and morphisms are degree-zero correspondences fixed under the sandwich with the two projectors. A reviewer should check that both identity laws are stated (left and right), that the associativity is the three-fold composite equality in the displayed order, and that the statement quantifies over an arbitrary world, so it is a theorem schema about the interface, not about one fixed model.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.