Functoriality of abelian image factorization
= Functoriality of abelian image factorization
A commuting square $vf=f'u$ induces a unique map between their images by $I(u,v)p=p'u$ and $i'I(u,v)=vi$. The <cokernel in a category> property supplies existence, and cancellation of the epimorphic $p$ supplies uniqueness. These equations prove identity and composition laws, giving a <functor> from the <arrow category> to the <abelian category>.