I was reading about the universal property of kernels in category theory: if $f:A\to B$ is a morphism in a category with zero morphisms, the kernel of $f$ is an ordered pair $(K, k)$ where $K$ is an object and $k$ a map from $K$ to $A$ such that $f\circ k = 0$; furthermore, if $(L, \ell)$ is another such ordered pair, there is a unique morphism $\tilde\ell$ such that $k\circ\tilde\ell = \ell$.
I also read that $k$ is in practice always a monomorphism, and found that this leads to the kernel being unique up to unique isomorphism. In group theory, $K$ is constructed explicitly as the preimage of $e_B$, and $k$ is simply inclusion. But what about in general? Is $k$ assumed to be a monomorphism, or can it be proven from the details given above?
$k$ is not assumed to be a monomorphism, this is a corollary of the definition.
Suppose $kx=ky$ for two arrows $x,y:L\to K$. Then $f\circ ky=(f\circ k)\circ y=0$ so the pair $(L,ky)$ has this property, so there should be a unique morphism $\tilde{\ell}:L\to K$ such that $k\tilde{\ell}=ky$. Obviously, both $x$ and $y$ serve as valid candidates for $\tilde{\ell}$, so by uniqueness they have to be the same; $x=y$ is forced.
Thus $k$ is a monomorphism. It's more generally true that any equaliser arrow is a monomorphism.