The pushout of $A$ and $B$ over $C$ along $f$ and $g$1 is the pushout of $A$ and $B$ over $C$ along $f$ and $g$ in $\mathsf{Sets}$ as in 
, .
- 1Further Terminology: Also called the fibre coproduct of $A$ and $B$ over $C$ along $f$ and $g$.
-
1.
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 )$.
-
2.
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$.
-
1.
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 4.2.4.1.3, we have a sequence
\[ \webleft (0,a\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (0,a'\webright ). \] -
2.
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 4.2.4.1.3, we have a sequence
\[ \webleft (1,b\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b'\webright ). \] -
3.
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 4.2.4.1.3, we have a sequence
\[ \webleft (0,a\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b\webright ). \] -
1.
We have $a,b\in A$ and $a=b$.
-
2.
We have $a,b\in B$ and $a=b$.
-
3.
There exist $x_{1},\ldots ,x_{n}\in A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ such that $a\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim 'b$, where we declare $x\sim 'y$ if one of the following conditions is satisfied:
-
(a)
There exists $c\in C$ such that $x=\webleft (0,f\webleft (c\webright )\webright )$ and $y=\webleft (1,g\webleft (c\webright )\webright )$.
-
(b)
There exists $c\in C$ such that $x=\webleft (1,g\webleft (c\webright )\webright )$ and $y=\webleft (0,f\webleft (c\webright )\webright )$.
In other words, there exist $x_{1},\ldots ,x_{n}\in A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ satisfying the following conditions:
-
(a)
-
1.
Wedge Sums of Pointed Sets. The wedge sum of two pointed sets of Chapter 6: Pointed Sets, Definition 6.3.3.1.1 is an example of a pushout of sets.
-
2.
Intersections via Unions. Let $X$ be a set. We have
for each $A,B\in \mathcal{P}\webleft (X\webright )$.
-
1.
Functoriality. The assignment $\webleft (A,B,C,f,g\webright )\mapsto A\mathbin {\textstyle \coprod _{f,C,g}}B$ 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 map $\xi \colon A\mathbin {\textstyle \coprod _{C}}B\overset {\exists !}{\to }A'\mathbin {\textstyle \coprod _{C'}}B'$ given by
\[ \xi \webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \phi \webleft (a\webright ) & \text{if $x=\webleft [\webleft (0,a\webright )\webright ]$},\\ \psi \webleft (b\webright ) & \text{if $x=\webleft [\webleft (1,b\webright )\webright ]$} \end{cases} \]for each $x\in A\mathbin {\textstyle \coprod _{C}}B$, which is the unique map making the diagram
commute.
-
2.
Adjointness. We have an adjunction
witnessed by a bijection
\[ \mathsf{Sets}_{X/}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X}B,C\webright ),\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{X/}\times \mathsf{Sets}_{X/}}\webleft (\webleft (A,B\webright ),\webleft (C,C\webright )\webright ) \]natural in $\webleft (A,B\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{X/}\times \mathsf{Sets}_{X/}\webright )$ and in $C\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{X/}\webright )$.
-
3.
Associativity. Given a diagram
in $\mathsf{Sets}$, we have isomorphisms of sets
\[ \webleft (A\mathbin {\textstyle \coprod _{X}}B\webright )\mathbin {\textstyle \coprod _{Y}}C\cong \webleft (A\mathbin {\textstyle \coprod _{X}}B\webright )\mathbin {\textstyle \coprod _{B}}\webleft (B\mathbin {\textstyle \coprod _{Y}}C\webright ) \cong A\mathbin {\textstyle \coprod _{X}}\webleft (B\mathbin {\textstyle \coprod _{Y}}C\webright ) \]where these pullbacks are built as in the diagrams
-
4.
Interaction With Composition. Given a diagram
in $\mathsf{Sets}$, we have isomorphisms of sets
\begin{align*} X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi \circ f,\psi \circ g}_{K}Y & \cong \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi ,j_{1}}_{A}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{i_{2},i_{1}}_{A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B}\webleft (\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{j_{2},\psi }_{B}Y\webright )\\ & \cong X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi ,i}_{A}\webleft (\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{j_{2},\psi }_{B}Y\webright )\\ & \cong \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi ,i_{1}}_{A}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{j,\psi }_{B}Y \end{align*}where
\[ \begin{aligned} j_{1} & = \mathrm{inj}^{A\times ^{f,g}_{K}B}_{1},\\ i_{1} & = \mathrm{inj}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{Y}}_{1},\\ i & = j_{1}\circ \mathrm{inj}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y}_{1}, \end{aligned} \qquad \begin{aligned} j_{2} & = \mathrm{inj}^{A\times ^{f,g}_{K}B}_{2},\\ i_{2} & = \mathrm{inj}^{X\times ^{\phi ,q_{1}}_{A\times ^{f,g}_{K}B}\webleft (A\times ^{f,g}_{K}B\webright )}_{2},\\ j & = j_{2}\circ \mathrm{inj}^{X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )}_{2}, \end{aligned} \]and where these pullbacks are built as in the diagrams
-
5.
Unitality. We have isomorphisms of sets
natural in $\webleft (A,f\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{X/}\webright )$.
-
6.
Commutativity. We have an isomorphism of sets
natural in $\webleft (A,f\webright ),\webleft (B,g\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{X/}\webright )$.
-
7.
Interaction With Coproducts. We have
-
8.
Symmetric Monoidality. The triple $\webleft (\mathsf{Sets}_{X/},\mathbin {\textstyle \coprod _{X}},X\webright )$ is a symmetric monoidal category.
4.2.4 Pushouts
Let $A$, $B$, and $C$ be sets and let $f\colon C\to A$ and $g\colon C\to B$ be functions.
Concretely, the pushout of $A$ and $B$ over $C$ along $f$ and $g$ is the pair $\webleft (A\mathbin {\textstyle \coprod _{C}}B,\left\{ \mathrm{inj}_{1},\mathrm{inj}_{2}\right\} \webright )$ consisting of:
Proof of Construction 4.2.4.1.2.
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
\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
\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:
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.
In detail, by Chapter 10: Conditions on Relations, Construction 10.5.2.1.2, the relation $\mathord {\sim }$ of Definition 4.2.4.1.1 is given by declaring $a\sim b$ iff one of the following conditions is satisfied:
It is common practice to write $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{C}B$ for the pushout of $A$ and $B$ over $C$ along $f$ and $g$, omitting the maps $f$ and $g$ from the notation and instead leaving them implicit, to be understood from the context.
However, the set $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{C}B$ depends very much on the maps $f$ and $g$, and sometimes it is necessary or useful to note this dependence explicitly. In such situations, we will write $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{f,C,g}B$ or $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{C}B$ for $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{C}B$.
Here are some examples of pushouts of sets.
Proof of Example 4.2.4.1.5.
Item 1: Wedge Sums of Pointed Sets
This follows by definition, as the wedge sum of two pointed sets is defined as a pushout.
Item 2: Intersections via Unions
Indeed, $A\mathbin {\textstyle \coprod _{A\cap B}}B$ is the quotient of $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ by the equivalence relation obtained by declaring $\webleft (0,a\webright )\sim \webleft (1,b\webright )$ iff $a=b\in A\cap B$, which is in bijection with $A\cup B$ via the map with $\webleft [\webleft (0,a\webright )\webright ]\mapsto a$ and $\webleft [\webleft (1,b\webright )\webright ]\mapsto b$.
Let $A$, $B$, $C$, and $X$ be sets.
Proof of Proposition 4.2.4.1.6.
Item 1: Functoriality
This is a special case of functoriality of co/limits, , of , with the explicit expression for $\xi $ following from the commutativity of the cube pushout diagram.
Item 2: : Adjointness
This follows from the universal property of the coproduct (pushouts are coproducts in $\mathsf{Sets}_{X/}$).
Item 3: Associativity
Omitted.
Item 4: Interaction With Composition
Omitted.
Item 5: Unitality
Omitted.
Item 6: Commutativity
Omitted.
Item 7: Interaction With Coproducts
Omitted.
Item 8: Symmetric Monoidality
Omitted.
