Structures · Category theory

CategoryTheory.IsGrothendieckAbelian

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.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Shape

One type argument · adds locallySmall, hasFilteredColimitsOfSize, ab5OfSize, hasSeparator