Diagram 4.3.3.2, I, in "Catégories Tannakiennes" by S. Rivano

Question

$\require{AMScd}\DeclareMathOperator\Hom{Hom}$In Catégories Tannakiennes by N. Saavedra, chapter I, diagram 4.3.3.2, he claims (as far as I can tell) that the following diagram commutes: $$\begin{CD} F(X^{\vee} \otimes Y) @>>> F(\underline{\Hom}(X,Y))\\ @AcAA @VF_{X,Y}VV\\ F(X^{\vee}) \otimes F(Y)\\ @VF_{X,\mathbf{1}} \otimes \mathrm{id}VV @VVV\\ F(X)^{\vee} \otimes F(Y) @>>> \underline{\Hom}(FX,FY) \end{CD}$$ Here, we assume that $F$ is a tensor functor between rigid tensor categories, where $F_{X,Y}$ is the induced map coming from $F(\text{ev})$ (suppressing the natural isomorphism $c$ coming from $F$ as a tensor functor) under the natural isomorphism $\Hom(F(\underline{\Hom}(X,Y)) \otimes F(X),F(Y)) \simeq \Hom(F(\underline{\Hom}(X,Y)),\underline{\Hom}(FX,FY))$, and $F_{X,\mathbf{1}}$ has the obvious interpretation from this.

As far as I can see (I don't know much French), N. Saavedra gives no explanation for the commutativity of this diagram. He later (5.2.2, I) shows that $F_{X,\mathbf{1}}$ is an isomorphism, and since all the other maps in the diagram above are isomorphisms, it then easily follows from the commutativity of the above diagram that $F_{X,Y}$ is an isomorphism.

Unless I am mistaken, the horizontal maps are the isomorphisms in $\mathcal{C},\mathcal{C}'$ (source and target of the functor $F$), coming from the isomorphism $X^{\vee} \otimes Y \cong \underline{\Hom}(X,Y)$.

So my question is basically how to see that this diagram commutes (my end goal is really to understand why $F_{X,Y}$ is an isomorphism).

Comment: note that in the above diagram, there is only one arrow $F_{X,Y}$ on the right, I just don't know how to write it as one arrow in AMScd.

I asked a similar question (not precisely the same) at MSE a while ago (Tensor functors on rigid categories.), but I had some trouble understanding the explanation given there (for example, I don't really know what an adjunction-diagram is).

Any clarification would be most helpful.

Edit: As per D. Rydhs comment, the horizontal maps are not neccessarily isomorphisms, since we are not assuming that we are in a rigid category. Furthermore, as D. Rydh points out, S. Rivano claims this follows as a special case of diagram 4.3.3.1 in S. Rivano (take $(X_1,Y_1) = (X,\mathbf{1})$ and $(X_2,Y_2) = (\mathbf{1},Y)$).

Answer 1

Here is a direct argument for showing that $F_{X,Y}$ is an isomorphism. One can argue that $F[X, Y]$ and $[FX, FY]$ are both representing objects for the functor $\mathcal{C}'(- \otimes FX, FY)$, and furthermore the universal element for $F[X, Y]$ is the map $F(\mathrm{ev}_{X,Y}) : F[X,Y] \otimes FX \to FY$.

By the general theory of representable functors, if $(A, a : \mathcal{D}(-, A) \cong G)$ and $(B, b : \mathcal{D}(-, B) \cong G)$ are representations of the same presheaf $G$, then by the full faithfulness of the Yoneda embedding there is a unique isomorphism $i : A \cong B$ such that $\mathcal{D}(-, i) = b^{-1} \circ a$. Explicitly, the forwards map $i : A \to B$ is given by $b^{-1}(a(\mathrm{id}_A))$, where $a(\mathrm{id}_A)$ is the universal element for $A$.

Returning to our rigid categories, we find that the natural isomorphism $$b : \mathcal{C}'(-, [FX,FY]) \cong \mathcal{C}'(- \otimes FX, FY)$$ is just the tensor-hom adjunction isomorphism, and thus the isomorphism $i : F[X,Y] \to [FX,FY]$ is given by the adjoint of the map $F(\mathrm{ev}_{X,Y})$, which is exactly $F_{X,Y}$.

---

EDIT: maybe this answer won't satisfy you because we still have to show that $F(\mathrm{ev}_{X,Y})$ works as a universal element. This still probably involves an annoying diagram.