Homological complexes in a Grothendieck abelian category #
Let c : ComplexShape ι be a complex shape with no loop, and
such that Small.{w} ι. Then, if C is a Grothendieck abelian
category (with IsGrothendieckAbelian.{w} C), the category
HomologicalComplex C c is Grothendieck abelian.
instance HomologicalComplex.locallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.LocallySmall.{w, v, u} C] [Small.{w, t} ι] :
instance HomologicalComplex.instHasFilteredColimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C] :
instance HomologicalComplex.hasExactColimitsOfShape (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] (J : Type w) [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] :
instance HomologicalComplex.ab5OfSize (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.AB5OfSize.{w', w, v, u} C] :
instance HomologicalComplex.isGrothendieckAbelian (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] [c.HasNoLoop] [Small.{w, t} ι] :