Grothendieck Axioms

This file defines some of the Grothendieck Axioms for abelian categories, and proves basic facts about them.

Definitions

• AB4 -- a category satisfies AB4 provided that coproducts are exact.
• AB5 -- a category satisfies AB5 provided that filtered colimits are exact.
• The duals of the above definitions, called AB4Star and AB5Star.

Theorems

• The implication from AB5 to AB4 is established in AB4.ofAB5.

Remarks

For AB4 and AB5, we only require left exactness as right exactness is automatic. A comparison with Grothendieck's original formulation of the properties can be found in the comments of the linked Stacks page. Exactness as the preservation of short exact sequences is introduced in CategoryTheory.Abelian.Exact.

We do not require Abelian in the definition of AB4 and AB5 because these classes represent individual axioms. An AB4 category is an abelian category satisfying AB4, and similarly for AB5.

Projects

• Add additional axioms, especially define Grothendieck categories.

References

• Stacks: Grothendieck's AB conditions

class CategoryTheory.AB4 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] : Prop

A category C which has coproducts is said to have AB4 provided that coproducts are exact.

• preservesFiniteLimits : ∀ (α : Type v), CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

  Exactness of coproducts stated as colim : (Discrete α ⥤ C) ⥤ C preserving limits.

class CategoryTheory.AB4Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : Prop

A category C which has products is said to have AB4Star (in literature AB4*) provided that products are exact.

• preservesFiniteColimits : ∀ (α : Type v), CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim

  Exactness of products stated as lim : (Discrete α ⥤ C) ⥤ C preserving colimits.

class CategoryTheory.AB5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFilteredColimits C] : Prop

A category C which has filtered colimits is said to have AB5 provided that filtered colimits are exact.

• preservesFiniteLimits : ∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J], CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

  Exactness of filtered colimits stated as colim : (J ⥤ C) ⥤ C on filtered J preserving limits.

class CategoryTheory.AB5Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCofilteredLimits C] : Prop

A category C which has cofiltered limits is said to have AB5Star (in literature AB5*) provided that cofiltered limits are exact.

• preservesFiniteColimits : ∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsCofiltered J], CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim

  Exactness of cofiltered limits stated as lim : (J ⥤ C) ⥤ C on cofiltered J preserving colimits.

instance CategoryTheory.preservesFiniteLimits_liftToFinset (C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α)

Equations

• ⋯ = ⋯

theorem CategoryTheory.AB4.of_AB5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFilteredColimits C] [CategoryTheory.AB5 C] : CategoryTheory.AB4 C

A category with finite biproducts and finite limits is AB4 if it is AB5.