Every (set) natural transformation is strong

119 Views Asked by At

It is well known that every functor $F : \mathcal{Set} \to \mathcal{Set}$ comes with a strength $s_F : F(A) \times B \to F(A\times B)$.

Now, let $F, G : \mathcal{Set} \to \mathcal{Set}$ be endofunctors on $\mathcal{Set}$, and $\tau : F \to G$ a natural transformation between them.

How can I prove that $\tau$ commutes with $s$? That is, $\tau \circ s_F = s_G \circ (\tau \times \mathrm{id}) : F(A) \times B \to G(A \times B)$.

1

There are 1 best solutions below

0
On BEST ANSWER

For convenience, I'm going to flip the arguments of $s_F$, i.e. I'll have $s_F : A\times F(B)\to F(A\times B)$. As you wrote in the comment, $s_F(a,x)=F(b\mapsto(a,b))(x)$ using the informal $\mapsto$ notation instead of naming a function as you did with $w_b$, or $s_F(a,x)=F(\lambda b.(a,b))(x)$ using the more formal lambda notation. What makes $F$ strong is that $F$'s action on arrows is itself a set function, i.e. an arrow of $\mathbf{Set}$. That is, for every $A$ and $B$, we have an arrow $B^A\to F(B)^{F(A)}$ that "internalizes" the action of $F$ on $\mathsf{Hom}(A,B)$.

There's two ways of producing such a function given the strength $s_F$. We can start with $\mathsf{Hom}(C,B^A)\cong\mathsf{Hom}(C\times A,B)$, apply $F$ to get $\mathsf{Hom}(F(C\times A),F(B))$, precompose with $s_F$ giving $\mathsf{Hom}(C\times F(A),F(B))$ and then use the currying isomorphism to produce $\mathsf{Hom}(C,F(B)^{F(A)})$. This is natural in $C$, and so, by Yoneda, it gives an arrow $B^A\to F(B)^{F(A)}$. Alternatively, we can consider the component of $s_F$ at $B^A$ producing $$B^A\times F(A)\stackrel{s_F}{\to}F(B^A\times A)\stackrel{\varepsilon}{\to}F(B)$$ and then curry this to produce an arrow $\mathsf{curry}(\varepsilon\circ s_F):B^A\to F(B)^{F(A)}$ where $\varepsilon : B^A\times A\to B$ is the counit of the adjunction for Cartesian closure, and corresponds to function application. The laws for the strength make this resulting arrow behave like we'd expect an "internalization" of $F$ would.

The previous paragraph was a bit of an aside. Write $\tilde s_F$ for the currying of $s_F$, i.e. $\tilde s_F(a)=x\mapsto s_F(a,x)= F(b\mapsto(a,b))$. For each $a\in A$, $\tilde s_F(a)\in F(A\times B)^{F(B)}$, or, since for $\mathbf{Set}$, $B^A\cong\mathsf{Hom}(A,B)$, $\tilde s_F(a)\in\mathsf{Hom}(F(B),F(A\times B))$. Given a natural transformation $\tau : F \to G$, naturality of $\tau$ means $$\require{AMScd}\begin{CD} F(B) @>\tau_B>> G(B) \\ @VF(b\mapsto(a,b))=\tilde s_FVV @VV\tilde s_G=G(b\mapsto(a,b))V \\ F(A\times B) @>>\tau_{A\times B}> G(A\times B) \end{CD}$$

Uncurrying the map $a\mapsto \tau_{A\times B}\circ\tilde s_F(a) = a\mapsto \tilde s_G(a)\circ\tau_B$ gives an arrow $A\times F(B)\to G(A\times B)$. Let the left hand side be represented by $l$ defined as $l(a,x)=\tau_{A\times B}(s_F(a,x))$ and the right hand side $r(a,x)=s_G(a,\tau_B(x))$, the equation is $l = r$, which is to say, $\tau_{A\times B}\circ s_F = s_G\circ(id\times\tau_B)$.