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)
:
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]
: