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]
:
(S.map F).ShortExact ā S.ShortExact