4.1.3 Binary Products of Sets

    Let $A$ and $B$ be sets.

    Definition 4.1.3.1.1 ▶ Binary Products of Sets

    The product of $A$ and $B$1 is the product of $A$ and $B$ in $\mathsf{Sets}$ as in Unresolved reference, Unresolved reference.

    1. 1Further Terminology: Also called the Cartesian product of $A$ and $B$.
    Construction 4.1.3.1.2 ▶ Construction of Binary Products of Sets

    Concretely, the product of $A$ and $B$ is the pair $\smash {\webleft (A\times B,\left\{ \operatorname {\mathrm{\mathrm{pr}}}_{1},\operatorname {\mathrm{\mathrm{pr}}}_{2}\right\} \webright )}$ consisting of:

    1. 1.

      The Limit. The set $A\times B$ defined by

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

      The Cone. The maps

      \begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1} & \colon A\times B\to A,\\ \operatorname {\mathrm{\mathrm{pr}}}_{2} & \colon A\times B\to B \end{align*}

      defined by

      \begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1}\webleft (a,b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}a,\\ \operatorname {\mathrm{\mathrm{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 Construction 4.1.3.1.2.

    We claim that $A\times B$ is the categorical product of $A$ and $B$ in the category of 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*} \operatorname {\mathrm{\mathrm{pr}}}_{1}\circ \phi & = p_{1},\\ \operatorname {\mathrm{\mathrm{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 4.1.3.1.3 ▶ Properties of Products of Sets

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

    1. 1.

      Functoriality. The assignments $A,B,\webleft (A,B\webright )\mapsto A\times B$ define functors

      \[ \begin{array}{ccc} A\times -\colon \mkern -15mu & \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets},\\ -\times B\colon \mkern -15mu & \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets},\\ -_{1}\times -_{2}\colon \mkern -15mu & \mathsf{Sets}\times \mathsf{Sets} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets}, \end{array} \]

      where $-_{1}\times -_{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}\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 \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, the action on $\operatorname {\mathrm{Hom}}$-sets

        \[ \mathord {\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 \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 2.

    Adjointness I. We have adjunctions

    witnessed by bijections

    \begin{align*} \mathsf{Sets}\webleft (A\times B,C\webright ) & \cong \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,C\webright )\webright ),\\ \mathsf{Sets}\webleft (A\times B,C\webright ) & \cong \mathsf{Sets}\webleft (B,\mathsf{Sets}\webleft (A,C\webright )\webright ), \end{align*}

    natural in $A,B,C\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 3.

    Adjointness II. We have an adjunction

    witnessed by a bijection

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

    natural in $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and in $\webleft (B,C\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\times \mathsf{Sets}\webright )$.

  • 4.

    Associativity. We have an isomorphism of sets

    \[ \alpha ^{\mathsf{Sets}}_{A,B,C}\colon \webleft (A\times B\webright )\times C\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A\times \webleft (B\times C\webright ), \]

    natural in $A,B,C\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 5.

    Unitality. We have isomorphisms of sets

    \begin{align*} \lambda ^{\mathsf{Sets}}_{A} & \colon \mathrm{pt}\times A \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A,\\ \rho ^{\mathsf{Sets}}_{A} & \colon A\times \mathrm{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }A, \end{align*}

    natural in $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 6.

    Commutativity. We have an isomorphism of sets

    \[ \sigma ^{\mathsf{Sets}}_{A,B}\colon A\times B \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }B\times A, \]

    natural in $A,B\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 7.

    Distributivity Over Coproducts. We have isomorphisms of sets

    \begin{align*} \delta ^{\mathsf{Sets}}_{\ell } & \colon A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright ) \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (A\times C\webright ),\\ \delta ^{\mathsf{Sets}}_{r} & \colon \webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B\webright )\times C \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times C\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (B\times C\webright ), \end{align*}

    natural in $A,B,C\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 8.

    Annihilation With the Empty Set. We have isomorphisms of sets

    \begin{align*} \zeta ^{\mathsf{Sets}}_{\ell } & \colon \text{Ø}\times A \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{Ø},\\ \zeta ^{\mathsf{Sets}}_{r} & \colon A\times \text{Ø}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{Ø}, \end{align*}

    natural in $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

  • 9.

    Distributivity Over Unions. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities

    \begin{align*} U\times \webleft (V\cup W\webright ) & = \webleft (U\times V\webright )\cup \webleft (U\times W\webright ),\\ \webleft (U\cup V\webright )\times W & = \webleft (U\times W\webright )\cup \webleft (V\times W\webright ) \end{align*}

    of subsets of $\mathcal{P}\webleft (X\times X\webright )$.

  • 10.

    Distributivity Over Intersections. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities

    \begin{align*} U\times \webleft (V\cap W\webright ) & = \webleft (U\times V\webright )\cap \webleft (U\times W\webright ),\\ \webleft (U\cap V\webright )\times W & = \webleft (U\times W\webright )\cap \webleft (V\times W\webright ) \end{align*}

    of subsets of $\mathcal{P}\webleft (X\times X\webright )$.

  • 11.

    Distributivity Over Differences. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities

    \begin{align*} U\times \webleft (V\setminus W\webright ) & = \webleft (U\times V\webright )\setminus \webleft (U\times W\webright ),\\ \webleft (U\setminus V\webright )\times W & = \webleft (U\times W\webright )\setminus \webleft (V\times W\webright ) \end{align*}

    of subsets of $\mathcal{P}\webleft (X\times X\webright )$.

  • 12.

    Distributivity Over Symmetric Differences. Let $X$ be a set. For each $U,V,W\in \mathcal{P}\webleft (X\webright )$, we have equalities

    \begin{align*} U\times \webleft (V\mathbin {\triangle }W\webright ) & = \webleft (U\times V\webright )\mathbin {\triangle }\webleft (U\times W\webright ),\\ \webleft (U\mathbin {\triangle }V\webright )\times W & = \webleft (U\times W\webright )\mathbin {\triangle }\webleft (V\times W\webright ) \end{align*}

    of subsets of $\mathcal{P}\webleft (X\times X\webright )$.

  • 13.

    Middle-Four Exchange with Respect to Intersections. The diagram

    commutes, i.e. we have

    \[ \webleft (U\times V\webright )\cap \webleft (W\times T\webright )=\webleft (U\cap V\webright )\times \webleft (W\cap T\webright ). \]

    for each $U,V,W,T\in \mathcal{P}\webleft (X\webright )$.

  • 14.

    Symmetric Monoidality. The 8-tuple $\left(\phantom{\mathrlap {\alpha ^{\mathsf{Sets}}}}\mathsf{Sets}\right.$, $\times $, $\mathrm{pt}$, $\mathsf{Sets}\webleft (-_{1},-_{2}\webright )$, $\alpha ^{\mathsf{Sets}}$, $\lambda ^{\mathsf{Sets}}$, $\rho ^{\mathsf{Sets}}$, $\left.\sigma ^{\mathsf{Sets}}\right)$ is a closed symmetric monoidal category.

  • 15.

    Symmetric Bimonoidality. The 18-tuple

    \[ \begin{aligned} & \left(\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\times ,\text{Ø},\mathrm{pt},\mathsf{Sets}\webleft (-_{1},-_{2}\webright ),\alpha ^{\mathsf{Sets}},\lambda ^{\mathsf{Sets}},\rho ^{\mathsf{Sets}},\sigma ^{\mathsf{Sets}},\right.\\ & \left.\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 }}},\sigma ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\delta ^{\mathsf{Sets}}_{\ell },\delta ^{\mathsf{Sets}}_{r},\zeta ^{\mathsf{Sets}}_{\ell },\zeta ^{\mathsf{Sets}}_{r}\right),\end{aligned} \]

    is a symmetric closed bimonoidal category, where $\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 }}}$, and $\sigma ^{\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}$ are the natural transformations from Item 3, Item 4, and Item 5 of Proposition 4.2.3.1.3.

    • Proof of Proposition 4.1.3.1.3.

    Item 1: Functoriality
    This follows from Unresolved reference, Unresolved reference of Unresolved reference.

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

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

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

    • •

      Map I. We define a map

      \[ \Phi _{B,C}\colon \mathsf{Sets}\webleft (A\times B,C\webright )\to \mathsf{Sets}\webleft (A,\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 3: Sets, Notation 3.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 \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,C\webright )\webright ),\to \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}=\operatorname {\mathrm{id}}_{\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}=\operatorname {\mathrm{id}}_{\mathsf{Sets}\webleft (A,\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 (\operatorname {\mathrm{id}}_{A}\times g^{*}\webright )\webright ]\webleft (\xi \webright ) & = \Phi _{B,C}\webleft (\webleft [\operatorname {\mathrm{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 3: Sets, Notation 3.1.1.1.2, we have

      \begin{align*} \webleft [\Phi _{B,C}\circ \webleft (\operatorname {\mathrm{id}}_{A}\times g^{*}\webright )\webright ]\webleft (\xi \webright ) & = \Phi _{B,C}\webleft (\webleft [\operatorname {\mathrm{id}}_{A}\times g^{*}\webright ]\webleft (\xi \webright )\webright )\\ & = \Phi _{B,C}\webleft (\webleft [\operatorname {\mathrm{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 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\Psi $ is also natural in each argument.

    This finishes the proof.

    Item 3: Adjointness II
    This follows from the universal property of the product.

    Item 4: Associativity
    This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.1.4.1.1.

    Item 5: Unitality
    This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.1.5.1.1 and Definition 5.1.6.1.1.

    Item 6: Commutativity
    This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.1.7.1.1.

    Item 7: Distributivity Over Coproducts
    This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.1.1.1 and Definition 5.3.2.1.1.

    Item 8: Annihilation With the Empty Set
    This is proved in the proof of Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.3.1.1 and Definition 5.3.4.1.1.

    Item 9: Distributivity Over Unions
    See [Proof Wiki Contributors, Cartesian Product Distributes Over Union — Proof Wiki].

    Item 10: Distributivity Over Intersections
    See Corollary 1 of [Proof Wiki Contributors, Cartesian Product of Intersections — Proof Wiki].

    Item 11: Distributivity Over Differences
    See [Proof Wiki Contributors, Cartesian Product Distributes Over Set Difference — Proof Wiki].

    Item 12: Distributivity Over Symmetric Differences
    See [Proof Wiki Contributors, Cartesian Product Distributes Over Symmetric Difference — Proof Wiki].

    Item 13: Middle-Four Exchange With Respect to Intersections
    See Corollary 1 of [Proof Wiki Contributors, Cartesian Product of Intersections — Proof Wiki].

    Item 14: Symmetric Monoidality
    This is a repetition of Chapter 5: Monoidal Structures on the Category of Sets, Proposition 5.1.9.1.1, and is proved there.

    Item 15: Symmetric Bimonoidality
    This is a repetition of Chapter 5: Monoidal Structures on the Category of Sets, Proposition 5.3.5.1.1, and is proved there.

    Remark 4.1.3.1.4 ▶ The Cartesian Product of Sets as an $\webleft (\mathbb {E}_{k},\mathbb {E}_{\ell }\webright )$-Tensor Product

    As shown in Item 1 of Proposition 4.1.3.1.3, the Cartesian product of sets defines a functor

    \[ -_{1}\times -_{2}\colon \mathsf{Sets}\times \mathsf{Sets}\to \mathsf{Sets}. \]

    This functor is the $\webleft (k,\ell \webright )=\webleft (-1,-1\webright )$ case of a family of functors

    \[ \otimes _{k,\ell }\colon \mathsf{Mon}_{\mathbb {E}_{k}}\webleft (\mathsf{Sets}\webright )\times \mathsf{Mon}_{\mathbb {E}_{\ell }}\webleft (\mathsf{Sets}\webright )\to \mathsf{Mon}_{\mathbb {E}_{k+\ell }}\webleft (\mathsf{Sets}\webright ) \]

    of tensor products of $\mathbb {E}_{k}$-monoid objects on $\mathsf{Sets}$ with $\mathbb {E}_{\ell }$-monoid objects on $\mathsf{Sets}$; see Unresolved reference.

    Remark 4.1.3.1.5 ▶ Diagrams for Item 9, Item 10, Item 11, and Item 12 of Proposition 4.1.3.1.3
Up

View Item 2 as PDF
6 tags refer to this tag
Statistics Cite

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

You can also use the contact form below: