The tensor product of motives and the Künneth formula
ProvedMilne.tensor_interchange_kunnethThe tensor structure of Section 6 of the source: the exterior product of morphisms composes componentwise (the interchange law), the exterior product of the identities of two motives is the identity of their tensor product, and the Künneth formula holds for the functor X ↦ hX: hX ⊗ hY = h(X × Y).
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
universe u v
namespace Milne
/-- The tensor structure and the Künneth formula (section 6 of the
paper): the exterior product of morphisms composes componentwise, the
exterior product of identities is the identity of the tensor product, and
the Künneth formula holds for the functor X ↦ hX:
hX ⊗ hY = h(X × Y). -/
theorem tensor_interchange_kunneth (W : CorrWorld.{u, v}) (X Y : W.Var)
(M M' N N' P P' : MotElem W)
(f : Hom W M N) (g : Hom W N P) (f' : Hom W M' N') (g' : Hom W N' P') :
crossHom W (homComp W f g) (homComp W f' g') =
homComp W (crossHom W f f') (crossHom W g g')
∧ crossHom W (idM W M) (idM W N) = idM W (tensorObj W M N)
∧ tensorObj W (hOf W X) (hOf W Y) = hOf W (W.prod X Y) := by
sorry
end Milne
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement asserts three identities in any world of correspondences W. First, the interchange law: for parallel pairs of morphisms f from M to N, g from N to P and f′ from M′ to N′, g′ from N′ to P′, the exterior product of the composite of f with g and the composite of f′ with g′ equals the composite of the exterior product of f and f′ with the exterior product of g and g′. Second, the tensor identity: the exterior product of the identity morphisms of M and N is the identity morphism of the tensor product of M and N. Third, the Künneth formula: for any two varieties X and Y, the tensor product of the motives hX and hY is the motive of the product variety: the pair (X × Y, the exterior product of the two diagonals) is literally the pair (X × Y, diagonal of X × Y), using the interface axiom that the exterior product of the diagonals is the diagonal of the product. A reviewer should check the variance of the interchange law and that the Künneth identity is on the nose for the functor h from varieties to motives, not up to isomorphism.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.