Definition 2.2.4.1.1 (0029): Pushouts of Sets

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

The pushout of $A$ and $B$ over $C$ along $f$ and $g$^[1] is the pair ^[2] $\webleft (A\mathbin {\textstyle \coprod _{C}}B,\webleft\{ \mathrm{inj}_{1},\mathrm{inj}_{2}\webright\} \webright )$ consisting of:

The Colimit. The set $A\mathbin {\textstyle \coprod _{C}}B$ defined by

\[ A\mathbin {\textstyle \coprod _{C}}B\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B/\mathord {\sim }_{C}, \]

where $\mathord {\sim }_{C}$ is the equivalence relation on $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ generated by $\webleft (0,f\webleft (c\webright )\webright )\sim _{C}\webleft (1,g\webleft (c\webright )\webright )$.
The Cocone. The maps

\begin{align*} \mathrm{inj}_{1} & \colon A\to A\mathbin {\textstyle \coprod _{C}}B,\\ \mathrm{inj}_{2} & \colon B\to A\mathbin {\textstyle \coprod _{C}}B \end{align*}

given by

\begin{align*} \mathrm{inj}_{1}\webleft (a\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (0,a\webright )\webright ]\\ \mathrm{inj}_{2}\webleft (b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (1,b\webright )\webright ]\end{align*}

for each $a\in A$ and each $b\in B$.

We claim that $A\mathbin {\textstyle \coprod _{C}}B$ is the categorical pushout of $A$ and $B$ over $C$ with respect to $\webleft (f,g\webright )$ in $\mathsf{Sets}$. First we need to check that the relevant pushout diagram commutes, i.e. that we have

Indeed, given $c\in C$, we have

\begin{align*} \webleft [\mathrm{inj}_{1}\circ f\webright ]\webleft (c\webright ) & = \mathrm{inj}_{1}\webleft (f\webleft (c\webright )\webright )\\ & = \webleft [\webleft (0,f\webleft (c\webright )\webright )\webright ]\\ & = \webleft [\webleft (1,g\webleft (c\webright )\webright )\webright ]\\ & = \mathrm{inj}_{2}\webleft (g\webleft (c\webright )\webright )\\ & = \webleft [\mathrm{inj}_{2}\circ g\webright ]\webleft (c\webright ),\end{align*}

where $\webleft [\webleft (0,f\webleft (c\webright )\webright )\webright ]=\webleft [\webleft (1,g\webleft (c\webright )\webright )\webright ]$ by the definition of the relation $\mathord {\sim }$ on $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$. Next, we prove that $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{C}B$ satisfies the universal property of the pushout. Suppose we have a diagram of the form

in $\mathsf{Sets}$. Then there exists a unique map $\phi \colon A\mathbin {\textstyle \coprod _{C}}B\to P$ making the diagram

commute, being uniquely determined by the conditions

\begin{align*} \phi \circ \mathrm{inj}_{1} & = \iota _{1},\\ \phi \circ \mathrm{inj}_{2} & = \iota _{2} \end{align*}

via

\[ \phi \webleft (x\webright )=\begin{cases} \iota _{1}\webleft (a\webright ) & \text{if $x=\webleft [\webleft (0,a\webright )\webright ]$,}\\ \iota _{2}\webleft (b\webright ) & \text{if $x=\webleft [\webleft (1,b\webright )\webright ]$} \end{cases} \]

for each $x\in A\mathbin {\textstyle \coprod _{C}}B$, where the well-definedness of $\phi $ is guaranteed by the equality $\iota _{1}\circ f=\iota _{2}\circ g$ and the definition of the relation $\mathord {\sim }$ on $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ as follows:

Case 1: Suppose we have $x=\webleft [\webleft (0,a\webright )\webright ]=\webleft [\webleft (0,a'\webright )\webright ]$ for some $a,a'\in A$. Then, by Remark 2.2.4.1.2, we have a sequence
\[ \webleft (0,a\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (0,a'\webright ). \]
Case 2: Suppose we have $x=\webleft [\webleft (1,b\webright )\webright ]=\webleft [\webleft (1,b'\webright )\webright ]$ for some $b,b'\in B$. Then, by Remark 2.2.4.1.2, we have a sequence
\[ \webleft (1,b\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b'\webright ). \]
Case 3: Suppose we have $x=\webleft [\webleft (0,a\webright )\webright ]=\webleft [\webleft (1,b\webright )\webright ]$ for some $a\in A$ and $b\in B$. Then, by Remark 2.2.4.1.2, we have a sequence
\[ \webleft (0,a\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b\webright ). \]

In all these cases, we declare $x\sim 'y$ iff there exists some $c\in C$ such that $x=\webleft (0,f\webleft (c\webright )\webright )$ and $y=\webleft (1,g\webleft (c\webright )\webright )$ or $x=\webleft (1,g\webleft (c\webright )\webright )$ and $y=\webleft (0,f\webleft (c\webright )\webright )$. Then, the equality $\iota _{1}\circ f=\iota _{2}\circ g$ gives

\begin{align*} \phi \webleft (\webleft [x\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (0,f\webleft (c\webright )\webright )\webright ]\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\iota _{1}\webleft (f\webleft (c\webright )\webright )\\ & = \iota _{2}\webleft (g\webleft (c\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\phi \webleft (\webleft [\webleft (1,g\webleft (c\webright )\webright )\webright ]\webright )\\ & = \phi \webleft (\webleft [y\webright ]\webright ), \end{align*}

with the case where $x=\webleft (1,g\webleft (c\webright )\webright )$ and $y=\webleft (0,f\webleft (c\webright )\webright )$ similarly giving $\phi \webleft (\webleft [x\webright ]\webright )=\phi \webleft (\webleft [y\webright ]\webright )$. Thus, if $x\sim 'y$, then $\phi \webleft (\webleft [x\webright ]\webright )=\phi \webleft (\webleft [y\webright ]\webright )$. Applying this equality pairwise to the sequences

\begin{align*} \webleft (0,a\webright )& \sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (0,a'\webright ),\\ \webleft (1,b\webright )& \sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b'\webright ),\\ \webleft (0,a\webright )& \sim ’x_{1}\sim ’\cdots \sim ’x_{n}\sim ’\webleft (1,b\webright )\end{align*}

gives

\begin{align*} \phi \webleft (\webleft [\webleft (0,a\webright )\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (0,a'\webright )\webright ]\webright ),\\ \phi \webleft (\webleft [\webleft (1,b\webright )\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (1,b'\webright )\webright ]\webright ),\\ \phi \webleft (\webleft [\webleft (0,a\webright )\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (1,b\webright )\webright ]\webright ), \end{align*}

showing $\phi $ to be well-defined.

Footnotes

[1] Further Terminology: Also called the fibre coproduct of $A$ and $B$ over $C$ along $f$ and $g$.

[2] Further Notation: Also written $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{f,C,g}B$.