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
(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.
The kernel of the cokernel of
f is called the (abelian) image of
The inclusion of the image into the codomain.
There is a canonical epimorphism
p : P ⟶ image f for every
f factors through its image via the canonical morphism
The cokernel of the kernel of
f is called the (abelian) coimage of
The projection onto the coimage.
There is a canonical monomorphism
i : coimage f ⟶ Q.
f factors through its coimage via the canonical morphism
The canonical map from the abelian coimage to the abelian image. In any abelian category this is an isomorphism.
Conversely, any additive category with kernels and cokernels and in which this is always an isomorphism, is abelian.
An alternative formulation of the canonical map from the abelian coimage to the abelian image.