CategoryTheory.ShortComplex.Splitting.shortExact

theorem CategoryTheory.ShortComplex.Splitting.shortExact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C], S.Splitting → S.ShortExact

This theorem states that in the category of short complexes in a preadditive category with a zero object, if a short complex is split, it is also short exact. Here, a short complex is a chain complex with only three nonzero terms, a split complex is one that has splitting of the differentials, and a short exact complex is a complex where the image of one morphism is equal to the kernel of the next.

More concisely: In the category of short complexes of a preadditive category with a zero object, a split complex is short exact.