Properties of objects stable under retracts

If idempotents split in a category C and an object property P is stable under retracts, then idempotents split in the full subcategory of P: an idempotent of a P-object splits in C through a retract of that object, which again satisfies P. This is how a full subcategory of an abelian category, such as the finitely generated projective modules, inherits the splitting of idempotents that makes indecomposability equivalent to the absence of nontrivial idempotent endomorphisms.

The zero objects form a property stable under retracts, and stability under retracts is inherited by inverse images along functors; in particular, the objects that a functor sends to zero form a property stable under retracts. A property closed under subobjects is stable under retracts.

Conversely, the essential image of a fully faithful functor out of an idempotent-complete category is stable under retracts: a retract of F.obj Z is cut out by an idempotent of F.obj Z, which comes from an idempotent of Z, and its splitting in the source is sent to the retract.

Main results

• CategoryTheory.ObjectProperty.isIdempotentComplete_fullSubcategory: the full subcategory of a property stable under retracts in an idempotent-complete category is idempotent complete.
• CategoryTheory.Functor.essImage_isStableUnderRetracts: the essential image of a fully faithful functor out of an idempotent-complete category is stable under retracts.

instance CategoryTheory.ObjectProperty.isIdempotentComplete_fullSubcategory {C : Type u_1} [Category.{v_1, u_1} C] [IsIdempotentComplete C] (P : ObjectProperty C) [P.IsStableUnderRetracts] : IsIdempotentComplete P.FullSubcategory

A full subcategory stable under retracts of an idempotent-complete category is idempotent complete: an idempotent splits in the ambient category through a retract of its object, which lies in the subcategory again.

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsZero_tauCeti {C : Type u_1} [Category.{v_1, u_1} C] : IsStableUnderRetracts Limits.IsZero

A retract of a zero object is a zero object.

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsInverseImage_tauCeti {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (P : ObjectProperty D) [P.IsStableUnderRetracts] (F : Functor C D) : (P.inverseImage F).IsStableUnderRetracts

The inverse image of a property stable under retracts is stable under retracts, since functors preserve retracts.

@[instance 100]

instance CategoryTheory.ObjectProperty.isStableUnderRetracts_of_isClosedUnderSubobjects {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] : P.IsStableUnderRetracts

A property closed under subobjects is stable under retracts, since the inclusion of a retract is a monomorphism.

instance CategoryTheory.Functor.essImage_isStableUnderRetracts {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [IsIdempotentComplete C] (F : Functor C D) [F.Full] [F.Faithful] : F.essImage.IsStableUnderRetracts

The essential image of a fully faithful functor out of an idempotent-complete category is stable under retracts.