In the question Do pushouts preserve monic? it is said that monics in a topos are stable under push out. I would like a precise reference or a nice proof of this fact for elementary topoi (for Grothendieck follows since it holds in Sets, then in presheaves and then in sheaves (pointwise computation + associated sheaf).
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
This is half of Corollary 2.4.3 in [Sketches of an elephant, Part A]. Here is (a paraphrase of) the proof:
Let $\mathcal{E}$ be an elementary topos, let $f : A \rightarrowtail B$ be a monomorphism in $\mathcal{E}$, and let $g : A \to C$ be any morphism in $\mathcal{E}$. Then the pushout of $f$ along $g$ is monic.
Proof. Let $d : C \to D$ and $e : B \to D$ constitute the colimiting cocone. We wish to show that $d$ is monic. Consider the morphism $\langle f, g \rangle : A \to B \times C$: this is monic because $f$ is. Let $h : B \to P C$ be the name of this binary relation, and let $\{ \cdot \} : C \to P C$ be the name of the equality relation on $C$. The universal property of pushouts then yields a factorisation of $d : C \to D$ through $\{ \cdot \} : C \to P C$. But $\{ \cdot \}$ is monic, so this implies $d$ is monic.
$\begingroup$
$\endgroup$
Just for reference, this is also the first half of corollary 4, ch. IV-10 in MacLane-Moerdijk "Sheaves in geometry and logic". The proof follows the same idea as the proof in Zhen Lin answer, except that the map $h: B \to PC$ is obtained using the previously proved property that $PC$ is injective, so that $\{.\}g$ extends to $B$.
