Properties of objects that are closed under extensions

Given a category C and P : ObjectProperty C, we define a type class P.IsClosedUnderExtensions expressing that the property is closed under extensions.

class CategoryTheory.ObjectProperty.IsClosedUnderExtensions {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] : Prop

Given P : ObjectProperty C, we say that P is closed under extensions if whenever 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is a short exact short complex, then P X₁ and P X₃ implies P X₂.

• prop_X₂_of_shortExact {S : ShortComplex C} (hS : S.ShortExact) (h₁ : P S.X₁) (h₃ : P S.X₃) : P S.X₂

theorem CategoryTheory.ObjectProperty.prop_X₂_of_shortExact {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [P.IsClosedUnderExtensions] {S : ShortComplex C} (hS : S.ShortExact) (h₁ : P S.X₁) (h₃ : P S.X₃) : P S.X₂

instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsTop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] : ⊤.IsClosedUnderExtensions

instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsIsZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] : IsClosedUnderExtensions Limits.IsZero

instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [P.IsClosedUnderExtensions] (F : Functor D C) [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : (P.inverseImage F).IsClosedUnderExtensions

theorem CategoryTheory.ObjectProperty.prop_biprod {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X₁ X₂ : C} (h₁ : P X₁) (h₂ : P X₂) [Preadditive C] [Limits.HasZeroObject C] [P.IsClosedUnderExtensions] [Limits.HasBinaryBiproduct X₁ X₂] : P (X₁ ⊞ X₂)