Subsection 2.2.2 (001W): Coproducts of Families of Sets

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`

The disjoint union of the family $\webleft\{ A_{i}\webright\} _{i\in I}$ is the pair $\webleft (\coprod _{i\in I}A_{i},\webleft\{ \mathrm{inj}_{i}\webright\} _{i\in I}\webright )$ consisting of:

The Colimit. The set $\coprod _{i\in I}A_{i}$ defined by

\[ \coprod _{i\in I}A_{i}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (i,x\webright )\in I\times \webleft (\bigcup _{i\in I}A_{i}\webright ) \ \middle |\ \text{$x\in A_{i}$}\webright\} . \]
The Cocone. The collection

\[ \webleft\{ \mathrm{inj}_{i} \colon A_{i}\to \coprod _{i\in I}A_{i}\webright\} _{i\in I} \]

of maps given by

\[ \mathrm{inj}_{i}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (i,x\webright ) \]

for each $x\in A_{i}$ and each $i\in I$.

We claim that $\coprod _{i\in I}A_{i}$ is the categorical coproduct of $\webleft\{ A_{i}\webright\} _{i\in I}$ in $\mathsf{Sets}$. Indeed, suppose we have, for each $i\in I$, a diagram of the form

in $\mathsf{Sets}$. Then there exists a unique map $\phi \colon \coprod _{i\in I}A_{i}\to C$ making the diagram

commute, being uniquely determined by the condition $\phi \circ \mathrm{inj}_{i}=\iota _{i}$ for each $i\in I$ via

\[ \phi \webleft (\webleft (i,x\webright )\webright )=\iota _{i}\webleft (x\webright ) \]

for each $\webleft (i,x\webright )\in \coprod _{i\in I}A_{i}$.

Let $\webleft\{ A_{i}\webright\} _{i\in I}$ be a family of sets.

Functoriality. The assignment $\webleft\{ A_{i}\webright\} _{i\in I}\mapsto \coprod _{i\in I}A_{i}$ defines a functor
\[ \coprod _{i\in I}\colon \mathsf{Fun}\webleft (I_{\mathsf{disc}},\mathsf{Sets}\webright )\to \mathsf{Sets} \]

where
- Action on Objects. For each $\webleft (A_{i}\webright )_{i\in I}\in \text{Obj}\webleft (\mathsf{Fun}\webleft (I_{\mathsf{disc}},\mathsf{Sets}\webright )\webright )$, we have
  
  \[ \webleft[\coprod _{i\in I}\webright]\webleft (\webleft (A_{i}\webright )_{i\in I}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\coprod _{i\in I}A_{i} \]
- Action on Morphisms. For each $\webleft (A_{i}\webright )_{i\in I},\webleft (B_{i}\webright )_{i\in I}\in \text{Obj}\webleft (\mathsf{Fun}\webleft (I_{\mathsf{disc}},\mathsf{Sets}\webright )\webright )$, the action on $\textup{Hom}$-sets
  
  \[ \webleft (\coprod _{i\in I}\webright )_{\webleft (A_{i}\webright )_{i\in I},\webleft (B_{i}\webright )_{i\in I}} \colon \text{Nat}\webleft (\webleft (A_{i}\webright )_{i\in I},\webleft (B_{i}\webright )_{i\in I}\webright )\to \mathsf{Sets}\webleft (\coprod _{i\in I}A_{i},\coprod _{i\in I}B_{i}\webright ) \]
  
  of $\coprod _{i\in I}$ at $\webleft (\webleft (A_{i}\webright )_{i\in I},\webleft (B_{i}\webright )_{i\in I}\webright )$ is defined by sending a map
  
  \[ \webleft\{ f_{i}\colon A_{i}\to B_{i} \webright\} _{i\in I} \]
  
  in $\text{Nat}\webleft (\webleft (A_{i}\webright )_{i\in I},\webleft (B_{i}\webright )_{i\in I}\webright )$ to the map of sets
  
  \[ \coprod _{i\in I}f_{i}\colon \coprod _{i\in I}A_{i}\to \coprod _{i\in I}B_{i} \]
  
  defined by
  
  \[ \webleft[\coprod _{i\in I}f_{i}\webright]\webleft (i,a\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{i}\webleft (a\webright ) \]
  
  for each $\webleft (i,a\webright )\in \coprod _{i\in I}A_{i}$.

Item 1: Functoriality

This follows from

The Clowder Project

2.2.2 Coproducts of Families of Sets