Exactness from short exact sequences

An additive functor between abelian categories that carries short exact sequences to short exact sequences preserves finite limits and finite colimits. Mathlib supplies the equivalence as CategoryTheory.Functor.exact_tfae, whose first and fourth entries are exactly the hypothesis and the pair of conclusions; the general results below are the named projections of that equivalence, and the third of them records the intermediate entry, preservation of homology.

theorem RS.preservesFiniteLimits_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact) : CategoryTheory.Limits.PreservesFiniteLimits F

A functor carrying short exact sequences to short exact sequences preserves finite limits.

theorem RS.preservesFiniteColimits_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact) : CategoryTheory.Limits.PreservesFiniteColimits F

A functor carrying short exact sequences to short exact sequences preserves finite colimits.

theorem RS.preservesHomology_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (h : ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact) : F.PreservesHomology

A functor carrying short exact sequences to short exact sequences preserves homology. This is the intermediate entry of the same equivalence, from which both preservation statements above are read off.