Construct an internal hom functor for a closed monoidal category

Question

I am studying closed monoidal category through Wikipedia and nLab. There could be misconceptions in my post. Please let me know in that case.

Definition of a Closed Monoidal Category

Let $M$ be a symmetric monoidal category. $M$ is closed if and only if there are:

1. an assignment $[-,-]$, called an internal hom of $M$, sending each pair $(b,c)$ of objects in $M$ to some object $[b,c]$ in $M$, and each pair $(1_b,h)$ of morphisms in $M$ to some morphism $[1_b,h]$ in $M$, and
2. an assignment $\eta$, called currying of $M$, sending each triple $(a,b,c)$ of objects in $M$ to some function $\eta_{a,b,c}:\operatorname{Hom}(a\otimes b,c)\to\operatorname{Hom}(a,[b,c])$,

such that for all object $b$ in $M$:

1. $[b,-]$, sending $c$ to $[b,c]$ and $h$ to $[1_b,h]$, is a functor;
2. $\eta_{-,b,-}:\operatorname{Hom}(-\otimes b,-)\to\operatorname{Hom}(-,[b,-])$ is a natural isomorphism.

(I did not use the term "right adjoint" in the definition, but I know what it is, so you can use that concept in the answer.)

Question

How does one prove that the internal hom above can be extended in a unique way to a functor $[-,-]:M^{\operatorname{op}}\times M\to M$ such that $\eta:\operatorname{Hom}(-\otimes-,-)\to\operatorname{Hom}([-,-],-)$ is a natural isomorphism?

My Attempt

Let $g:b'\to b$ and $h:c\to c'$ be morphisms in $M$. We should define $[g,h]$, and then check that $[-,-]$ becomes a functor and $\eta$ becomes a natural isomorphism. The requirement that $\eta$ should be a natural transformation forces the following diagram to commute:
$\require{AMScd}$
\begin{CD}
\operatorname{Hom}([b,c]\otimes b,c) @>{\eta_{[b,c],b,c}}>> \operatorname{Hom}([b,c],[b,c])\\
@VVV @VVV\\
\operatorname{Hom}([b,c]\otimes b',c') @>{\eta_{[b,c],b',c'}}>> \operatorname{Hom}([b,c],[b',c'])
\end{CD}
So there is only one way to define $[g,h]$. Namely,
\begin{equation}
[g,h] = \eta_{[b,c],b',c'}(h\circ(\eta_{[b,c],b,c}^{-1}(1_{[b,c]}))\circ(1_{[b,c]}\otimes g))\text{.}
\end{equation}

I proved that $[1_b,1_c]=1_{[b,c]}$ for all objects $b,c$ in $M$. But I could not prove that $[g',h']\circ[g,h]=[g\circ g',h'\circ h]$. Both sides of the equation becomes too messy when spelled out.

Answer 1

Nice work so far! I think breaking down the definition of this functor into smaller pieces will be helpful.

Given a morphism $g : b' \to b$ and an object $c$, we define $[g,1_c] : [b,c] \to [b',c]$ to be $$\eta_{[b,c],b',c}(\eta_{[b,c],b,c}^{-1}(1_{[b,c]}) \circ (1_{[b,c]} \otimes g)).$$

Then we verify two conditions:

1. $[g_1 \circ g_2, 1_c] = [g_2, 1_c] \circ [g_1, 1_c]$ for all morphisms $g_1 : b' \to b$, $g_2 : b'' \to b'$, and all objects $c$.
2. $[1_{b'}, h] \circ [g,1_c] = [g, 1_{c'}] \circ [1_b, h]$ for all morphisms $g : b' \to b$ and $h : c \to c'$.

From these two facts it follows that defining $[g, h] = [g, 1_{c'}] \circ [1_b, h]$ makes $[{-},{=}]$ into a functor. This is general phenomenon: to define a functor $C_1 \times C_2 \to D$, you just need to describe the functoriality in each component and then check that they "commute" (in the sense of condition 2 above).

Unfortunately I don't have time to write a full answer right now, but I hope this helps you finish the proof -- the benefit of doing it this way is that you only have to deal with two morphisms (instead of four) at any time.

---

For condition 1, we equivalently need to verify that the following diagram commutes:

(Check that this is really equivalent!). The three morphisms in this diagram also appeared in the commutative squares witnessing the naturality of $\eta$ (the square you drew in your post). So we paste those squares around the outside as follows:

Now check that the squares & triangles marked in red commute, and use the fact that the colored arrows are isomorphisms to deduce that the inner triangle commutes.

Apologies for the poor handwriting, I hope it's still understandable!