Equivalent conditions for a preabelian category to be abelian

Question

Let's fix some terminology first. A category $\mathcal{C}$ is preabelian if:

1) $Hom_{\mathcal{C}}(A,B)$ is an abelian group for every $A,B$ such that composition is biadditive,

2) $\mathcal{C}$ has a zero object,

3) $\mathcal{C}$ has binary products,

4) $\mathcal{C}$ has kernels and cokernels.

A category $\mathcal{C}$ is abelian if it is preabelian and satisfies:

5) every monomorphism is a kernel and every epimorphism is a cokernel.

Define the coimage of a map to be the cokernel of its kernel, and the image to be the kernel of its cokernel. We have the following commutative diagram:

where $\overline{f}$ is the only existing map (because of universality of kernel and cokernel).

I'm having trouble proving the following:

A preabelian category $\mathcal{C}$ is abelian iff $\overline{f}$ is an isomorphism.

The converse is easily shown, I'm having trouble proving $\Rightarrow$...

Answer 1

Here is an argument for $\Rightarrow$. There is not much more to it than chasing diagrams (as it should be). Also, I didn't really bother to check which (parts of the) axioms are actually needed:

1. In presence of 1),2),3) we have that $\mathcal{C}$ has biproducts as well: every binary coproduct is also a binary product. (This is not used below but I added it for the sake of completeness)

2. Assuming 1)-5), an epi $e:B \to C$ is the cokernel of its kernel.
   Indeed, let $f$ be a morphism such that $e = \operatorname{coker}\,{f}$ and let $k = \operatorname{ker}{e}$. Since $ef = 0$, we see that $f = kf'$. If $y$ is such that $yk =0$ then $ykf' = yf = 0$ and hence $y = y'e$, and thus $e$ is a cokernel of $k$.
   
   Dually, a mono is the kernel of its cokernel.

3. Assuming 1)-5) a morphism which is both an epimorphism and a monomorphism is an isomorphism.
   
   I leave that as an easy exercise (I gave the argument in the comments above).

4. Let $f: A \to B$. The morphism $i: \operatorname{Coim}{f} \to B$ is monic.
   To this end, let $x: X \to \operatorname{Coim}{f}$ be such that $ix = 0$. Let $q = \operatorname{coker}{x}$ and let $j: \operatorname{Coker}{x} \to B$ be the unique map such that $i = jq$. Since $qp$ is epi we have a morphism $h: H \to A$ such that $qp = \operatorname{coker}{{h}}$. Now $fh = iph = jqph = 0$ so $h = kh'$. This gives that $ph = pkh' = 0$,
   so $p$ factors as $p = p'(qp) = (p'q)p$. But $p$ is epi, so $p'q = 1_{\operatorname{Coim}{f}}$. This implies that $q$ is a monomorphism and finally $qx = 0$ implies that $x = 0$. We have shown that $ix = 0$ implies $x = 0$ and thus $i$ is a monomorphism.
   
   Dually $j: A \to \operatorname{Im}f$ is an epimorphism.

5. Consider the factorization of $f$: By step 4 we have that $A \to \operatorname{Im}{f}$ and $\operatorname{Coim}{f} \to B$ are epi and mono, respectively. Therefore $\bar{f}$ is both epi and mono and we're done by step 3.