Remark 7.2.1.1.5 (00CM): Basepoints of Tensors of Pointed Sets by Sets

7.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 7.2.1.1.1 ▶ Tensors of Pointed Sets by Sets

The tensor of $\webleft (X,x_{0}\webright )$ by $A$¹ is the tensor $A\odot \webleft (X,x_{0}\webright )$² of $\webleft (X,x_{0}\webright )$ by $A$ as in , .

¹Further Terminology: Also called the copower of $\webleft (X,x_{0}\webright )$ by $A$.
²Further Notation: Often written $A\odot X$ for simplicity.

Remark 7.2.1.1.2 ▶ Unwinding Definition 7.2.1.1.1

In detail, the tensor of $\webleft (X,x_{0}\webright )$ by $A$ is the pointed set $A\odot \webleft (X,x_{0}\webright )$ satisfying the following universal property:

(★)

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

This universal property is in turn equivalent to the following one:

(★)

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

\[ \mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}\webleft (A\times X,K\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ 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} \right\} . \]

Proof of the Equivalence in Remark 7.2.1.1.2.

We claim that 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 \operatorname {\mathrm{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 4: Constructions With Sets, Item 2 of Proposition 4.1.3.1.3:

•
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 7.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 6: Pointed Sets, Definition 6.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 7.2.1.1.3.

(Proven below in a bit.)

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

1.
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.
2.
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.
3.
Invertibility I. We claim that

\[ \Psi _{K}\circ \Phi _{K}=\operatorname {\mathrm{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*}
4.
Invertibility II. We claim that

\[ \Phi _{K}\circ \Psi _{K}=\operatorname {\mathrm{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*}
5.
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*}
6.
Naturality of $\Psi $. Since $\Phi $ is natural and $\Phi $ is a componentwise inverse to $\Psi $, it follows from Chapter 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\Psi $ is also natural.

This finishes the proof.

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

1.
Functoriality. The assignments $A,\webleft (X,x_{0}\webright ),\webleft (A,\webleft (X,x_{0}\webright )\webright )$ define functors

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

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$.
2.
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 \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and $X,Y\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{*}\webright )$.
3.
Adjointness II. We have an adjunctions
witnessed by a bijection

\[ \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}\webleft (A\odot X,Y\webright )\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}\webleft (X,A\pitchfork Y\webright ), \]

natural in $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and $X,Y\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{*}\webright )$.
4.
As a Weighted Colimit. We have

\[ A\odot X\cong \operatorname {\mathrm{colim}}^{\webleft [A\webright ]}\webleft (X\webright ), \]

where in the right hand side we write:
- •
  $A$ for the functor $A\colon \mathrm{pt}\to \mathsf{Sets}$ picking $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$;
- •
  $X$ for the functor $X\colon \mathrm{pt}\to \mathsf{Sets}_{*}$ picking $\webleft (X,x_{0}\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{*}\webright )$.
5.
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 \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and $\webleft (X,x_{0}\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{*}\webright )$.
6.
Interaction With Homs. We have a natural isomorphism

\[ \mathsf{Sets}_{*}\webleft (A\odot X,-\webright )\cong A\pitchfork \mathsf{Sets}_{*}\webleft (X,-\webright ). \]
7.
The Tensor Evaluation Map. For each $X,Y\in \operatorname {\mathrm{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 \operatorname {\mathrm{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$.
8.
The Tensor Coevaluation Map. For each $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and each $X\in \operatorname {\mathrm{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 \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ and $X\in \operatorname {\mathrm{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$.