Short Exact Sequences in Abelian Categories

This file contains lemmas about short exact sequences in abelian categories.

theorem CategoryTheory.ShortExact.reflects_shortExact_of_faithful {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {S : ShortComplex C} (hS : (S.map F).ShortExact) : S.ShortExact

theorem CategoryTheory.ShortExact.shortExact_map_iff {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {S : ShortComplex C} [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits F] : (S.map F).ShortExact ↔ S.ShortExact