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.

def CategoryTheory.ShortComplex.isLimitOfIsLimitπ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {F : Functor J (ShortComplex C)} (c : Limits.Cone F) (h₁ : Limits.IsLimit (π₁.mapCone c)) (h₂ : Limits.IsLimit (π₂.mapCone c)) (h₃ : Limits.IsLimit (π₃.mapCone c)) : 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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] : 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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] : Limits.IsLimit (π₁.mapCone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] : Limits.IsLimit (π₂.mapCone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] : Limits.IsLimit (π₃.mapCone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] : Limits.IsLimit (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] : Limits.HasLimit F

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

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

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

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

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

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

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

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

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

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

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

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

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

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

def CategoryTheory.ShortComplex.isColimitOfIsColimitπ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {F : Functor J (ShortComplex C)} (c : Limits.Cocone F) (h₁ : Limits.IsColimit (π₁.mapCocone c)) (h₂ : Limits.IsColimit (π₂.mapCocone c)) (h₃ : Limits.IsColimit (π₃.mapCocone c)) : 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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] : 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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] : Limits.IsColimit (π₁.mapCocone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] : Limits.IsColimit (π₂.mapCocone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] : Limits.IsColimit (π₃.mapCocone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] : Limits.IsColimit (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] : Limits.HasColimit F

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

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

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

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

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

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

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

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

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

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

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

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

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

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