mathlib documentation


Exact sequences in abelian categories #

In an abelian category, we get several interesting results related to exactness which are not true in more general settings.

Main results #

In an abelian category, a pair of morphisms f : X ⟶ Y, g : Y ⟶ Z is exact iff image_subobject f = kernel_subobject g.