Image factorization (source code)

= Image factorization
{title2=$A\twoheadrightarrow\operatorname{im}f\hookrightarrow B$}

An image of $f:A\to B$ is the least <subobject> $m:I\hookrightarrow B$ through which $f$ factors. In a <category> with <pullback in a category> constructions this gives a <strong epimorphism>–<monomorphism> factorization $f=me$: pull back any mono in a lifting square for $e$ to $I$; minimality of the image forces the resulting mono to be invertible, producing a diagonal. Conversely, the lifting property of the strong part proves minimality. No stability under pullback is asserted; that is an additional property in a <regular category>.