Right unitor in the monoidal category of sup-lattices In short: I am trying to find a right unitor for the monoidal category $\mathsf{SupLat}$ of sup-lattices.
1. Preliminaries
Let $L,M$ be sup-lattices.
Denote by $L^*$ the set $L$ with order $l \leq_{L^*} m \text{ iff } m \leq_L l$. One shows that $L^*$ is a sup-lattice. On the set $\operatorname{Hom}(L,M)$ of join-preserving functions $L \rightarrow M$ one defines a partial order by setting $f \leq g \text{ iff }f(l)\leq g(l) \text{ for all } l \in L$. The poset $\operatorname{Hom}(L,M)$ is a sup-lattice with $(\bigvee f_i)(l)=\bigvee (f_i(l)) \text{ for } l \in L, f \in \operatorname{Hom}(L,M)$.
Define the monoidal product of $L$ and $M$ as $L \otimes M := \operatorname{Hom}(L,M^*)^*$. How does the functor $\otimes$ behave on morphisms? Define $I:=\{0 <1\}$. Is $I$ the monoidal unit?
If so, I am trying to give a natural isomorphism $L \xrightarrow{\sim}L \otimes I$.
2. My attempt
My candidate map is
$$r_L^{-1}:L \rightarrow \operatorname{Hom}(L, \{1<0\})^* \\ l \mapsto I_{\downarrow l}$$ where $I_{\downarrow l}$ denotes the indicator function of the lower closure of $l \in L$. I was able to show that $I_{\downarrow l}$ preserves arbitrary joins. However, $r_L^{-1}$ does not seem to be join preserving:
Let $L=\{0,x,y,z,1\}$ with $x,y,z$ pairwise incomparable. Let $S=\{0,x,y\}$. Then $\big(r_L^{-1}(\bigvee S)\big)(z)= \big(r_L^{-1}(1)\big)(z)=1.$ However (with $\bigvee ^*$ the supremum in the opposite poset $\operatorname{Hom}(L, \{1<0\})^*$) : $\big(\bigvee ^* r_L^{-1}(S)\big)(z)= \big(\bigwedge r_L^{-1}(S)\big)(z)= \big(\bigwedge \{I_{\downarrow 0}, I_{\downarrow x}, I_{\downarrow y}\} \big)(z)=0$. Did I make a mistake somewhere? What are the right unitor and its inverse in the monoidal category $\mathsf {SupLat}$?
 A: You're right that the unit for $\otimes$ is $I = \{ 0 < 1 \} = \mathcal{P}(1)$, where $\mathcal{P} : \mathsf{Set} \to \mathsf{SupLat}$ is the powerset functor (indeed, this is the free suplattice functor). However, I think you're thinking about the tensor product in a way that's making your life harder than it needs to be.
The quickest way to see this is to note that $L \cong \text{Hom}(I, L)$, so that we also have (by duality)
$$
L^* \cong \text{Hom}(I, L^*) \cong \text{Hom}(L, I^*).
$$
From here, it's easy an easy computation that
$$
L \otimes I \cong \text{Hom}(L, I^*)^* \cong (L^*)^* \cong L
$$

That said, here's another way to think about the tensor product, which I think will make your life easier. It's kind of hard to find this written down somewhere, which is why I want to say a few words about it here.
There's a very tight analogy between suplattices and abelian groups, where we think of $\vee \approx +$. In fact, we can push this analogy further, where monoids in $\mathsf{SupLat}$ act like monoids in $\mathsf{Ab}$ -- that is, rings.
With this in mind, we might consider an alternative definition for the tensor product. Say that a map
$f : L_1 \times L_2 \to M$ is a bimorphism if and only if

*

*$f \left ( \bigvee x_i, y \right ) = \bigvee f(x_i, y)$

*$f \left ( x, \bigvee y_i \right ) = \bigvee f(x, y_i)$
Then the tensor product $L_1 \otimes L_2$ is the universal suplattice with a bimorphism from $L_1 \times L_2$.

As with abelian groups, we could appeal to the adjoint functor theorem to argue the "bimorphisms" functor is representable, so a tensor product exists. But it's useful to know how to build the tensor product by hand. Without going into too many details, if $\mathcal{D} : \mathsf{Posets} \to \mathsf{SupLat}$ is the downset functor, which is left adjoint to the forgetful functor $U : \mathsf{SupLat} \to \mathsf{Posets}$, then one can show
$$
L_1 \otimes L_2 = 
\frac{\mathcal{D}(UL_1 \times UL_2)}{
\bigcup \downarrow (x_i, y) = \downarrow(\bigvee x_i, y) \quad \quad
\bigcup \downarrow(x, y_i) = \downarrow(x, \bigvee y_i)}
$$
where, as usual, $\downarrow (x^*,y^*) = \{ (x,y) \mid (x,y) \leq (x^*, y^*) \}$ is a principal downset. As an exercise, do you see how this is entirely analogous to the usual construction of the tensor product of abelian groups?
Lastly, notice that $\text{Hom}(L_1 \otimes L_2, M) \cong \text{Hom}(L_1, \text{Hom}(L_2, M))$. This (coupled with duality) lets us show that our new (imo, better) definition of tensor product agrees with the definition you gave:
$$
\begin{align}
\text{Hom}(L_1 \otimes L_2, X) 
&\cong \text{Hom}(L_1, \text{Hom}(L_2, X)) \\
&\cong \text{Hom}(L_1, \text{Hom}(X^*, L_2^*)) \\
&\cong \text{Hom}(X^*, \text{Hom}(L_1, L_2^*)) \\
&\cong \text{Hom}(\text{Hom}(L_1, L_2^*)^*, X)
\end{align}
$$
the claim then follows by yoneda, since this was natural in $X$.
With this construction, you can show that $L \cong L \otimes I$ by checking that a bimorphism from $L \times I \to M$ is the same thing as a morphism out of $L$. This isn't hard, and I'll leave it as a cute exercise.
In fact, this definition makes it much easier to see what $- \otimes L$ does to morphisms.
If $f : X \to Y$, then $f \otimes L : X \otimes L \to Y \otimes L$ is defined by
$$
(f \otimes L)( \downarrow(x,l) ) = \downarrow(fx,l)
$$
it's not hard to check that this preserves the defining relations of the tensor product, so it really does define a map.

Surprisingly, examples of these kinds of computations in $\mathsf{SupLat}$ can be tricky to find. If you're interested in more, I suggest the first few chapters of Joyal and Tierney's An Extension of the Galois Theory of Grothendieck. Don't let the title scare you! Chapters $I$ and $II$ are all about the category of sup lattices and its monoidal structure, and it's surprisingly readable!

I hope this helps ^_^
