Limits and colimits in the category of homological complexes

In this file, it is shown that if a category C has (co)limits of shape J, then it is also the case of the categories HomologicalComplex C c, and the evaluation functors eval C c i : HomologicalComplex C c ⥤ C commute to these.

def HomologicalComplex.isLimitOfEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) (s : CategoryTheory.Limits.Cone F) (hs : (i : ι) → CategoryTheory.Limits.IsLimit ((HomologicalComplex.eval C c i).mapCone s)) : CategoryTheory.Limits.IsLimit s

A cone in HomologicalComplex C c is limit if the induced cones obtained by applying eval C c i : HomologicalComplex C c ⥤ C for all i are limit.

Equations

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

@[simp]

theorem HomologicalComplex.coneOfHasLimitEval_pt_d {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (n : ι) (m : ι) : (HomologicalComplex.coneOfHasLimitEval F).pt.d n m = CategoryTheory.Limits.limMap (CategoryTheory.NatTrans.mk fun (j : J) => (F.toPrefunctor.obj j).d n m)

@[simp]

theorem HomologicalComplex.coneOfHasLimitEval_π_app_f {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (j : J) (n : ι) : ((HomologicalComplex.coneOfHasLimitEval F).π.app j).f n = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n)) j

@[simp]

theorem HomologicalComplex.coneOfHasLimitEval_pt_X {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (n : ι) : (HomologicalComplex.coneOfHasLimitEval F).pt.X n = CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))

noncomputable def HomologicalComplex.coneOfHasLimitEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.Cone F

A cone for a functor F : J ⥤ HomologicalComplex C c which is given in degree n by the limit F ⋙ eval C c n.

Equations

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

noncomputable def HomologicalComplex.isLimitConeOfHasLimitEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.IsLimit (HomologicalComplex.coneOfHasLimitEval F)

The cone coneOfHasLimitEval F is limit.

Equations

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

instance HomologicalComplex.instHasLimitHomologicalComplexInstCategoryHomologicalComplex {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.HasLimit F

Equations

• (_ : CategoryTheory.Limits.HasLimit F) = (_ : CategoryTheory.Limits.HasLimit F)

noncomputable instance HomologicalComplex.instPreservesLimitHomologicalComplexInstCategoryHomologicalComplexEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (n : ι) : CategoryTheory.Limits.PreservesLimit F (HomologicalComplex.eval C c n)

Equations

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

instance HomologicalComplex.instHasLimitsOfShapeHomologicalComplexInstCategoryHomologicalComplex {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (HomologicalComplex C c)

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J (HomologicalComplex C c)) = (_ : CategoryTheory.Limits.HasLimitsOfShape J (HomologicalComplex C c))

noncomputable instance HomologicalComplex.instPreservesLimitsOfShapeHomologicalComplexInstCategoryHomologicalComplexEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] (n : ι) : CategoryTheory.Limits.PreservesLimitsOfShape J (HomologicalComplex.eval C c n)

Equations

• HomologicalComplex.instPreservesLimitsOfShapeHomologicalComplexInstCategoryHomologicalComplexEval n = CategoryTheory.Limits.PreservesLimitsOfShape.mk

instance HomologicalComplex.instHasFiniteLimitsHomologicalComplexInstCategoryHomologicalComplex {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (HomologicalComplex C c)

Equations

• (_ : CategoryTheory.Limits.HasFiniteLimits (HomologicalComplex C c)) = (_ : CategoryTheory.Limits.HasFiniteLimits (HomologicalComplex C c))

noncomputable instance HomologicalComplex.instPreservesFiniteLimitsHomologicalComplexInstCategoryHomologicalComplexEval {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] (n : ι) : CategoryTheory.Limits.PreservesFiniteLimits (HomologicalComplex.eval C c n)

Equations

• HomologicalComplex.instPreservesFiniteLimitsHomologicalComplexInstCategoryHomologicalComplexEval n = CategoryTheory.Limits.PreservesFiniteLimits.mk

instance HomologicalComplex.instMonoXF {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Mono φ] (n : ι) : CategoryTheory.Mono (φ.f n)

Equations

• (_ : CategoryTheory.Mono (φ.f n)) = (_ : CategoryTheory.Mono ((HomologicalComplex.eval C c n).toPrefunctor.map φ))

def HomologicalComplex.isColimitOfEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) (s : CategoryTheory.Limits.Cocone F) (hs : (i : ι) → CategoryTheory.Limits.IsColimit ((HomologicalComplex.eval C c i).mapCocone s)) : CategoryTheory.Limits.IsColimit s

A cocone in HomologicalComplex C c is colimit if the induced cocones obtained by applying eval C c i : HomologicalComplex C c ⥤ C for all i are colimit.

Equations

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

@[simp]

