Split Monomorphism is Monic

Theorem

Let $\mathbf C$ be a metacategory.

Let $f: C \to D$ be a split monomorphism.

Then $f: C \rightarrowtail D$ is monic.

Proof

Let $g: D \to C$ be a morphism such that:

$g \circ f = \operatorname{id}_C$

which is guaranteed to exist by definition of split monomorphism.

Suppose that $x, y: B \to C$ are morphisms such that:

$f \circ x = f \circ y$

Then necessarily also:

$g \circ f \circ x = g \circ f \circ y$

and hence, since $g \circ f = \operatorname{id}_C$, it follows that:

$\operatorname{id}_C \circ x = \operatorname{id}_C \circ y$

which yields the result by the definition of identity morphism.

The situation is illustrated by the following commutative diagram:

$\quad\quad \begin{xy} <-4em,0em>*+{B} = "B", <0em,0em> *+{C} = "C", <4em,0em> *+{D} = "D", <4em,-4em>*+{C} = "C2", "B"+/r.5em/+/^.25em/;"C"+/l.5em/+/^.25em/ **@{-} ?>*@{>} ?*!/_.6em/{x}, "B"+/r.5em/+/_.25em/;"C"+/l.5em/+/_.25em/ **@{-} ?>*@{>} ?*!/^.6em/{y}, "C";"D" **@{-} ?>*@{>} ?*!/_.6em/{f}, "C";"C2" **@{-} ?>*@{>} ?*!/^.6em/{\operatorname{id}_C}, "D";"C2" **@{-} ?>*@{>} ?*!/_.6em/{g}, \end{xy}$

$\blacksquare$

Sources

• 2010: Steve Awodey: Category Theory (2nd ed.) ... (previous) ... (next): $\S 2.1.1$