Reflecting indecomposability through a functor

A functor preserving zero morphisms and binary biproducts reflects indecomposability at an object if it reflects zero objects on that object's retracts. This local condition is useful for quotient functors: a quotient can kill many objects while killing no nonzero summand of the particular object under consideration.

theorem CategoryTheory.Functor.indecomposable_of_indecomposable_obj_of_reflects_isZero_retract {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroMorphisms D] [Limits.HasBinaryBiproducts D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproducts F] {X : C} (hX : Indecomposable (F.obj X)) (hF : ∀ {Y : C} (a : Retract Y X), Limits.IsZero (F.obj Y) → Limits.IsZero Y) : Indecomposable X

A functor preserving zero morphisms and binary biproducts reflects indecomposability at X if every retract of X whose image is zero is itself zero.