# 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`

.

## 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 filtered`J`

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 cofiltered`J`

preserving colimits.