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.

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 (F.comp (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.

@[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 (F.comp (HomologicalComplex.eval C c n))] (j : J) (x✝ : ι) : ((HomologicalComplex.coneOfHasLimitEval F).π.app j).f x✝ = CategoryTheory.Limits.limit.π (F.comp (HomologicalComplex.eval C c x✝)) 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 (F.comp (HomologicalComplex.eval C c n))] (n : ι) : (HomologicalComplex.coneOfHasLimitEval F).pt.X n = CategoryTheory.Limits.limit (F.comp (HomologicalComplex.eval C c n))

@[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 (F.comp (HomologicalComplex.eval C c n))] (n m : ι) : (HomologicalComplex.coneOfHasLimitEval F).pt.d n m = CategoryTheory.Limits.limMap { app := fun (j : J) => (F.obj j).d n m, naturality := ⋯ }

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 (F.comp (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.instHasLimit {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesLimitsOfShapeEvalOfHasLimitsOfShape {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, 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

• ⋯ = ⋯

instance HomologicalComplex.instHasFiniteLimits {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

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesFiniteLimitsEvalOfHasFiniteLimits {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

• ⋯ = ⋯

instance HomologicalComplex.instMonoFOfHasFiniteLimits {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 L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Mono φ] (n : ι) : CategoryTheory.Mono (φ.f n)

Equations

• ⋯ = ⋯

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.

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 (F.comp (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.

@[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 (F.comp (HomologicalComplex.eval C c n))] (j : J) (n : ι) : ((HomologicalComplex.coconeOfHasColimitEval F).ι.app j).f n = CategoryTheory.Limits.colimit.ι (F.comp (HomologicalComplex.eval C c n)) j

@[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 (F.comp (HomologicalComplex.eval C c n))] (n m : ι) : (HomologicalComplex.coconeOfHasColimitEval F).pt.d n m = CategoryTheory.Limits.colimMap { app := fun (j : J) => (F.obj j).d n m, naturality := ⋯ }

@[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 (F.comp (HomologicalComplex.eval C c n))] (n : ι) : (HomologicalComplex.coconeOfHasColimitEval F).pt.X n = CategoryTheory.Limits.colimit (F.comp (HomologicalComplex.eval C c n))

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 (F.comp (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.instHasColimit {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) [∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] : CategoryTheory.Limits.HasColimit F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesColimitsOfShapeEvalOfHasColimitsOfShape {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, 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

• ⋯ = ⋯

instance HomologicalComplex.instHasFiniteColimits {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

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesFiniteColimitsEvalOfHasFiniteColimits {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

• ⋯ = ⋯

instance HomologicalComplex.instEpiFOfHasFiniteColimits {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 L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Epi φ] (n : ι) : CategoryTheory.Epi (φ.f n)

Equations

• ⋯ = ⋯

theorem HomologicalComplex.preservesLimitsOfShape_of_eval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_4} [CategoryTheory.Category.{u_5, u_4} D] (G : CategoryTheory.Functor D (HomologicalComplex C c)) : (∀ (i : ι), CategoryTheory.Limits.PreservesLimitsOfShape J (G.comp (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.

theorem HomologicalComplex.preservesColimitsOfShape_of_eval {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_4} [CategoryTheory.Category.{u_5, u_4} D] (G : CategoryTheory.Functor D (HomologicalComplex C c)) : (∀ (i : ι), CategoryTheory.Limits.PreservesColimitsOfShape J (G.comp (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.

noncomputable instance HomologicalComplex.instPreservesLimitsOfShapeSingle {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i : ι) : CategoryTheory.Limits.PreservesLimitsOfShape J (HomologicalComplex.single C c i)

Equations

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesColimitsOfShapeSingle {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i : ι) : CategoryTheory.Limits.PreservesColimitsOfShape J (HomologicalComplex.single C c i)

Equations

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesFiniteLimitsSingle {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i : ι) : CategoryTheory.Limits.PreservesFiniteLimits (HomologicalComplex.single C c i)

Equations

• ⋯ = ⋯

noncomputable instance HomologicalComplex.instPreservesFiniteColimitsSingle {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i : ι) : CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.single C c i)

Equations

• ⋯ = ⋯