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 of hasLimits_of_hasColimits_of_isSeparating) and its dual is introduced in Adjunction.AdjointFunctorTheorems. The module Abelian.Transfer is extended with the induced preadditive and abelian structure of ShrinkHoms 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 to Adjunction.Generator. Moreover, some notable changes are made in Abelian.GrothendieckAxioms.Basic. Besides adding @[stacks] attributes, hasExactColimitsOfShape_of_equiv is renamed to HasExactColimitsOfShape.of_domain_equivalence and is afforded a counterpart HasExactColimitsOfShape.of_codomain_equivalence (with similar changes to HasExactLimitsOfShape).

Estimated changes