Item 2 (01EL) — The Clowder Project

4.2.3 Binary Coproducts

Let $A$ and $B$ be sets.

Definition 4.2.3.1.1 ▶ Coproducts of Sets

The coproduct of $A$ and $B$¹ is the coproduct of $A$ and $B$ in $\mathsf{Sets}$ as in , .

¹Further Terminology: Also called the disjoint union of $A$ and $B$.

Construction 4.2.3.1.2 ▶ Construction of Coproducts of Sets

Concretely, the coproduct of $A$ and $B$ is the pair $(A\coprod B,\left\{ \mathrm{inj}_{1},\mathrm{inj}_{2}\right\} )$ consisting of:

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\{ (0,a)\in S\ \middle |\ a\in A\right\} \cup \left\{ (1,b)\in S\ \middle |\ b\in B\right\} , \end{align*}

where $S=\left\{ 0,1\right\} \times (A\cup B)$.

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}(a) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(0,a),\\ \mathrm{inj}_{2}(b) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(1,b), \end{align*}

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

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

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

commute, being uniquely determined by the conditions

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

via

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

for each $x\in A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$.

Proposition 4.2.3.1.3 ▶ Properties of Coproducts of Sets

Let $A$, $B$, $C$, and $X$ be sets.

1.
Functoriality. The assignment $A,B,(A,B)\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 $(A,B)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}\times \mathsf{Sets})$, we have
  
  \[ [-_{1}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}-_{2}](A,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. \]
- •
  Action on Morphisms. For each $(A,B),(X,Y)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, the action on $\operatorname {\mathrm{Hom}}$-sets
  
  \[ \mathbin {\textstyle \coprod _{(A,B),(X,Y)}} \colon \mathsf{Sets}(A,X)\times \mathsf{Sets}(B,Y)\to \mathsf{Sets}(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) \]
  
  of $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$ at $((A,B),(X,Y))$ is defined by sending $(f,g)$ 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
  
  \[ [f\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g](x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} (0,f(a)) & \text{if $x=(0,a)$,}\\ (1,g(b)) & \text{if $x=(1,b)$,}\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}}(\mathsf{Sets})$.
2.
Adjointness. We have an adjunction
witnessed by a bijection

\[ \mathsf{Sets}(A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B,C),\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}\times \mathsf{Sets}}((A,B),(C,C)) \]

natural in $(A,B)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}\times \mathsf{Sets})$ and in $C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
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 (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y)\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 }}(Y\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Z), \]

natural in $X,Y,Z\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.
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}}(\mathsf{Sets})$.
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}}(\mathsf{Sets})$.
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.