mathlib documentation


The abelian image and coimage. #

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

In an abelian category we usually want the image of a morphism f to be defined as kernel (cokernel.π f), and the coimage to be defined as cokernel (kernel.ι f).

We make these definitions here, as abelian.image f and abelian.coimage f (without assuming the category is actually abelian), and later relate these to the usual categorical notions when in an abelian category.

There is a canonical morphism coimage_image_comparison : abelian.coimage f ⟶ abelian.image f. Later we show that this is always an isomorphism in an abelian category, and conversely a category with (co)kernels and finite products in which this morphism is always an isomorphism is an abelian category.

@[protected, reducible]

The kernel of the cokernel of f is called the (abelian) image of f.

@[protected, reducible]

The inclusion of the image into the codomain.

@[protected, reducible]

There is a canonical epimorphism p : P ⟶ image f for every f.

@[protected, reducible]

The cokernel of the kernel of f is called the (abelian) coimage of f.

@[protected, reducible]

There is a canonical monomorphism i : coimage f ⟶ Q.