Limits and colimits in the category of short complexes

In this file, it is shown if a category C with zero morphisms has limits of a certain shape J, then it is also the case of the category ShortComplex C.

TODO (@rioujoel): Do the same for colimits.

def CategoryTheory.ShortComplex.isLimitOfIsLimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (c : CategoryTheory.Limits.Cone F) (h₁ : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₁.mapCone c)) (h₂ : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₂.mapCone c)) (h₃ : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₃.mapCone c)) : CategoryTheory.Limits.IsLimit c

If a cone with values in ShortComplex C is such that it becomes limit when we apply the three projections ShortComplex C ⥤ C, then it is limit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.limitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.Cone F

Construction of a limit cone for a functor J ⥤ ShortComplex C using the limits of the three components J ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isLimitπ₁MapConeLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₁.mapCone (CategoryTheory.ShortComplex.limitCone F))

limitCone F becomes limit after the application of π₁ : ShortComplex C ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isLimitπ₂MapConeLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₂.mapCone (CategoryTheory.ShortComplex.limitCone F))

limitCone F becomes limit after the application of π₂ : ShortComplex C ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isLimitπ₃MapConeLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₃.mapCone (CategoryTheory.ShortComplex.limitCone F))

limitCone F becomes limit after the application of π₃ : ShortComplex C ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isLimitLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.limitCone F)

limitCone F is limit.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ShortComplex.hasLimit_of_hasLimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₁

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₂

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₃

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ShortComplex.hasLimitsOfShape {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.ShortComplex C)

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₁

Equations

• CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₁ = { preservesLimit := fun {K : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} => inferInstance }

noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₂

Equations

• CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₂ = { preservesLimit := fun {K : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} => inferInstance }

noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₃

Equations

• CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₃ = { preservesLimit := fun {K : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} => inferInstance }

instance CategoryTheory.ShortComplex.hasFiniteLimits {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShortComplex C)

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₁

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₂

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₃

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] : CategoryTheory.ShortComplex.π₁.PreservesMonomorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] : CategoryTheory.ShortComplex.π₂.PreservesMonomorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] : CategoryTheory.ShortComplex.π₃.PreservesMonomorphisms

Equations

• ⋯ = ⋯

def CategoryTheory.ShortComplex.isColimitOfIsColimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (c : CategoryTheory.Limits.Cocone F) (h₁ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone c)) (h₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone c)) (h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone c)) : CategoryTheory.Limits.IsColimit c

If a cocone with values in ShortComplex C is such that it becomes colimit when we apply the three projections ShortComplex C ⥤ C, then it is colimit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.colimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.Cocone F

Construction of a colimit cocone for a functor J ⥤ ShortComplex C using the colimits of the three components J ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isColimitπ₁MapCoconeColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))

colimitCocone F becomes colimit after the application of π₁ : ShortComplex C ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isColimitπ₂MapCoconeColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))

colimitCocone F becomes colimit after the application of π₂ : ShortComplex C ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isColimitπ₃MapCoconeColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))

colimitCocone F becomes colimit after the application of π₃ : ShortComplex C ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.isColimitColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.colimitCocone F)

colimitCocone F is colimit.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ShortComplex.hasColimit_of_hasColimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.HasColimit F

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₁

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₂

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₃

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ShortComplex.hasColimitsOfShape {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.ShortComplex C)

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₁

Equations

• CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₁ = { preservesColimit := fun {K : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} => inferInstance }

noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₂

Equations

• CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₂ = { preservesColimit := fun {K : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} => inferInstance }

noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₃

Equations

• CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₃ = { preservesColimit := fun {K : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} => inferInstance }

instance CategoryTheory.ShortComplex.hasFiniteColimits {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.ShortComplex C)

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₁

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₂

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₃

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] : CategoryTheory.ShortComplex.π₁.PreservesEpimorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] : CategoryTheory.ShortComplex.π₂.PreservesEpimorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] : CategoryTheory.ShortComplex.π₃.PreservesEpimorphisms

Equations

• ⋯ = ⋯