Definition 6.3.4.1.1 (00BF): Pushouts of Pointed Sets

6.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 6.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 pushout of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ over $\webleft (Z,z_{0}\webright )$ along $\webleft (f,g\webright )$ in $\mathsf{Sets}_{*}$ as in , .

Construction 6.3.4.1.2 ▶ Construction of Pushouts of Pointed Sets

Concretely, 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 .

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 4: Constructions With Sets, Definition 4.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 6.3.4.1.3 ▶ 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.

1.
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.
2.
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
3.
Unitality. We have isomorphisms of sets
4.
Commutativity. We have an isomorphism of sets
5.
Interaction With Coproducts. We have
6.
Symmetric Monoidality. The triple $\webleft (\mathsf{Sets}_{*},\mathbin {\textstyle \coprod _{X}},\webleft (X,x_{0}\webright )\webright )$ is a symmetric monoidal category.