Commit 2024-12-16 16:45 3a32603f
View on Github →feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce Grothendieck categories (#18510)
Define Grothendieck categories in a new separate file. According to our definition, a Grothendieck category w.r.t an universe w is an abelian category that is locally small w.r.t w, has exact filtered colimits of size w
(AB5) and has a separator.
Some essential theorems are provided:
- The definition is invariant under equivalences of categories, and in particular, under shrinking the hom sets to size
w
. - Grothendieck categories are have all limits and colimits of size w (completeness and cocompleteness).
In order to facilitate the proofs of the theorems, the new lemma
hasLimits_of_hasColimits_of_hasSeparator
(a variant ofhasLimits_of_hasColimits_of_isSeparating
) and its dual is introduced inAdjunction.AdjointFunctorTheorems
. The moduleAbelian.Transfer
is extended with the induced preadditive and abelian structure ofShrinkHoms
and existing transfer lemmas are generalized so that the hom sets need not have the same universes. Transfer lemmas for separators and coseparators are added toAdjunction.Generator
. Moreover, some notable changes are made inAbelian.GrothendieckAxioms.Basic
. Besides adding@[stacks]
attributes,hasExactColimitsOfShape_of_equiv
is renamed toHasExactColimitsOfShape.of_domain_equivalence
and is afforded a counterpartHasExactColimitsOfShape.of_codomain_equivalence
(with similar changes toHasExactLimitsOfShape
).