Subsection 2.1.3 (000S): 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`

2.1.3 Binary Products of Sets

Let $A$ and $B$ be sets.

The product^[1] 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 ^[2]

\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\} .\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$.

Proof of Definition 2.1.3.1.1.

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$.

Proposition 2.1.3.1.2 ▶ Properties of Products of Sets

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

Functoriality. The assignments $A,B,\webleft (A,B\webright )\mapsto A\times B$ define functors
\begin{gather*} \begin{aligned} A\times - & \colon \mathsf{Sets}\to \mathsf{Sets},\\ -\times B & \colon \mathsf{Sets}\to \mathsf{Sets}, \end{aligned}\\ -_{1}\times -_{2} \colon \mathsf{Sets}\times \mathsf{Sets}\to \mathsf{Sets}, \end{gather*}

where $-_{1}\times -_{2}$ is the functor where
- Action on Objects. For each $\webleft (A,B\webright )\in \text{Obj}\webleft (\mathsf{Sets}\times \mathsf{Sets}\webright )$, we have
  
  \[ \webleft [-_{1}\times -_{2}\webright ]\webleft (A,B\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B. \]
- Action on Morphisms. For each $\webleft (A,B\webright ),\webleft (X,Y\webright )\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on $\textup{Hom}$-sets
  
  \[ \times _{\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\times B,X\times Y\webright ) \]
  
  of $\times $ at $\webleft (\webleft (A,B\webright ),\webleft (X,Y\webright )\webright )$ is defined by sending $\webleft (f,g\webright )$ to the function
  
  \[ f\times g\colon A\times B\to X\times Y \]
  
  defined by
  
  \[ \webleft [f\times g\webright ]\webleft (a,b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f\webleft (a\webright ),g\webleft (b\webright )\webright ) \]
  
  for each $\webleft (a,b\webright )\in A\times B$.
and where $A\times -$ and $-\times B$ are the partial functors of $-_{1}\times -_{2}$ at $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Adjointness. We have adjunctions
witnessed by bijections
\begin{align*} \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,C\webright ) & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (A,\textup{Hom}_{\mathsf{Sets}}\webleft (B,C\webright )\webright ),\\ \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,C\webright ) & \cong \textup{Hom}_{\mathsf{Sets}}\webleft (B,\textup{Hom}_{\mathsf{Sets}}\webleft (A,C\webright )\webright ), \end{align*}

natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Associativity. We have an isomorphism of sets
\[ \webleft (A\times B\webright )\times C \cong A\times \webleft (B\times C\webright ), \]

natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Unitality. We have isomorphisms of sets
\begin{align*} \text{pt}\times A & \cong A,\\ A\times \text{pt}& \cong A, \end{align*}

natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Commutativity. We have an isomorphism of sets
\[ A\times B \cong B\times A, \]

natural in $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Annihilation With the Empty Set. We have isomorphisms of sets
\begin{align*} A\times \emptyset & \cong \emptyset ,\\ \emptyset \times A & \cong \emptyset , \end{align*}

natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Distributivity Over Unions. We have isomorphisms of sets
\begin{align*} A\times \webleft (B\cup C\webright ) & = \webleft (A\times B\webright )\cup \webleft (A\times C\webright ),\\ \webleft (A\cup B\webright )\times C & = \webleft (A\times C\webright )\cup \webleft (B\times C\webright ). \end{align*}
Distributivity Over Intersections. We have isomorphisms of sets
\begin{align*} A\times \webleft (B\cap C\webright ) & = \webleft (A\times B\webright )\cap \webleft (A\times C\webright ),\\ \webleft (A\cap B\webright )\times C & = \webleft (A\times C\webright )\cap \webleft (B\times C\webright ). \end{align*}
Middle-Four Exchange with Respect to Intersections. We have an isomorphism of sets
\[ \webleft (A\times B\webright )\cap \webleft (C\times D\webright )\cong \webleft (A\cap B\webright )\times \webleft (C\cap D\webright ). \]
Distributivity Over Differences. We have isomorphisms of sets
\begin{align*} A\times \webleft (B\setminus C\webright ) & = \webleft (A\times B\webright )\setminus \webleft (A\times C\webright ),\\ \webleft (A\setminus B\webright )\times C & = \webleft (A\times C\webright )\setminus \webleft (B\times C\webright ), \end{align*}

natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Distributivity Over Symmetric Differences. We have isomorphisms of sets
\begin{align*} A\times \webleft (B\mathbin {\triangle }C\webright ) & = \webleft (A\times B\webright )\mathbin {\triangle }\webleft (A\times C\webright ),\\ \webleft (A\mathbin {\triangle }B\webright )\times C & = \webleft (A\times C\webright )\mathbin {\triangle }\webleft (B\times C\webright ), \end{align*}

natural in $A,B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Symmetric Monoidality. The triple $\webleft (\mathsf{Sets},\times ,\text{pt}\webright )$ is a symmetric monoidal category.
Symmetric Bimonoidality. The quintuple $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset ,\times ,\text{pt}\webright )$ is a symmetric bimonoidal category.

Proof of Proposition 2.1.3.1.2.

Item 1: Functoriality

This follows from

Item 2: Adjointness

We prove only that there’s an adjunction $-\times B\dashv \textup{Hom}_{\mathsf{Sets}}\webleft (B,-\webright )$, witnessed by a bijection

\[ \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,C\webright )\cong \textup{Hom}_{\mathsf{Sets}}\webleft (A,\textup{Hom}_{\mathsf{Sets}}\webleft (B,C\webright )\webright ), \]

natural in $B,C\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, as the proof of the existence of the adjunction $A\times -\dashv \textup{Hom}_{\mathsf{Sets}}\webleft (A,-\webright )$ follows almost exactly in the same way.

Map I. We define a map

\[ \Phi _{B,C}\colon \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,C\webright )\to \textup{Hom}_{\mathsf{Sets}}\webleft (A,\textup{Hom}_{\mathsf{Sets}}\webleft (B,C\webright )\webright ), \]

by sending a function

\[ \xi \colon A\times B\to C \]

to the function
where we define

\[ \xi ^{\dagger }_{a}\webleft (b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a,b\webright ) \]

for each $b\in B$. In terms of the $[\mspace {-3mu}[a\mapsto f\webleft (a\webright )]\mspace {-3mu}]$ notation of Chapter 1: Sets, Notation 1.1.1.1.2, we have

\[ \xi ^{\dagger }\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]]\mspace {-3mu}]. \]
Map II. We define a map

\[ \Psi _{B,C}\colon \textup{Hom}_{\mathsf{Sets}}\webleft (A,\textup{Hom}_{\mathsf{Sets}}\webleft (B,C\webright )\webright ),\to \textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,C\webright ) \]

given by sending a function
to the function

\[ \xi ^{\dagger }\colon A\times B\to C \]

defined by

\begin{align*} \xi ^{\dagger }\webleft (a,b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{ev}_{b}\webleft (\mathrm{ev}_{a}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{ev}_{b}\webleft (\xi _{a}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}\webleft (b\webright )\end{align*}

for each $\webleft (a,b\webright )\in A\times B$.
Invertibility I. We claim that

\[ \Psi _{A,B}\circ \Phi _{A,B}=\text{id}_{\textup{Hom}_{\mathsf{Sets}}\webleft (A\times B,C\webright )}. \]

Indeed, given a function $\xi \colon A\times B\to C$, we have

\begin{align*} \webleft [\Psi _{A,B}\circ \Phi _{A,B}\webright ]\webleft (\xi \webright ) & = \Psi _{A,B}\webleft (\Phi _{A,B}\webleft (\xi \webright )\webright )\\ & = \Psi _{A,B}\webleft (\Phi _{A,B}\webleft ([\mspace {-3mu}[\webleft (a,b\webright )\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]\webright )\webright )\\ & = \Psi _{A,B}\webleft ([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = \Psi _{A,B}\webleft ([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[b'\mapsto \xi \webleft (a',b'\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[\webleft (a,b\webright )\mapsto \mathrm{ev}_{b}\webleft (\mathrm{ev}_{a}\webleft ([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[b'\mapsto \xi \webleft (a',b'\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\webright )]\mspace {-3mu}]\\ & = [\mspace {-3mu}[\webleft (a,b\webright )\mapsto \mathrm{ev}_{b}\webleft ([\mspace {-3mu}[b'\mapsto \xi \webleft (a,b'\webright )]\mspace {-3mu}]\webright )]\mspace {-3mu}]\\ & = [\mspace {-3mu}[\webleft (a,b\webright )\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]\\ & = \xi . \end{align*}
Invertibility II. We claim that

\[ \Phi _{A,B}\circ \Psi _{A,B}=\text{id}_{\textup{Hom}_{\mathsf{Sets}}\webleft (A,\textup{Hom}_{\mathsf{Sets}}\webleft (B,C\webright )\webright )}. \]

Indeed, given a function
we have

\begin{align*} \webleft [\Phi _{A,B}\circ \Psi _{A,B}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{A,B}\webleft (\Psi _{A,B}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{A,B}\webleft ([\mspace {-3mu}[\webleft (a,b\webright )\mapsto \xi _{a}\webleft (b\webright )]\mspace {-3mu}]\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{A,B}\webleft ([\mspace {-3mu}[\webleft (a',b'\webright )\mapsto \xi _{a'}\webleft (b'\webright )]\mspace {-3mu}]\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \mathrm{ev}_{\webleft (a,b\webright )}\webleft ([\mspace {-3mu}[\webleft (a',b'\webright )\mapsto \xi _{a'}\webleft (b'\webright )]\mspace {-3mu}]\webright )]\mspace {-3mu}]]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi _{a}\webleft (b\webright )]\mspace {-3mu}]]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[a\mapsto \xi _{a}]\mspace {-3mu}]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi .\end{align*}
Naturality for $\Phi $, Part I. We need to show that, given a function $g\colon B\to B'$, the diagram

commutes. Indeed, given a function

\[ \xi \colon A\times B'\to C, \]

we have

\begin{align*} \webleft [\Phi _{B,C}\circ \webleft (\text{id}_{A}\times g^{*}\webright )\webright ]\webleft (\xi \webright ) & = \Phi _{B,C}\webleft (\webleft [\text{id}_{A}\times g^{*}\webright ]\webleft (\xi \webright )\webright )\\ & = \Phi _{B,C}\webleft (\xi \webleft (-_{1},g\webleft (-_{2}\webright )\webright )\webright )\\ & = \webleft [\xi \webleft (-_{1},g\webleft (-_{2}\webright )\webright )\webright ]^{\dagger }\\ & = \xi ^{\dagger }_{-_{1}}\webleft (g\webleft (-_{2}\webright )\webright )\\ & = \webleft (g^{*}\webright )_{*}\webleft (\xi ^{\dagger }\webright )\\ & = \webleft (g^{*}\webright )_{*}\webleft (\Phi _{B',C}\webleft (\xi \webright )\webright )\\ & = \webleft [\webleft (g^{*}\webright )_{*}\circ \Phi _{B',C}\webright ]\webleft (\xi \webright ). \end{align*}

Alternatively, using the $[\mspace {-3mu}[a\mapsto f\webleft (a\webright )]\mspace {-3mu}]$ notation of Chapter 1: Sets, Notation 1.1.1.1.2, we have

\begin{align*} \webleft [\Phi _{B,C}\circ \webleft (\text{id}_{A}\times g^{*}\webright )\webright ]\webleft (\xi \webright ) & = \Phi _{B,C}\webleft (\webleft [\text{id}_{A}\times g^{*}\webright ]\webleft (\xi \webright )\webright )\\ & = \Phi _{B,C}\webleft (\webleft [\text{id}_{A}\times g^{*}\webright ]\webleft ([\mspace {-3mu}[\webleft (a,b'\webright )\mapsto \xi \webleft (a,b'\webright )]\mspace {-3mu}]\webright )\webright )\\ & = \Phi _{B,C}\webleft ([\mspace {-3mu}[\webleft (a,b\webright )\mapsto \xi \webleft (a,g\webleft (b\webright )\webright )]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi \webleft (a,g\webleft (b\webright )\webright )]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto g^{*}\webleft ([\mspace {-3mu}[b'\mapsto \xi \webleft (a,b'\webright )]\mspace {-3mu}]\webright )]\mspace {-3mu}]\\ & = \webleft (g^{*}\webright )_{*}\webleft ([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b'\mapsto \xi \webleft (a,b'\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = \webleft (g^{*}\webright )_{*}\webleft (\Phi _{B',C}\webleft ([\mspace {-3mu}[\webleft (a,b'\webright )\mapsto \xi \webleft (a,b'\webright )]\mspace {-3mu}]\webright )\webright )\\ & = \webleft (g^{*}\webright )_{*}\webleft (\Phi _{B',C}\webleft (\xi \webright )\webright )\\ & = \webleft [\webleft (g^{*}\webright )_{*}\circ \Phi _{B',C}\webright ]\webleft (\xi \webright ). \end{align*}
Naturality for $\Phi $, Part II. We need to show that, given a function $h\colon C\to C'$, the diagram

commutes. Indeed, given a function

\[ \xi \colon A\times B\to C, \]

we have

\begin{align*} \webleft [\Phi _{B,C}\circ h_{*}\webright ]\webleft (\xi \webright ) & = \Phi _{B,C}\webleft (h_{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{B,C}\webleft (h_{*}\webleft ([\mspace {-3mu}[\webleft (a,b\webright )\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]\webright )\webright )\\ & = \Phi _{B,C}\webleft ([\mspace {-3mu}[\webleft (a,b\webright )\mapsto h\webleft (\xi \webleft (a,b\webright )\webright )]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto h\webleft (\xi \webleft (a,b\webright )\webright )]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto h_{*}\webleft ([\mspace {-3mu}[b\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = \webleft (h_{*}\webright )_{*}\webleft ([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[b\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]]\mspace {-3mu}]\webright )\\ & = \webleft (h_{*}\webright )_{*}\webleft (\Phi _{B,C}\webleft ([\mspace {-3mu}[\webleft (a,b\webright )\mapsto \xi \webleft (a,b\webright )]\mspace {-3mu}]\webright )\webright )\\ & = \webleft (h_{*}\webright )_{*}\webleft (\Phi _{B,C}\webleft (\xi \webright )\webright )\\ & = \webleft [\webleft (h_{*}\webright )_{*}\circ \Phi _{B,C}\webright ]\webleft (\xi \webright ). \end{align*}
Naturality for $\Psi $. Since $\Phi $ is natural in each argument and $\Phi $ is a componentwise inverse to $\Psi $ in each argument, it follows from Chapter 8: Categories, Item 2 of Proposition 8.8.6.1.2 that $\Psi $ is also natural in each argument.

Item 3: Associativity

See [Proof Wiki, Bijection between $R\times(S\times T)$ and $(R\times S)\times T$].

Item 4: Unitality

Clear.

Item 5: Commutativity

See [Proof Wiki, Bijection between $S\times T$ and $T\times S$].

Item 6: Annihilation With the Empty Set

See [Proof Wiki, Cartesian Product Is Empty Iff Factor Is Empty].

Item 7: Distributivity Over Unions

See [Proof Wiki, Cartesian Product Distributes Over Union].

Item 8: Distributivity Over Intersections

See Corollary 1 of [Proof Wiki, Cartesian Product of Intersections].

Item 9: Middle-Four Exchange With Respect to Intersections

See Corollary 1 of [Proof Wiki, Cartesian Product of Intersections].

Item 10: Distributivity Over Differences

See [Proof Wiki, Cartesian Product Distributes Over Set Difference].

Item 11: Distributivity Over Symmetric Differences

See [Proof Wiki, Cartesian Product Distributes Over Symmetric Difference].

Item 12: Symmetric Monoidality

See [MO 382264].

Item 13: Symmetric Bimonoidality

Omitted.

Footnotes

[1] Further Terminology: Also called the Cartesian product of $A$ and $B$ or the binary Cartesian product of $A$ and $B$, for emphasis.

This can also be thought of as the $\webleft (\mathbb {E}_{-1},\mathbb {E}_{-1}\webright )$-tensor product of $A$ and $B$.

[2] In other words, $A\times B$ is the set whose elements are ordered pairs $\webleft (a,b\webright )$ with $a\in A$ and $b\in B$ as in Definition 2.3.4.1.1

Noticed something off, or have any comments? Feel free to reach out!

You can also use the contact form below: