Documentation

Mathlib.CategoryTheory.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 imageSubobject f = kernelSubobject g.

The dual result is true even in non-abelian categories, see CategoryTheory.exact_comp_mono_iff.

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

If X ⟶ Y ⟶ Z ⟶ 0 is exact, then the second map is a cokernel of the first.

Instances For

    If 0 ⟶ X ⟶ Y ⟶ Z is exact, then the first map is a kernel of the second.

    Instances For
      theorem CategoryTheory.Abelian.Exact.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : CategoryTheory.Exact f g) :

      A functor preserving finite limits and finite colimits preserves exactness. The converse result is also true, see Functor.preservesFiniteLimitsOfMapExact and Functor.preservesFiniteColimitsOfMapExact.

      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 preserves kernels.

      Instances For

        A functor which preserves exactness preserves zero cokernels.

        Instances For

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

          Instances For

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

            Instances For