Grothendieck Axioms #
This file defines some of the Grothendieck Axioms for abelian categories, and proves basic facts about them.
Definitions #
AB4
-- an abelian category satisfiesAB4
provided that coproducts are exact.AB5
-- an abelian category satisfiesAB5
provided that filtered colimits are exact.- The duals of the above definitions, called
AB4Star
andAB5Star
.
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 #
References #
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.
Instances
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.
Instances
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 filteredJ
preserving limits.
Instances
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 cofilteredJ
preserving colimits.