Subsection 4.3.4 (00BE): Pushouts — The Clowder Project

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`

4.3.4 Pushouts

Let $\webleft (X,x_{0}\webright )$, $\webleft (Y,y_{0}\webright )$, and $\webleft (Z,z_{0}\webright )$ be pointed sets and let $f\colon \webleft (Z,z_{0}\webright )\to \webleft (X,x_{0}\webright )$ and $g\colon \webleft (Z,z_{0}\webright )\to \webleft (Y,y_{0}\webright )$ be morphisms of pointed sets.

Definition 4.3.4.1.1 ▶ Pushouts of Pointed Sets

The pushout of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ over $\webleft (Z,z_{0}\webright )$ along $\webleft (f,g\webright )$ is the pair consisting of:

The Colimit. The pointed set $\webleft (X\coprod _{f,Z,g}Y,p_{0}\webright )$, where:
- The set $X\coprod _{f,Z,g}Y$ is the pushout (of unpointed sets) of $X$ and $Y$ over $Z$ with respect to $f$ and $g$;
- We have $p_{0}=\webleft [x_{0}\webright ]=\webleft [y_{0}\webright ]$.
The Cocone. The morphisms of pointed sets

\begin{align*} \mathrm{inj}_{1} & \colon \webleft (X,x_{0}\webright )\to \webleft (X\mathbin {\textstyle \coprod _{Z}}Y,p_{0}\webright ),\\ \mathrm{inj}_{2} & \colon \webleft (Y,y_{0}\webright )\to \webleft (X\mathbin {\textstyle \coprod _{Z}}Y,p_{0}\webright ) \end{align*}

given by

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

for each $x\in X$ and each $y\in Y$.

Proof of Definition 4.3.4.1.1.

Firstly, we note that indeed $\webleft [x_{0}\webright ]=\webleft [y_{0}\webright ]$, as we have

\begin{align*} x_{0} & = f\webleft (z_{0}\webright ),\\ y_{0} & = g\webleft (z_{0}\webright ) \end{align*}

since $f$ and $g$ are morphisms of pointed sets, with the relation $\mathord {\sim }$ on $X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{Z}Y$ then identifying $x_{0}=f\webleft (z_{0}\webright )\sim g\webleft (z_{0}\webright )=y_{0}$.

We now claim that $\webleft (X\mathbin {\textstyle \coprod _{Z}}Y,p_{0}\webright )$ is the categorical pushout of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ over $\webleft (Z,z_{0}\webright )$ 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 $z\in Z$, we have

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

where $\webleft [\webleft (0,f\webleft (z\webright )\webright )\webright ]=\webleft [\webleft (1,g\webleft (z\webright )\webright )\webright ]$ by the definition of the relation $\mathord {\sim }$ on $X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y$ (the coproduct of unpointed sets of $X$ and $Y$). Next, we prove that $X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{Z}Y$ satisfies the universal property of the pushout. Suppose we have a diagram of the form

in $\mathsf{Sets}_{*}$. Then there exists a unique morphism of pointed sets

\[ \phi \colon \webleft (X\mathbin {\textstyle \coprod _{Z}}Y,p_{0}\webright )\to \webleft (P,*\webright ) \]

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 (p\webright )=\begin{cases} \iota _{1}\webleft (x\webright ) & \text{if $x=\webleft [\webleft (0,x\webright )\webright ]$,}\\ \iota _{2}\webleft (y\webright ) & \text{if $x=\webleft [\webleft (1,y\webright )\webright ]$} \end{cases} \]

for each $p\in X\mathbin {\textstyle \coprod _{Z}}Y$, where the well-definedness of $\phi $ is proven in the same way as in the proof of Chapter 2: Constructions With Sets, Definition 2.2.4.1.1. Finally, we show that $\phi $ is indeed a morphism of pointed sets, as we have

\begin{align*} \phi \webleft (p_{0}\webright ) & = \phi \webleft (\webleft [\webleft (0,x_{0}\webright )\webright ]\webright )\\ & = \iota _{1}\webleft (x_{0}\webright )\\ & = *, \end{align*}

or alternatively

\begin{align*} \phi \webleft (p_{0}\webright ) & = \phi \webleft (\webleft [\webleft (1,y_{0}\webright )\webright ]\webright )\\ & = \iota _{2}\webleft (y_{0}\webright )\\ & = *, \end{align*}

where we use that $\iota _{1}$ (resp. $\iota _{2}$) is a morphism of pointed sets.

Proposition 4.3.4.1.2 ▶ Properties of Pushouts of Pointed Sets

Let $\webleft (X,x_{0}\webright )$, $\webleft (Y,y_{0}\webright )$, $\webleft (Z,z_{0}\webright )$, and $\webleft (A,a_{0}\webright )$ be pointed sets.

Functoriality. The assignment $\webleft (X,Y,Z,f,g\webright )\mapsto X\mathbin {\textstyle \coprod _{f,Z,g}}Y$ defines a functor
\[ -_{1}\mathbin {\textstyle \coprod _{-_{3}}}-_{1}\colon \mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}\webright )\to \mathsf{Sets}_{*}, \]

where $\mathcal{P}$ is the category that looks like this:

In particular, the action on morphisms of $-_{1}\mathbin {\textstyle \coprod _{-_{3}}}-_{1}$ is given by sending a morphism

in $\mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}_{*}\webright )$ to the morphism of pointed sets

\[ \xi \colon \webleft (X\mathbin {\textstyle \coprod _{Z}}Y,p_{0}\webright )\overset {\exists !}{\to }\webleft (X'\mathbin {\textstyle \coprod _{Z'}}Y',p'_{0}\webright ) \]

given by

\[ \xi \webleft (p\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \phi \webleft (x\webright ) & \text{if $p=\webleft [\webleft (0,x\webright )\webright ]$},\\ \psi \webleft (y\webright ) & \text{if $p=\webleft [\webleft (1,y\webright )\webright ]$} \end{cases} \]

for each $p\in X\mathbin {\textstyle \coprod _{Z}}Y$, which is the unique morphism of pointed sets making the diagram

commute.
Associativity. Given a diagram

in $\mathsf{Sets}$, we have isomorphisms of pointed sets

\[ \webleft (X\mathbin {\textstyle \coprod _{W}}Y\webright )\mathbin {\textstyle \coprod _{V}}Z\cong \webleft (X\mathbin {\textstyle \coprod _{W}}Y\webright )\mathbin {\textstyle \coprod _{Y}}\webleft (Y\mathbin {\textstyle \coprod _{V}}Z\webright ) \cong X\mathbin {\textstyle \coprod _{W}}\webleft (Y\mathbin {\textstyle \coprod _{V}}Z\webright ), \]

where these pullbacks are built as in the diagrams
Unitality. We have isomorphisms of sets
Commutativity. We have an isomorphism of sets
Interaction With Coproducts. We have
Symmetric Monoidality. The triple $\webleft (\mathsf{Sets}_{*},\mathbin {\textstyle \coprod _{X}},\webleft (X,x_{0}\webright )\webright )$ is a symmetric monoidal category.