Grothendieck categories

This file defines Grothendieck categories and proves basic facts about them.

Definitions

A Grothendieck category according to the Stacks project is an abelian category provided that it has AB5 and a separator. However, this definition is not invariant under equivalences of categories. Therefore, if C is an abelian category, the class IsGrothendieckAbelian.{w} C has a weaker definition that is also satisfied for categories that are merely equivalent to a Grothendieck category in the former strict sense.

Theorems

The invariance under equivalences of categories is established in IsGrothendieckAbelian.of_equivalence.

In particular, ShrinkHoms.isGrothendieckAbelian C shows that ShrinkHoms C satisfies our definition of a Grothendieck category after shrinking its hom sets, which coincides with the strict definition in this case.

Relevant implications of IsGrothendieckAbelian are established in IsGrothendieckAbelian.hasLimits and IsGrothendieckAbelian.hasColimits.

References

• Stacks: Grothendieck's AB conditions

class CategoryTheory.IsGrothendieckAbelian (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : Prop

If C is an abelian category, we shall say that it satisfies IsGrothendieckAbelian.{w} C if it is locally small (relative to w), has exact filtered colimits of size w (AB5) and has a separator. If [Category.{v} C] and w = v, this means that C satisfies AB5 and has a separator; general results about Grothendieck abelian categories can be reduced to this case using the instance ShrinkHoms.isGrothendieckAbelian below.

The introduction of the auxiliary universe w shall be needed for certain applications to categories of sheaves. That the present definition still preserves essential properties of Grothendieck categories is ensured by IsGrothendieckAbelian.of_equivalence, which shows that every instance for C implies an instance for ShrinkHoms C with hom sets in Type w.

Stacks Tag 079B

• locallySmall : CategoryTheory.LocallySmall.{w, v, u} C
• hasFilteredColimitsOfSize : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C
• ab5OfSize : CategoryTheory.AB5OfSize.{w, w, v, u} C
• hasSeparator : CategoryTheory.HasSeparator C

theorem CategoryTheory.IsGrothendieckAbelian.of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] [CategoryTheory.IsGrothendieckAbelian C] (α : C ≌ D) : CategoryTheory.IsGrothendieckAbelian D

instance CategoryTheory.ShrinkHoms.isGrothendieckAbelian (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian C] : CategoryTheory.IsGrothendieckAbelian (CategoryTheory.ShrinkHoms.{u} C)

instance CategoryTheory.IsGrothendieckAbelian.hasColimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian C] : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C

instance CategoryTheory.IsGrothendieckAbelian.hasLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian C] : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C