The motive of the projective line is the sum of the unit and the Lefschetz motive
ProvedMilne.p1_motive_splitThe motivic decomposition of the projective line (Sections 5-6 of the source): the diagonal of ℙ¹ decomposes as Δ = e₀ + e₂ into orthogonal idempotents, giving h(ℙ¹, Δ) = h(ℙ¹, e₀) ⊕ h(ℙ¹, e₂) — the paper's h(ℙ¹) = 𝟙 ⊕ 𝕃 — and every endomorphism of the motive of the projective line is a rational combination of the two idempotents, the paper's End(h(ℙ¹)) = ℤ ⊕ ℤ.
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
universe u v
namespace Milne
/-- The motivic decomposition of the projective line (sections 5 and 6 of
the paper): the diagonal of ℙ¹ × ℙ¹ decomposes as Δ = e₀ + e₂ into
orthogonal idempotents, giving h(ℙ¹, Δ) = h(ℙ¹, e₀) ⊕ h(ℙ¹, e₂) — the
paper's h(ℙ¹, Δ) = 𝟙 ⊕ 𝕃 — and every endomorphism of the motive of the
projective line is a ℚ-combination of the two idempotents, the paper's
End(hℙ¹, Δ) = ℤ ⊕ ℤ. -/
theorem p1_motive_split (W : CorrWorld.{u, v}) :
∃ i₀ : Hom W (H0 W) (P1M W),
∃ i₂ : Hom W (L1 W) (P1M W),
∃ p₀ : Hom W (P1M W) (H0 W),
∃ p₂ : Hom W (P1M W) (L1 W),
homComp W i₀ p₀ = idM W (H0 W)
∧ homComp W i₂ p₂ = idM W (L1 W)
∧ homComp W i₂ p₀ = homZero W (L1 W) (H0 W)
∧ homComp W i₀ p₂ = homZero W (H0 W) (L1 W)
∧ homAdd W (homComp W p₀ i₀) (homComp W p₂ i₂) = idM W (P1M W)
∧ ∀ φ : Hom W (P1M W) (P1M W),
∃ a b : ℚ, φ.val = W.add (W.smul a W.e0) (W.smul b W.e2) := 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 there exist morphisms i₀ from the unit summand h(ℙ¹, e₀) and i₂ from the Lefschetz summand h(ℙ¹, e₂) into the motive of the projective line, and projections p₀, p₂ back, satisfying the five biproduct identities — so the motive of the projective line is the direct sum of the two summands — and, in addition, every endomorphism φ of the motive of the projective line is of the form a · e₀ + b · e₂ for rational numbers a and b. A reviewer should check that the span is by rational, not integral, combinations (the source's End is ℤ ⊕ ℤ, and the rational statement is the weaker, correct one for the interface); that the two summands are cut out by the Künneth idempotents e₀ and e₂ supplied by the world, whose orthogonality and diagonal sum are interface data; and that the biproduct identities are the five displayed equations, with the cross composites landing between the two different summands in both directions.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.