Subsection 4.2.1 (00CG): Tensors of Pointed Sets by 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`

4.2.1 Tensors of Pointed Sets by Sets

Let $\webleft (X,x_{0}\webright )$ be a pointed set and let $A$ be a set.

Definition 4.2.1.1.1 ▶ Tensors of Pointed Sets by Sets

The tensor of $\webleft (X,x_{0}\webright )$ by $A$^[1] is the pointed set ^[2] $A\odot \webleft (X,x_{0}\webright )$ satisfying the following universal property:

We have a bijection

\[ \mathsf{Sets}_{*}\webleft (A\odot X,K\webright )\cong \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright ), \]

natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.

Remark 4.2.1.1.2 ▶ Unwinding Definition 4.2.1.1.1

The universal property in Definition 4.2.1.1.1 is equivalent to the following one:

We have a bijection

\[ \mathsf{Sets}_{*}\webleft (A\odot X,K\webright ) \cong \mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright ), \]

natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, where $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright )$ is the set defined by

\[ \mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ f\in \mathsf{Sets}\webleft (A\times X,K\webright )\ \middle |\ \begin{aligned} & \text{for each $a\in A$, we}\\ & \text{have $f\webleft (a,x_{0}\webright )=k_{0}$}\end{aligned} \webright\} . \]

Proof of Remark 4.2.1.1.2.

We claim we have a bijection

\[ \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )\cong \mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright ) \]

natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$. Indeed, this bijection is a restriction of the bijection

\[ \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (X,K\webright )\webright )\cong \mathsf{Sets}\webleft (A\times X,K\webright ) \]

of Chapter 2: Constructions With Sets, Item 2 of Proposition 2.1.3.1.2:

A map
in $\mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )$ gets sent to the map

\[ \xi ^{\dagger }\colon A\times X\to K \]

defined by

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

for each $\webleft (a,x\webright )\in A\times X$, which indeed lies in $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright )$, as we have

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

for each $a\in A$, where we have used that $\xi _{a}\in \mathsf{Sets}_{*}\webleft (X,K\webright )$ is a morphism of pointed sets.
Conversely, a map

\[ \xi \colon A\times X\to K \]

in $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright )$ gets sent to the map
where

\[ \xi ^{\dagger }_{a}\colon X \to K \]

is the map defined by

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

for each $x\in X$, and indeed lies in $\mathsf{Sets}_{*}\webleft (X,K\webright )$, as we have

\begin{align*} \xi ^{\dagger }_{a}\webleft (x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a,x_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}k_{0}.\end{align*}

This finishes the proof.

Construction 4.2.1.1.3 ▶ Construction of Tensors of Pointed Sets by Sets

Concretely, the tensor of $\webleft (X,x_{0}\webright )$ by $A$ is the pointed set $A\odot \webleft (X,x_{0}\webright )$ consisting of:

The Underlying Set. The set $A\odot X$ given by

\[ A\odot X\cong \bigvee _{a\in A}\webleft (X,x_{0}\webright ), \]

where $\bigvee _{a\in A}\webleft (X,x_{0}\webright )$ is the wedge product of the $A$-indexed family $\webleft (\webleft (X,x_{0}\webright )\webright )_{a\in A}$ of Chapter 3: Pointed Sets, Definition 3.3.2.1.1.
The Basepoint. The point $\webleft [\webleft (a,x_{0}\webright )\webright ]=\webleft [\webleft (a',x_{0}\webright )\webright ]$ of $\bigvee _{a\in A}\webleft (X,x_{0}\webright )$.

Proof of Construction 4.2.1.1.3.

(Proven below in a bit.)

Notation 4.2.1.1.4 ▶ Elements of Tensors of Pointed Sets by Sets

We write $a\odot x$ for the element $\webleft [\webleft (a,x\webright )\webright ]$ of

\begin{align*} A\odot X & \cong \bigvee _{a\in A}\webleft (X,x_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\coprod _{i\in I}X_{i}\webright )/\mathord {\sim }.\end{align*}

Remark 4.2.1.1.5 ▶ Basepoints of Tensors of Pointed Sets by Sets

Taking the tensor of any element of $A$ with the basepoint $x_{0}$ of $X$ leads to the same element in $A\odot X$, i.e. we have

\[ a\odot x_{0}=a'\odot x_{0}, \]

for each $a,a'\in A$. This is due to the equivalence relation $\mathord {\sim }$ on

\[ \bigvee _{a\in A}\webleft (X,x_{0}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\coprod _{a\in A}X/\mathord {\sim } \]

identifying $\webleft (a,x_{0}\webright )$ with $\webleft (a',x_{0}\webright )$, so that the equivalence class $a\odot x_{0}$ is independent from the choice of $a\in A$.

Proof of Construction 4.2.1.1.3.

We claim we have a bijection

\[ \mathsf{Sets}_{*}\webleft (A\odot X,K\webright )\cong \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright ) \]

natural in $\webleft (K,k_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.

Map I. We define a map

\[ \Phi _{K}\colon \mathsf{Sets}_{*}\webleft (A\odot X,K\webright ) \to \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright ) \]

by sending a morphism of pointed sets

\[ \xi \colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ) \]

to the map of sets
where

\[ \xi _{a}\colon \webleft (X,x_{0}\webright )\to \webleft (K,k_{0}\webright ) \]

is the morphism of pointed sets defined by

\[ \xi _{a}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a\odot x\webright ) \]

for each $x\in X$. Note that we have

\begin{align*} \xi _{a}\webleft (x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (a\odot x_{0}\webright )\\ & = k_{0},\end{align*}

so that $\xi _{a}$ is indeed a morphism of pointed sets, where we have used that $\xi $ is a morphism of pointed sets.
Map II. We define a map

\[ \Psi _{K}\colon \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )\to \mathsf{Sets}_{*}\webleft (A\odot X,K\webright ) \]

given by sending a map
to the morphism of pointed sets

\[ \xi ^{\dagger }\colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ) \]

defined by

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

for each $a\odot x\in A\odot X$. Note that $\xi ^{\dagger }$ is indeed a morphism of pointed sets, as we have

\begin{align*} \xi ^{\dagger }\webleft (a\odot x_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}\webleft (x_{0}\webright )\\ & = k_{0}, \end{align*}

where we have used that $\xi \webleft (a\webright )\in \mathsf{Sets}_{*}\webleft (X,K\webright )$ is a morphism of pointed sets.
Invertibility I. We claim that

\[ \Psi _{K}\circ \Phi _{K}=\text{id}_{\mathsf{Sets}_{*}\webleft (A\odot X,K\webright )}. \]

Indeed, given a morphism of pointed sets

\[ \xi \colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ), \]

we have

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

\[ \Phi _{K}\circ \Psi _{K}=\text{id}_{\mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright )}. \]

Indeed, given a morphism $\xi \colon A\to \mathsf{Sets}_{*}\webleft (X,K\webright )$, we have

\begin{align*} \webleft [\Phi _{K}\circ \Psi _{K}\webright ]\webleft (\xi \webright ) & = \Phi _{K}\webleft (\Psi _{K}\webleft (\xi \webright )\webright )\\ & = \Phi _{K}\webleft ([\mspace {-3mu}[a\odot x\mapsto \xi _{a}\webleft (x\webright )]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[x\mapsto \xi _{a}\webleft (x\webright )]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto \xi \webleft (a\webright )]\mspace {-3mu}]\\ & = \xi .\end{align*}
Naturality of $\Phi $. We need to show that, given a morphism of pointed sets

\[ \phi \colon \webleft (K,k_{0}\webright )\to \webleft (K',k'_{0}\webright ), \]

the diagram

commutes. Indeed, given a morphism of pointed sets

\[ \xi \colon \webleft (A\odot X,a\odot x_{0}\webright )\to \webleft (K,k_{0}\webright ), \]

we have

\begin{align*} \webleft [\Phi _{K'}\circ \phi _{*}\webright ]\webleft (\xi \webright ) & = \Phi _{K'}\webleft (\phi _{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{K'}\webleft (\phi \circ \xi \webright )\\ & = \webleft (\phi \circ \xi \webright )^{\dagger }\\ & = [\mspace {-3mu}[a\mapsto \phi \circ \xi \webleft (a\odot -\webright )]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto \phi _{*}\webleft (\xi \webleft (a\odot -\webright )\webright )]\mspace {-3mu}]\\ & = \webleft (\phi _{*}\webright )_{*}\webleft ([\mspace {-3mu}[a\mapsto \xi \webleft (a\odot -]\mspace {-3mu}]\webright )\webright )\\ & = \webleft (\phi _{*}\webright )_{*}\webleft (\Phi _{K}\webleft (\xi \webright )\webright )\\ & = \webleft [\webleft (\phi _{*}\webright )_{*}\circ \Phi _{K}\webright ]\webleft (\xi \webright ). \end{align*}
Naturality of $\Psi $. Since $\Phi $ is natural and $\Phi $ is a componentwise inverse to $\Psi $, it follows from Chapter 8: Categories, Item 2 of Proposition 8.8.6.1.2 that $\Psi $ is also natural.

This finishes the proof.

Proposition 4.2.1.1.6 ▶ Properties of Tensors of Pointed Sets by Sets

Let $\webleft (X,x_{0}\webright )$ be a pointed set and let $A$ be a set.

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

In particular, given:
- A map of sets $f\colon A\to B$;
- A pointed map $\phi \colon \webleft (X,x_{0}\webright )\to \webleft (Y,y_{0}\webright )$;
the induced map

\[ f\odot \phi \colon A\odot X\to B\odot Y \]

is given by

\[ \webleft [f\odot \phi \webright ]\webleft (a\odot x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (a\webright )\odot \phi \webleft (x\webright ) \]

for each $a\odot x\in A\odot X$.
Adjointness I. We have an adjunction
witnessed by a bijection
\[ \mathsf{Sets}_{*}\webleft (A\odot X,K\webright )\cong \mathsf{Sets}\webleft (A,\mathsf{Sets}_{*}\webleft (X,K\webright )\webright ), \]

natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Adjointness II. We have an adjunctions
witnessed by a bijection
\[ \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (A\odot X,Y\webright )\cong \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X,A\pitchfork Y\webright ), \]

natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
As a Weighted Colimit. We have
\[ A\odot X\cong \text{colim}^{\webleft [A\webright ]}\webleft (X\webright ), \]

where in the right hand side we write:
- $A$ for the functor $A\colon \text{pt}\to \mathsf{Sets}$ picking $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$;
- $X$ for the functor $X\colon \text{pt}\to \mathsf{Sets}_{*}$ picking $\webleft (X,x_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Iterated Tensors. We have an isomorphism of pointed sets
\[ A\odot \webleft (B\odot X\webright )\cong \webleft (A\times B\webright )\odot X, \]

natural in $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $\webleft (X,x_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Interaction With Homs. We have a natural isomorphism
\[ \mathsf{Sets}_{*}\webleft (A\odot X,-\webright )\cong A\pitchfork \mathsf{Sets}_{*}\webleft (X,-\webright ). \]
The Tensor Evaluation Map. For each $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, we have a map
\[ \mathrm{ev}^{\odot }_{X,Y}\colon \mathsf{Sets}_{*}\webleft (X,Y\webright )\odot X\to Y, \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, and given by

\[ \mathrm{ev}^{\odot }_{X,Y}\webleft (f\odot x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright ) \]

for each $f\odot x\in \mathsf{Sets}_{*}\webleft (X,Y\webright )\odot X$.
The Tensor Coevaluation Map. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and each $X\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, we have a map
\[ \mathrm{coev}^{\odot }_{A,X}\colon A\to \mathsf{Sets}_{*}\webleft (X,A\odot X\webright ), \]

natural in $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $X\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, and given by

\[ \mathrm{coev}^{\odot }_{A,X}\webleft (a\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[\mspace {-3mu}[x\mapsto a\odot x]\mspace {-3mu}] \]

for each $a\in A$.