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 #
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.
- locallySmall : LocallySmall.{w, v, u} C
- hasFilteredColimitsOfSize : Limits.HasFilteredColimitsOfSize.{w, w, v, u} C
- ab5OfSize : AB5OfSize.{w, w, v, u} C
- hasSeparator : HasSeparator C