Documentation

Mathlib.CategoryTheory.ObjectProperty.Extensions

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. We also show that this condition is self-dual: P.op is closed under extensions iff P is.

source
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₂.

Instances
    source
    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₂
    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsTop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
    ⊤.IsClosedUnderExtensions
    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsIsZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
    IsClosedUnderExtensions Limits.IsZero
    source
    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
    source
    theorem CategoryTheory.ObjectProperty.isClosedUnderExtensions_op_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] :
    P.op.IsClosedUnderExtensions ↔ P.IsClosedUnderExtensions

    A property of objects P.op is closed under extensions iff P is, since a short complex in Cᵒᵖ is short exact iff the corresponding short complex in C is.

    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsOppositeOp {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [P.IsClosedUnderExtensions] :
    P.op.IsClosedUnderExtensions
    source
    theorem CategoryTheory.ObjectProperty.isClosedUnderExtensions_unop_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (Q : ObjectProperty Cᵒᵖ) :
    Q.unop.IsClosedUnderExtensions ↔ Q.IsClosedUnderExtensions

    A property of objects Q.unop is closed under extensions iff Q is.

    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsUnopOfOpposite {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderExtensions] :
    Q.unop.IsClosedUnderExtensions
    source
    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₂)