Arrows from initial objects to non-isomorphic objects in an elementary topos are monomorphisms?

Question

Let $\mathscr{T}$ be an elementary topos (I use the definition of a Cartesian closed, finitely complete category with a subobject classifier). Let $a$ be any object (that's not isomorphic to $0$) of $\mathscr{T}$, and $0$ the initial object. Is any arrow of the form $f: 0 \to a$ a monomorphism? I believe the answer is yes, but I can't figure out a proof.

Answer 1

The answer is that they are, but for stupid reasons : the same reason that in $\mathbf{Set}$, any map $\emptyset \to A$ is mono.

Indeed, in an elementary topos $\mathscr{T}$, any object $A$ with a map $A\to 0$ is also $0$, so this map is actually unique.

To prove this, first note that for any object $B$, $B\times 0 \simeq 0$. Indeed, by exponentiation, one has $\hom(B\times 0, X)\cong \hom(0,X^B) \cong \{*\}$, naturally in $X$, so $B\times 0$ is an initial object.

Then note that if you have a map $f:A\to 0$, then you have a map $A\to A\times 0$, namely $(id_A,f)$. Now $\pi_A\circ (id_A,f) = id_A$ by definition, and $\pi_A\circ (id_A,f)\circ \pi_A = id_A\circ \pi_A = \pi_A=\pi_A\circ id_{A\times 0}$, $\pi_0\circ (id_A,f)\circ \pi_A = f\circ \pi_A= \pi_0\circ id_{A\times 0}$ because $A\times 0$ is initial, and so there's a unique map $A\times 0 \to 0$ : if I know one such map, it must be this one.

These two equations prove (universal property of the product) that $(id_A,f)\circ \pi_A = id_{A\times 0}$; so that $(id_A,f)$ and $\pi_A$ are a pair of isomorphisms : $A\simeq A\times 0$. But $A\times 0 \simeq 0$, so $A\simeq 0$.

Now we proved that any object with a map $A\to 0$ must be initial, so if there are two maps $f,g: B\to 0$ such that [insert any condition you like], then $f=g$. In particular, any map leaving $0$ is a monomorphism