Theorems · Inductive type · category theory

CategoryTheory.IsGrothendieckAbelian

(C : Type u) → [inst : 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.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Cited by

30 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian