Split short exact sequences and additive functors

A short exact sequence whose epimorphism admits a section is split, and a split sequence stays split — hence short exact — under any additive functor. This is the mechanism by which the fibre functor of RS.Classical.Deligne.FibreAdditive is seen to carry short exact sequences to short exact sequences: base change produces a section of the epimorphism, and the splitting is then transported by additivity alone, with no exactness hypothesis on the functor.

Both steps are available in Mathlib. The splitting induced by a section is CategoryTheory.ShortComplex.Splitting.ofExactOfSection, which needs only a balanced preadditive category, and the transport is CategoryTheory.ShortComplex.Splitting.map followed by CategoryTheory.ShortComplex.Splitting.shortExact. The three two results below are the packaged forms used in this development, naming the general statements at the shape in which they are consumed.

noncomputable def RS.ShortComplex.ShortExact.splittingOfSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (s : S.X₃ ⟶ S.X₂) (hs : CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃) : S.Splitting

A section of the epimorphism splits a short exact sequence. The retraction is the factorization of 𝟙 - g ≫ s through the kernel f.

Equations

• RS.ShortComplex.ShortExact.splittingOfSplitEpi hS s hs = CategoryTheory.ShortComplex.Splitting.ofExactOfSection S ⋯ s hs ⋯