mathlib documentation

category_theory.abelian.exact

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_comp_mono_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) :

A functor preserving finite limits and finite colimits preserves exactness. The converse result is also true, see functor.preserves_finite_limits_of_map_exact and functor.preserves_finite_colimits_of_map_exact.

A functor which preserves exactness preserves zero morphisms.

A functor which preserves exactness preserves monomorphisms.

A functor which preserves exactness preserves epimorphisms.

A functor which preserves exactness is left exact, i.e. preserves finite limits. This is part of the inverse implication to functor.map_exact.

Equations

A functor which preserves exactness is right exact, i.e. preserves finite colimits. This is part of the inverse implication to functor.map_exact.

Equations