The coproduct of $A$ and $B$1 is the coproduct of $A$ and $B$ in $\mathsf{Sets}$ as in 
, .
- 1Further Terminology: Also called the disjoint union of $A$ and $B$.
-
1.
The Colimit. The set $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ defined by
\begin{align*} A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\coprod _{z\in \left\{ A,B\right\} }z\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (0,a\webright )\in S\ \middle |\ a\in A\right\} \cup \left\{ \webleft (1,b\webright )\in S\ \middle |\ b\in B\right\} , \end{align*}where $S=\left\{ 0,1\right\} \times \webleft (A\cup B\webright )$.
-
2.
The Cocone. The maps
\begin{align*} \mathrm{inj}_{1} & \colon A \to A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B,\\ \mathrm{inj}_{2} & \colon B \to A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B, \end{align*}given by
\begin{align*} \mathrm{inj}_{1}\webleft (a\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (0,a\webright ),\\ \mathrm{inj}_{2}\webleft (b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (1,b\webright ), \end{align*}for each $a\in A$ and each $b\in B$.
-
1.
Functoriality. The assignment $A,B,\webleft (A,B\webright )\mapsto A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ defines functors
\[ \begin{array}{ccc} A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-\colon \mkern -15mu & \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets},\\ -\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B\colon \mkern -15mu & \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets},\\ -_{1}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-_{2}\colon \mkern -15mu & \mathsf{Sets}\times \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets}, \end{array} \]where $-_{1}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-_{2}$ is the functor where
-
•
Action on Objects. For each $\webleft (A,B\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\times \mathsf{Sets}\webright )$, we have
\[ \webleft [-_{1}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-_{2}\webright ]\webleft (A,B\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B. \] -
•
Action on Morphisms. For each $\webleft (A,B\webright ),\webleft (X,Y\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, the action on $\operatorname {\mathrm{Hom}}$-sets
\[ \mathbin {\textstyle \coprod _{\webleft (A,B\webright ),\webleft (X,Y\webright )}} \colon \mathsf{Sets}\webleft (A,X\webright )\times \mathsf{Sets}\webleft (B,Y\webright )\to \mathsf{Sets}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B,X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ) \]of $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$ at $\webleft (\webleft (A,B\webright ),\webleft (X,Y\webright )\webright )$ is defined by sending $\webleft (f,g\webright )$ to the function
\[ f\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g\colon A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B\to X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y \]defined by
\[ \webleft [f\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g\webright ]\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \webleft (0,f\webleft (a\webright )\webright ) & \text{if $x=\webleft (0,a\webright )$,}\\ \webleft (1,g\webleft (b\webright )\webright ) & \text{if $x=\webleft (1,b\webright )$,}\end{cases} \]for each $x\in A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$.
and where $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-$ and $-\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ are the partial functors of $-_{1}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-_{2}$ at $A,B\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.
-
•
-
2.
Adjointness. We have an adjunction
witnessed by a bijection
\[ \mathsf{Sets}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B,C\webright ),\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}\times \mathsf{Sets}}\webleft (\webleft (A,B\webright ),\webleft (C,C\webright )\webright ) \]natural in $\webleft (A,B\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\times \mathsf{Sets}\webright )$ and in $C\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.
-
3.
Associativity. We have an isomorphism of sets
\[ \alpha ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y,Z} \colon \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Z \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (Y\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Z\webright ), \]natural in $X,Y,Z\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.
-
4.
Unitality. We have isomorphisms of sets
\begin{align*} \lambda ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X} & \colon \text{Ø}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}X \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X,\\ \rho ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X} & \colon X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\text{Ø}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X, \end{align*}natural in $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.
-
5.
Commutativity. We have an isomorphism of sets
\[ \sigma ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y} \colon X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }Y\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}X, \]natural in $X,Y\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.
-
6.
Symmetric Monoidality. The 7-tuple $\left(\phantom{\mathrlap {\alpha ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$, $\text{Ø}$, $\alpha ^{\mathsf{Sets}}_{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$, $\lambda ^{\mathsf{Sets}}_{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$, $\rho ^{\mathsf{Sets}}_{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$, $\left.\sigma ^{\mathsf{Sets}}\right)$ is a symmetric monoidal category.
4.2.3 Binary Coproducts
Let $A$ and $B$ be sets.
Concretely, the coproduct of $A$ and $B$ is the pair $\webleft (A\coprod B,\left\{ \mathrm{inj}_{1},\mathrm{inj}_{2}\right\} \webright )$ consisting of:
Proof of Construction 4.2.3.1.2.
We claim that $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ is the categorical coproduct of $A$ and $B$ in $\mathsf{Sets}$. Indeed, suppose we have a diagram of the form
\begin{align*} \phi \circ \mathrm{inj}_{A} & = \iota _{A},\\ \phi \circ \mathrm{inj}_{B} & = \iota _{B} \end{align*}
via
\[ \phi \webleft (x\webright )=\begin{cases} \iota _{A}\webleft (a\webright ) & \text{if $x=\webleft (0,a\webright )$,}\\ \iota _{B}\webleft (b\webright ) & \text{if $x=\webleft (1,b\webright )$} \end{cases} \]
for each $x\in A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$.
Let $A$, $B$, $C$, and $X$ be sets.
Proof of Proposition 4.2.3.1.3.
Item 1: Functoriality
This follows from , of .
Item 2: Adjointness
This follows from the universal property of the coproduct.
Item 3: Associativity
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.2.3.1.1.
Item 4: Unitality
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.2.4.1.1 and Definition 5.2.5.1.1.
Item 5: Commutativity
This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.2.6.1.1.
Item 6: Symmetric Monoidality
This is a repetition of Chapter 5: Monoidal Structures on the Category of Sets, Proposition 5.2.7.1.1, and is proved there.
