Proof that $\bf M$-$\bf Set$ is a cartesian closed category

86 Views Asked by At

Let $\mathbf {M\text{-} Set}$ be the category of the sets equipped with a right action of a monoid $M$; fixed an $M$-$\mathrm {Set}$ (call it $X$), I want to prove that the functor $-\times X: \mathbf {M\text{-} Set}\to\mathbf {M\text{-} Set}$ is a left adjoint to $-^X$ (so I also have to prove that the last functor is defined $\mathbf {M\text{-} Set}\to\mathbf {M\text{-} Set}$).

Using the adjunction $F\dashv U:\mathbf {M\text{-} Set}\to\bf Set$, where $U$ is the forgetful functor, for any $Y$ in $\mathbf {M\text{-} Set}$ I have that $$U(Y^X)\cong \mathbf{Set}(*,U(Y^X))\cong \mathbf {M\text{-} Set}(M,Y^X),$$ because $F(*)$ is $M$. In this way I described the underlying set of $Y^X$; easily, it becomes an $M$-$\mathrm {Set}$ with the action that sends the morphism $f:M\to Y^X$ to the morphism $m\cdot f$ such that $(m\cdot f) (1_M)=f(m)$. At this point I can prove the adjunction showing that the counit is the evaluation and it has the universal property needed (in class we did the same thing to prove that $-\times S$ is a left adjoint to $-^S$ in $\bf Set$). Is my reasoning correct? I'm confused because the teacher mentioned (during the proof) that $\mathbf {M\text{-} Set}(M,Y^X)$ is in natural bijecton with $\mathbf {M\text{-} Set}(M\times X,Y)$, but this should be a consequence of our thesis. I quite can't tell if he was just mentioning it, or if this bijection must be used in the proof (as a necessary condition for the thesis to be true), because he left the rest as exercise.