Equality of morphisms in star-autonomous categories

85 Views Asked by At

1.Context
Let $(C, \otimes, I, a, l,r)$ be a monoidal category. Suppose $S: C^{op} \xrightarrow{\sim} C$ is an equivalence of categories with inverse $S’$. Assume that there are bijections $\phi_{X,Y,Z}: Hom_C(X \otimes Y,SZ) \xrightarrow{\sim} Hom_C(X, S(Y \otimes Z))$ natural in $X,Y,Z$. (This makes $C$ a star-autonomous category.) Note that we do not assume that $S$ is a monoidal equivalence. For simplicity suppose that the associator $a$ is the identity and that $S$ and $S'$ are strict inverses.

2. Question
I am trying to verify that the following diagram commutes for all $A,B \in Obj(C)$:

$$\require{AMScd} \require{cancel} \def\diaguparrow#1{\smash{\raise.5em\rlap{\ \ \scriptstyle #1} \lower.6em{\cancelto{}{\Space{2em}{1.7em}{0px}}}}} \begin{CD} && S(I \otimes S'(A \otimes B))\\ & \diaguparrow{f} @VVhV \\ A\otimes S(I \otimes S'B) @>>g> A \otimes B \end{CD}$$ where $$f:=\phi_{A \otimes S(I \otimes S'B),I,A\otimes B} \Big(id_A \otimes \phi_{S(I \otimes S'B), I, S'B}^{-1}\big( id_{S(I \otimes S'B)}\big) \Big)$$ $$g:= id_A \otimes S(l_{S‘B}^{-1})$$ $$h:=S(l_{S'(A \otimes B)}^{-1}).$$

That this diagram commutes is one step of the proof that any star-autonomous category is linearly distributive.

Using the functoriality of $S$ as well as the naturality of $\phi$ and $\phi^{-1}$ I was able to show that it suffices to prove the following equality of morphisms in $C$: $$\phi_{A \otimes B, I, S'(A \otimes B)} \Big( id_A \otimes \phi^{-1}_{B,I,S'B} \big(S(l_{S'B})\big)\Big)=S(l_{S'(A\otimes B)}).$$

I unsuccesfully tried using the naturality of $\phi$ and $l$. Any hints on how to tackle this problem?