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} ι]
: