Effective motives are pseudo-abelian: idempotent endomorphisms split
ProvedMilne.idempotent_splitAn idempotent degree-zero endomorphism f of a motive h(X, e), sandwiched by the projector e (so that e f e = f), decomposes the motive into the direct sum of its complement and image summands h(X, e − f) ⊕ h(X, f), expressed through the five biproduct identities of the two inclusions and two projections (Section 6 of the source: the category of motives is pseudo-abelian).
import Mathlib import Definitions.Def_Milne_world import Definitions.Def_Milne_motives import Definitions.Def_Milne_zeta
universe u v
namespace Milne
/-- The category of effective motives is pseudo-abelian (section 6 of the
paper): an idempotent f in the endomorphism ring of a motive
M = h(X, e) decomposes the motive into the direct sum of its kernel and
image summands h(X, e − f) ⊕ h(X, f). The direct sum is expressed
through its projection-inclusion equations. -/
theorem idempotent_split (W : CorrWorld.{u, v}) (M : MotElem W) (f : W.Corr M.X M.X)
(hf : W.cc f f = f) (hdf : W.deg f = 0) (hfe : W.cc (W.cc M.e f) M.e = f) :
∃ i₁ : Hom W (idemCompl W M f hf hdf hfe) M,
∃ i₂ : Hom W (idemImg W M f hf hdf) M,
∃ p₁ : Hom W M (idemCompl W M f hf hdf hfe),
∃ p₂ : Hom W M (idemImg W M f hf hdf),
homComp W i₁ p₁ = idM W (idemCompl W M f hf hdf hfe)
∧ homComp W i₂ p₂ = idM W (idemImg W M f hf hdf)
∧ homComp W i₂ p₁ =
homZero W (idemImg W M f hf hdf) (idemCompl W M f hf hdf hfe)
∧ homComp W i₁ p₂ =
homZero W (idemCompl W M f hf hdf hfe) (idemImg W M f hf hdf)
∧ homAdd W (homComp W p₁ i₁) (homComp W p₂ i₂) = idM W M := by
sorry
end Milne
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: given a motive M = h(X, e) and an idempotent degree-zero correspondence f with e f e = f, there exist morphisms i₁ from the complement summand h(X, e − f) into M and i₂ from the image summand h(X, f) into M, and projections p₁, p₂ in the reverse directions, satisfying the five biproduct identities: the composite of i₁ with p₁ is the identity of the complement summand, the composite of i₂ with p₂ is the identity of the image summand, the two cross composites are the corresponding zero morphisms, and the sum of the composite of p₁ with i₁ and the composite of p₂ with i₂ is the identity of M. A reviewer should check that the splitting is asserted through explicit morphisms satisfying the biproduct equations rather than as an isomorphism with a separately constructed direct-sum object, and that the complement summand carries the correspondence e − f, which the interface axiom on complements keeps idempotent.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.