About the internal hom in a symmetric monoidal closed category

Question

Let $\mathcal{C}$ be a symmetric monoidal closed category. My question is the following:

Given three objects $X$, $Y$ and $Z$, and a morphism $f \colon Y \to Z$ in $\mathcal{C}$, does it necessarily exist a morphism from $X \multimap Y$ to $X \multimap Z$ in $\mathcal{C}$?

By $X \multimap Y$ I denote the internal hom object of $X$ and $Y$, also denoted by $[X,Y]$ in some contexts.

I know that the answer to my question is positive in the category $\mathbf{Set}$ of sets (which is symmetric monoidal closed), where $X \multimap Y = Y^X$ is the set of functions from $X$ to $Y$: in this case, given $f \colon Y \to Z$, the morphism from $X \multimap Y$ to $X \multimap Z$ is just the function associating with every $g \colon X \to Y$ the function $f \circ g \colon X \to Z$.

My question is related to the study of linear logic, since symmetric monoidal closed categories provide a natural interpretation of the multiplicative intuitionistic fragment of linear logic.

Answer 1

Yes. The internal hom constitutes a bifunctor $(-)\multimap (-):\mathcal{C}^{\mathrm{op}}\times \mathcal{C}\to \mathcal{C}$, just as in $\mathbf{Set}$. This follows from the adjunction isomorphism between the internal hom and the tensor, and the fact that the tensor is a bifunctor.

More formally, given $f:Y\to Z$, the postcomposition morphism $X\multimap f:X\multimap Y\to X\multimap Z$ must correspond to a morphism $(X\multimap Y)\otimes X\to Z$. The morphism that answers to that description is the composition $f\circ \mathrm{ev}$, where $\mathrm{ev}:(X\multimap Y)\otimes X\to Y$ is the evaluation map, the counit of the hom-tensor adjunction. So, morally, the map is simply $(X\multimap f)(g)(x)=f(g(x))$, as one would hope.

Answer 2

In addition to the direct approach from Kevin Carlson's answer, another way to view this would be via the Yoneda lemma, i.e. consider the functors $\operatorname{Hom}(-, X) : \mathcal{C}^{\mathrm{op}} \to \mathrm{Sets}$ in place of $X$. Then, the map you want corresponds to $$ \operatorname{Hom}(-, X \multimap Y) \simeq \operatorname{Hom}(- \otimes X, Y) \overset{f \circ}{\rightarrow} \operatorname{Hom}(- \otimes X, Z) \simeq \operatorname{Hom}(-, X \multimap Z).$$ By the Yoneda lemma, this morphism of functors corresponds to a unique morphism in $\operatorname{Hom}(X \multimap Y, X \multimap Z)$.