Let $(M, \otimes, I)$ be a left-closed (non-symmetric) monoidal category with left-internal hom $\underline{\operatorname{hom}}(-,-)$.
Denote by $\sigma_{A,B,C}: M(A\otimes B, C) \xrightarrow{\sim} M(A,\underline{\operatorname{hom}}(B,C))$ the natural isomorphism obtained from the closed monoidal structure.
Consider the evaluation morphism $\operatorname{ev}_{A,B}: \underline{\operatorname{hom}}(A,B) \otimes A \rightarrow B$.
Define for $A,B \in M$ the following morphism $f_{A,B}:= \sigma_{A \otimes \underline{\operatorname{hom}} (I,B),I,A\otimes B}(\operatorname{id}_A \otimes\operatorname{ev}_{I,B})$.
For $A \in M$ let $g_A: \underline{\operatorname{hom}}(I,A) \xrightarrow{\sim} A$ be the isomorphism obtained from the Yoneda lemma.
I am struggling to show that the following equality of morphisms holds for any two objects $A,B \in M$: $$g_{A \otimes B} \circ f_{A,B}=\operatorname{id}_A \otimes g_B.$$
Does this equality even hold? Any ideas on how to prove it?
Best Answer
Drawing all the commutative diagrams and writing all the subscripts is too troublesome, so I will briefly sketch the proof in words instead. Hopefully you will be able to reconstruct the details yourself.
Consider the right unitor $\rho : X \otimes I \to X$. It corresponds under the tensor–hom adjunction to $[I, \rho] \circ \eta : X \to [I, X]$, where $\eta : X \to [I, X \otimes I]$ is the unit of the adjunction. You know that $X \to [I, X]$ is invertible: indeed, its inverse is the isomorphism $g : [I, X] \to X$ you ask about. (Well, I believe it is. Your definition is dependent on the choice of natural isomorphism $X \otimes I \cong I$ but I presume you have made the only truly natural choice, namely $\rho$.) So we find that $g = \epsilon \circ \rho^{-1}$, where $\epsilon : [I, X] \otimes I \to X$ is the counit (i.e. evaluation) and $\rho^{-1} : [I, X] \to [I, X] \otimes I$ is the inverse unitor.
The morphism $f : A \otimes [I, B] \to [I, A \otimes B]$ you define is given by $[I, (A \otimes \epsilon) \circ \alpha] \circ \eta$, where $\alpha : (A \otimes [I, B]) \otimes I \to A \otimes ([I, B] \otimes I)$ is the associator. Thus, your question becomes: is $$ A \otimes [I, B] \xrightarrow{A \otimes \rho^{-1}} A \otimes ([I, B] \otimes I) \xrightarrow{A \otimes \epsilon} A \otimes B $$ equal to the following composite? \begin{multline} A \otimes [I, B] \xrightarrow{\eta} [I, (A \otimes [I, B]) \otimes I] \xrightarrow{[I, \alpha]} [ I, A \otimes ([I, B] \otimes I)] \xrightarrow{[I, A \otimes \epsilon]} [I, A \otimes B] \\ \xrightarrow{\rho^{-1}} [I, A \otimes B] \otimes I \xrightarrow{\epsilon} A \otimes B \end{multline}
The answer is yes, of course. Since all of the morphisms involved are invertible, it suffices to show that the composite \begin{multline} A \otimes [I, B] \xrightarrow{\eta} [I, (A \otimes [I, B]) \otimes I] \xrightarrow{[I, \alpha]} [ I, A \otimes ([I, B] \otimes I)] \xrightarrow{[I, A \otimes \epsilon]} [I, A \otimes B] \\ \xrightarrow{\rho^{-1}} [I, A \otimes B] \otimes I \xrightarrow{\epsilon} A \otimes B \xrightarrow{A \otimes \epsilon^{-1}} A \otimes ([I, B] \otimes I) \xrightarrow{A \otimes \rho} A \otimes [I, B] \end{multline} is the identity. Using naturality to shuffle $\rho$ around, it eventually boils down to two identities: $$ (A \otimes [I, B]) \otimes I \xrightarrow{\alpha} A \otimes ([I, B] \otimes I) \xrightarrow{A \otimes \rho} A \otimes [I, B] $$ is equal to $\rho : (A \otimes [I, B]) \otimes I \to A \otimes [I, B]$, and $$ (A \otimes [I, B]) \otimes I \xrightarrow{\eta \otimes I} [I, (A \otimes [I, B]) \otimes I] \otimes I \xrightarrow{\epsilon} (A \otimes [I, B]) \otimes I $$ is the identity.