Construction 2.1.3.1.2 (01DL): Construction of Binary Products 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 product of $A$ and $B$ is the pair $\webleft (A\times B,\webleft\{ \text{pr}_{1},\text{pr}_{2}\webright\} \webright )$ consisting of:

The Limit. The set $A\times B$ defined by
\begin{align*} A\times B & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\prod _{z\in \webleft\{ A,B\webright\} }z\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ f\in \mathsf{Sets}\webleft (\webleft\{ 0,1\webright\} ,A\cup B\webright )\ \middle |\ \text{we have $f\webleft (0\webright )\in A$ and $f\webleft (1\webright )\in B$}\webright\} \\ & \cong \webleft\{ \webleft\{ \webleft\{ a\webright\} ,\webleft\{ a,b\webright\} \webright\} \in \mathcal{P}\webleft (\mathcal{P}\webleft (A\cup B\webright )\webright )\ \middle |\ \text{we have $a\in A$ and $b\in B$}\webright\} \\ & \cong \webleft\{ \begin{aligned} & \text{ordered pairs $\webleft (a,b\webright )$ with}\\ & \text{$a\in A$ and $b\in B$}\end{aligned} \webright\} .\end{align*}
The Cone. The maps
\begin{align*} \text{pr}_{1} & \colon A\times B\to A,\\ \text{pr}_{2} & \colon A\times B\to B \end{align*}

defined by

\begin{align*} \text{pr}_{1}\webleft (a,b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}a,\\ \text{pr}_{2}\webleft (a,b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}b \end{align*}

for each $\webleft (a,b\webright )\in A\times B$.

We claim that $A\times B$ is the categorical product 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 P\to A\times B$ making the diagram

commute, being uniquely determined by the conditions

\begin{align*} \text{pr}_{1}\circ \phi & = p_{1},\\ \text{pr}_{2}\circ \phi & = p_{2} \end{align*}

via

\[ \phi \webleft (x\webright )=\webleft (p_{1}\webleft (x\webright ),p_{2}\webleft (x\webright )\webright ) \]

for each $x\in P$.