theorem HomologicalComplex.coconeOfHasColimitEval_pt_X {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (n : ι) : (HomologicalComplex.coconeOfHasColimitEval F).pt.X n = CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))

@[simp]

theorem HomologicalComplex.coconeOfHasColimitEval_pt_d {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (n : ι) (m : ι) : (HomologicalComplex.coconeOfHasColimitEval F).pt.d n m = CategoryTheory.Limits.colimMap (CategoryTheory.NatTrans.mk fun (j : J) => (F.toPrefunctor.obj j).d n m)

@[simp]

theorem HomologicalComplex.coconeOfHasColimitEval_ι_app_f {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (j : J) (n : ι) : ((HomologicalComplex.coconeOfHasColimitEval F).ι.app j).f n = CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n)) j

noncomputable def HomologicalComplex.coconeOfHasColimitEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.Cocone F

A cocone for a functor F : J ⥤ HomologicalComplex C c which is given in degree n by the colimit of F ⋙ eval C c n.

Equations

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

noncomputable def HomologicalComplex.isColimitCoconeOfHasColimitEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.IsColimit (HomologicalComplex.coconeOfHasColimitEval F)

The cocone coconeOfHasLimitEval F is colimit.

Equations

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

instance HomologicalComplex.instHasColimitHomologicalComplexInstCategoryHomologicalComplex {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.HasColimit F

Equations

• (_ : CategoryTheory.Limits.HasColimit F) = (_ : CategoryTheory.Limits.HasColimit F)

noncomputable instance HomologicalComplex.instPreservesColimitHomologicalComplexInstCategoryHomologicalComplexEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (HomologicalComplex.eval C c n))] (n : ι) : CategoryTheory.Limits.PreservesColimit F (HomologicalComplex.eval C c n)

Equations

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

instance HomologicalComplex.instHasColimitsOfShapeHomologicalComplexInstCategoryHomologicalComplex {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (HomologicalComplex C c)

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J (HomologicalComplex C c)) = (_ : CategoryTheory.Limits.HasColimitsOfShape J (HomologicalComplex C c))

noncomputable instance HomologicalComplex.instPreservesColimitsOfShapeHomologicalComplexInstCategoryHomologicalComplexEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] (n : ι) : CategoryTheory.Limits.PreservesColimitsOfShape J (HomologicalComplex.eval C c n)

Equations

• HomologicalComplex.instPreservesColimitsOfShapeHomologicalComplexInstCategoryHomologicalComplexEval n = CategoryTheory.Limits.PreservesColimitsOfShape.mk

instance HomologicalComplex.instHasFiniteColimitsHomologicalComplexInstCategoryHomologicalComplex {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (HomologicalComplex C c)

Equations

• (_ : CategoryTheory.Limits.HasFiniteColimits (HomologicalComplex C c)) = (_ : CategoryTheory.Limits.HasFiniteColimits (HomologicalComplex C c))

noncomputable instance HomologicalComplex.instPreservesFiniteColimitsHomologicalComplexInstCategoryHomologicalComplexEval {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] (n : ι) : CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.eval C c n)

Equations

• HomologicalComplex.instPreservesFiniteColimitsHomologicalComplexInstCategoryHomologicalComplexEval n = CategoryTheory.Limits.PreservesFiniteColimits.mk

instance HomologicalComplex.instEpiXF {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Epi φ] (n : ι) : CategoryTheory.Epi (φ.f n)

Equations

• (_ : CategoryTheory.Epi (φ.f n)) = (_ : CategoryTheory.Epi ((HomologicalComplex.eval C c n).toPrefunctor.map φ))

def HomologicalComplex.preservesLimitsOfShapeOfEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_4} [CategoryTheory.Category.{u_7, u_4} D] (G : CategoryTheory.Functor D (HomologicalComplex C c)) : ((i : ι) → CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Functor.comp G (HomologicalComplex.eval C c i))) → CategoryTheory.Limits.PreservesLimitsOfShape J G

A functor D ⥤ HomologicalComplex C c preserves limits of shape J if for any i, G ⋙ eval C c i does.

Equations

• HomologicalComplex.preservesLimitsOfShapeOfEval G x = CategoryTheory.Limits.PreservesLimitsOfShape.mk

def HomologicalComplex.preservesColimitsOfShapeOfEval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_4} [CategoryTheory.Category.{u_7, u_4} D] (G : CategoryTheory.Functor D (HomologicalComplex C c)) : ((i : ι) → CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Functor.comp G (HomologicalComplex.eval C c i))) → CategoryTheory.Limits.PreservesColimitsOfShape J G

A functor D ⥤ HomologicalComplex C c preserves colimits of shape J if for any i, G ⋙ eval C c i does.

Equations

• HomologicalComplex.preservesColimitsOfShapeOfEval G x = CategoryTheory.Limits.PreservesColimitsOfShape.mk