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.

theorem category_theory.abelian.exact_epi_comp_iff {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X Y) (g : Y Z) {W : C} (h : W X) [category_theory.epi h] :

The dual result is true even in non-abelian categories, see category_theory.exact_epi_comp_iff.

@[protected, instance]

If ex : exact f g and epi g, then cokernel.desc _ _ ex.w is an isomorphism.

theorem category_theory.abelian.exact.op {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X Y) (g : Y Z) (h : category_theory.exact f g) :