Monoidal functor and the units

category-theorymonoidal-categoriesproof-explanation

In their book Tensor Categories Etingof, Gelaki, Nikshych and Ostrik define a monoidal functor between monoidal categories $(C,\otimes,1,\alpha,r,s)$ and $(C',\otimes', 1',\alpha',r',s')$ as the functor $F\colon C\to C'$ together with a natural isomorphism $J_{X,Y}\colon F(X)\otimes'F(Y)\to F(X\otimes Y)$ such that $F(1), 1'$ are isomorphic and the diagram

enter image description here

commutes.

Unlike other sources, they do not require a canonical isomorphism $F(1)\to 1'$ for which certain diagrams commute as a part of the data, but claim that it is possible to prove that such an isomorphism exists (provided there exists some isomorphism between them):

enter image description here

However, I find it troubling to prove that such an isomorphism exists.

Best Answer

The diagram they give defines a canonical morphism $\psi: 1'\otimes' F(1)\to F(1)\otimes' F(1)$.

Now you can use the following fact: in a monoidal category, if $A$ is isomorphic to the unit, then for any morphism $g: X\otimes A\to Y\otimes A$ there exists a unique morphism $f: X\to Y$ such that $g=f\otimes Id_A$. You can apply this with $A=F(1)$, $X=1'$, $Y=F(1)$ and $g=\psi$. The point is that you don't need to specify the isomorphism between $A$ and the unit, just its existence is enough.

Related Question