Grothendieck Axioms

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

Definitions

• AB4 -- an abelian category satisfies AB4 provided that coproducts are exact.
• AB5 -- an abelian 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.

Projects

• Add additional axioms, especially define Grothendieck categories.
• Prove that AB5 implies AB4.

References

• Stacks: Grothendieck's AB conditions

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

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] : Type (max u (v + 1))

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] : Type (max u (v + 1))

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] : Type (max u (v + 1))

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.preservesFiniteLimitsLiftToFinset (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

• One or more equations did not get rendered due to their size.

def CategoryTheory.AB4.ofAB5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFiniteCoproducts 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.

Equations

• One or more equations did not get rendered due to their size.