CatDat

Implication Details

Claim: Given a morphism whose category has pushouts, if it is a strict monomorphism, then it is an effective monomorphism.

Proof: Let $m : A \to B$ be a strict monomorphism in a category with pushouts. In particular, the pushout $B \sqcup_A B$ exists (and actually, we only need this pushout) with coprojections $i_1,i_2 : B \rightrightarrows B \sqcup_A B$ satisfying $i_1 \circ m = i_2 \circ m$. To show that $m$ is the equalizer of $i_1,i_2$, let $t : T \to B$ be a morphism with $i_1 \circ t = i_2 \circ t$. If $g,h : B \rightrightarrows C$ is any parallel pair with $g \circ m = h \circ m$, it induces a morphism $(g;h) : B \sqcup_A B \to C$ with $(g;h) \circ i_1 = g$ and $(g;h) \circ i_2 = h$. By composing these equations with $t$, we get $$g \circ t = (g;h) \circ i_1 \circ t = (g;h) \circ i_2 \circ t = h \circ t.$$ Thus, $t$ equalizes every parallel pair that is equalized by $m$. Since $m$ is a strict monomorphism, $t$ factors through $m$.