Documentation

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms

Grothendieck Axioms #

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

Definitions #

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.

Instances

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

    Instances

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

      Instances

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

        Instances