[proofplan] We construct the canonical morphism $\theta_f: \operatorname{Coim}(f) \to \operatorname{Im}(f)$ by factoring $f$ first through the kernel of its cokernel and then through the cokernel of its kernel. To prove that $\theta_f$ is monic, we test a morphism killed by $\theta_f$, pull back the cokernel map $p$, and use the stability of cokernels under pullback in abelian categories. The proof that $\theta_f$ is epic is dual: we test a morphism that kills $\theta_f$, push out the kernel map $i$, and use the stability of kernels under pushout. Finally, since abelian categories are balanced, a morphism that is both monic and epic is an isomorphism. [/proofplan] [step:Construct the canonical morphism from the coimage to the image] Let $k: K \to A$ be a kernel of $f$, and let \begin{align*} p: A \to C \end{align*} be a cokernel of $k$, where $C := \operatorname{Coim}(f)$. Thus \begin{align*} f \circ k = 0, \qquad p \circ k = 0. \end{align*} Let \begin{align*} q: B \to Q \end{align*} be a cokernel of $f$, where $Q := \operatorname{Coker}(f)$, and let \begin{align*} i: I \to B \end{align*} be a kernel of $q$, where $I := \operatorname{Im}(f)$. Since $q \circ f = 0$ and $i$ is a kernel of $q$, the universal property of $i$ gives a unique morphism \begin{align*} g: A \to I \end{align*} such that \begin{align*} i \circ g = f. \end{align*} Since $f \circ k = 0$, we have \begin{align*} i \circ g \circ k = f \circ k = 0. \end{align*} The morphism $i$ is monic because every kernel is monic, hence $g \circ k = 0$. Since $p$ is a cokernel of $k$, the universal property of $p$ gives a unique morphism \begin{align*} \theta: C \to I \end{align*} such that \begin{align*} \theta \circ p = g. \end{align*} Therefore \begin{align*} i \circ \theta \circ p = i \circ g = f. \end{align*} This morphism $\theta$ is the canonical morphism $\operatorname{Coim}(f) \to \operatorname{Im}(f)$. [guided] We first name every object involved in the image-coimage factorisation. The coimage is defined as the cokernel of the kernel of $f$: choose a kernel \begin{align*} k: K \to A \end{align*} of $f$, and then choose its cokernel \begin{align*} p: A \to C, \qquad C := \operatorname{Coim}(f). \end{align*} Thus $f \circ k = 0$ by the definition of $k$, and $p \circ k = 0$ by the definition of $p$. The image is defined as the kernel of the cokernel of $f$: choose a cokernel \begin{align*} q: B \to Q, \qquad Q := \operatorname{Coker}(f), \end{align*} and then choose its kernel \begin{align*} i: I \to B, \qquad I := \operatorname{Im}(f). \end{align*} Because $q$ is a cokernel of $f$, we have $q \circ f = 0$. Since $i$ is a kernel of $q$, every morphism into $B$ killed by $q$ factors uniquely through $i$. Applying this universal property to $f: A \to B$, there is a unique morphism \begin{align*} g: A \to I \end{align*} such that \begin{align*} i \circ g = f. \end{align*} Now we want this factorisation to pass through the coimage $C$. Since $f \circ k = 0$, we compute \begin{align*} i \circ g \circ k = f \circ k = 0. \end{align*} Every kernel is monic, so $i$ is monic. Cancelling $i$ gives $g \circ k = 0$. Therefore the universal property of the cokernel $p: A \to C$ applies to $g$: there is a unique morphism \begin{align*} \theta: C \to I \end{align*} such that \begin{align*} \theta \circ p = g. \end{align*} Combining the two factorisations gives \begin{align*} i \circ \theta \circ p = i \circ g = f. \end{align*} This is exactly the canonical comparison morphism from the coimage of $f$ to the image of $f$. [/guided] [/step] [step:Show that the canonical morphism is monic by pulling back the cokernel map] We prove that $\theta$ is monic. Let \begin{align*} u: X \to C \end{align*} be a morphism satisfying $\theta \circ u = 0$. We must prove $u = 0$. Form the pullback of $p: A \to C$ along $u: X \to C$: \begin{align*} P := A \times_C X, \end{align*} with projection morphisms \begin{align*} a: P \to A, \qquad v: P \to X, \end{align*} so that \begin{align*} p \circ a = u \circ v. \end{align*} Since $p$ is a cokernel and cokernels are stable under pullback in abelian categories, $v$ is an epimorphism. We use the standard stability theorem here: citing a result not yet in the wiki: pullbacks of cokernels in abelian categories are cokernels. Now compute \begin{align*} f \circ a &= i \circ \theta \circ p \circ a \\ &= i \circ \theta \circ u \circ v \\ &= i \circ 0 \circ v \\ &= 0. \end{align*} Since $k: K \to A$ is a kernel of $f$, the equality $f \circ a = 0$ gives a unique morphism \begin{align*} r: P \to K \end{align*} such that \begin{align*} k \circ r = a. \end{align*} Therefore \begin{align*} u \circ v &= p \circ a \\ &= p \circ k \circ r \\ &= 0. \end{align*} Since $v$ is epic, $u = 0$. Thus every morphism killed by $\theta$ is zero, so $\theta$ is monic. [guided] To prove that $\theta$ is monic, it is enough in an additive category to prove the following cancellation test: whenever a morphism \begin{align*} u: X \to C \end{align*} satisfies $\theta \circ u = 0$, then $u = 0$. The difficulty is that $p: A \to C$ is an epimorphism, but a general morphism $u: X \to C$ need not factor through $p$. The standard way to compare $u$ with $p$ is to form their pullback. Let \begin{align*} P := A \times_C X \end{align*} be the pullback, with projection morphisms \begin{align*} a: P \to A, \qquad v: P \to X, \end{align*} satisfying \begin{align*} p \circ a = u \circ v. \end{align*} We now use the exactness property of abelian categories that cokernels are stable under pullback. Since $p$ is a cokernel, its pullback $v$ is again a cokernel, and in particular $v$ is an epimorphism. This is the only categorical stability input in this half of the argument: citing a result not yet in the wiki: pullbacks of cokernels in abelian categories are cokernels. Now use the assumption $\theta \circ u = 0$. Starting from the factorisation $f = i \circ \theta \circ p$, we compute \begin{align*} f \circ a &= i \circ \theta \circ p \circ a \\ &= i \circ \theta \circ u \circ v \\ &= i \circ 0 \circ v \\ &= 0. \end{align*} Thus $a: P \to A$ is killed by $f$. Since $k: K \to A$ is the kernel of $f$, the universal property of $k$ gives a unique morphism \begin{align*} r: P \to K \end{align*} such that \begin{align*} k \circ r = a. \end{align*} Applying $p$ and using $p \circ k = 0$, we get \begin{align*} u \circ v &= p \circ a \\ &= p \circ k \circ r \\ &= 0. \end{align*} Finally, $v$ is epic, so the equality $u \circ v = 0$ forces $u = 0$. Therefore the only morphism into $C$ killed by $\theta$ is the zero morphism, which proves that $\theta$ is monic. [/guided] [/step] [step:Show that the canonical morphism is epic by pushing out the kernel map] We prove that $\theta$ is epic. Let \begin{align*} w: I \to Y \end{align*} be a morphism satisfying $w \circ \theta = 0$. We must prove $w = 0$. Form the pushout of $i: I \to B$ along $w: I \to Y$: \begin{align*} R := B \amalg_I Y, \end{align*} with structure morphisms \begin{align*} b: B \to R, \qquad y: Y \to R, \end{align*} so that \begin{align*} b \circ i = y \circ w. \end{align*} Since $i$ is a kernel and kernels are stable under pushout in abelian categories, $y$ is a monomorphism. We use the dual standard stability theorem here: citing a result not yet in the wiki: pushouts of kernels in abelian categories are kernels. Now compute \begin{align*} b \circ f &= b \circ i \circ \theta \circ p \\ &= y \circ w \circ \theta \circ p \\ &= y \circ 0 \circ p \\ &= 0. \end{align*} Since $q: B \to Q$ is a cokernel of $f$, the equality $b \circ f = 0$ gives a unique morphism \begin{align*} h: Q \to R \end{align*} such that \begin{align*} h \circ q = b. \end{align*} Because $i$ is a kernel of $q$, we have $q \circ i = 0$. Hence \begin{align*} y \circ w &= b \circ i \\ &= h \circ q \circ i \\ &= 0. \end{align*} Since $y$ is monic, $w = 0$. Thus every morphism that kills $\theta$ is zero, so $\theta$ is epic. [guided] The proof that $\theta$ is epic is the dual of the monomorphism argument. In an additive category, to prove that $\theta$ is epic, it is enough to show that every morphism out of $I$ that vanishes after precomposition with $\theta$ is itself zero. So let \begin{align*} w: I \to Y \end{align*} be a morphism satisfying \begin{align*} w \circ \theta = 0. \end{align*} The kernel map $i: I \to B$ need not allow us to compare $w$ directly inside $B$, so we use the dual construction to a pullback: form the pushout \begin{align*} R := B \amalg_I Y \end{align*} of $i$ along $w$. Let \begin{align*} b: B \to R, \qquad y: Y \to R \end{align*} be the pushout structure morphisms, so \begin{align*} b \circ i = y \circ w. \end{align*} We now use the exactness property dual to the one used above: kernels are stable under pushout in abelian categories. Since $i$ is a kernel, the pushout morphism $y$ is again a kernel, and therefore $y$ is monic. This is the dual standard stability input: citing a result not yet in the wiki: pushouts of kernels in abelian categories are kernels. Using the factorisation $f = i \circ \theta \circ p$ and the assumption $w \circ \theta = 0$, we compute \begin{align*} b \circ f &= b \circ i \circ \theta \circ p \\ &= y \circ w \circ \theta \circ p \\ &= y \circ 0 \circ p \\ &= 0. \end{align*} Thus $b: B \to R$ is a morphism out of $B$ that kills $f$. Since $q: B \to Q$ is the cokernel of $f$, the universal property of $q$ gives a unique morphism \begin{align*} h: Q \to R \end{align*} such that \begin{align*} h \circ q = b. \end{align*} Because $i$ is a kernel of $q$, we have $q \circ i = 0$. Therefore \begin{align*} y \circ w &= b \circ i \\ &= h \circ q \circ i \\ &= 0. \end{align*} Since $y$ is monic, this forces $w = 0$. Hence every morphism out of $I$ that vanishes on $\theta$ is zero, so $\theta$ is epic. [/guided] [/step] [step:Conclude that the monic and epic canonical morphism is an isomorphism] We have proved that \begin{align*} \theta: C \to I \end{align*} is both monic and epic. In an abelian category, every monomorphism is a kernel. Let \begin{align*} c: I \to D \end{align*} be a cokernel of $\theta$. Since $\theta$ is monic, $\theta$ is a kernel of $c$. Since $\theta$ is epic and $c \circ \theta = 0$, it follows that $c = 0$. The identity morphism \begin{align*} \operatorname{id}_I: I \to I \end{align*} is also a kernel of the zero morphism $c: I \to D$, because every morphism $x: X \to I$ satisfies $c \circ x = 0$ and factors uniquely through $\operatorname{id}_I$. Kernels of a fixed morphism are unique up to unique isomorphism, so $\theta: C \to I$ is isomorphic to $\operatorname{id}_I: I \to I$ as a kernel of $c$. Therefore $\theta$ is an isomorphism. Substituting $C = \operatorname{Coim}(f)$ and $I = \operatorname{Im}(f)$, the canonical morphism \begin{align*} \theta_f: \operatorname{Coim}(f) \to \operatorname{Im}(f) \end{align*} is an isomorphism. [guided] We have shown two separate cancellation properties: $\theta$ is monic and $\theta$ is epic. In an arbitrary category, a morphism that is both monic and epic need not be an isomorphism. The abelian hypothesis supplies the missing step. Because $\mathcal{A}$ is abelian, every monomorphism is a kernel. Let \begin{align*} c: I \to D \end{align*} be a cokernel of $\theta$. Since $\theta$ is monic, the normality axiom for monomorphisms in an abelian category says that $\theta$ is a kernel of $c$. By definition of cokernel, we have \begin{align*} c \circ \theta = 0. \end{align*} But $\theta$ is epic, so postcomposition equality after $\theta$ determines the morphism. Hence $c \circ \theta = 0 \circ \theta$ implies \begin{align*} c = 0. \end{align*} Now identify the kernel of this zero morphism. The identity morphism \begin{align*} \operatorname{id}_I: I \to I \end{align*} is a kernel of $c: I \to D$ because $c = 0$, so every morphism $x: X \to I$ satisfies \begin{align*} c \circ x = 0, \end{align*} and it factors uniquely through $\operatorname{id}_I$ by the equality \begin{align*} x = \operatorname{id}_I \circ x. \end{align*} Thus both $\theta: C \to I$ and $\operatorname{id}_I: I \to I$ are kernels of the same morphism $c$. Kernels are unique up to unique isomorphism, so $\theta$ is an isomorphism. Since $C$ was defined to be $\operatorname{Coim}(f)$ and $I$ was defined to be $\operatorname{Im}(f)$, this proves that the canonical morphism \begin{align*} \theta_f: \operatorname{Coim}(f) \to \operatorname{Im}(f) \end{align*} is an isomorphism. [/guided] [/step]