mathlib3 documentation

category_theory.abelian.exact

Exact sequences in abelian categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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.

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