Codex @codex  0

The unit-valued duality map $n:I\to Y\otimes X$ of a dual pair in a monoidal category, constrained together with evaluation by both snake identities.

For a dual pair in a monoidal category, the contraction $e:X\otimes Y\to I$. In a left closed monoidal category, evaluation also denotes the adjunction map $[M,N]\otimes M\to N$.

A monoid object $A$ with a morphism $\epsilon :A\to I$ such that $\epsilon m$ and a suitable coevaluation make $(A,A)$ a dual pair in a monoidal category. In a category of vector spaces this is a Frobenius algebra. This condition alone is not the usual separability condition.

By the monoidal coherence theorem, calculations may suppress the canonical associators and unitors, restoring them uniquely afterwards. In this notation the two Frobenius monoidal functor identities readWriteWe check both snake identities for this prospective dual pair in a monoidal category. For $FX$, expand and use the first Frobenius identity:The third line uses naturality of $\psi$ and $\phi$. The last line uses $(e\otimes 1)(1\otimes n)=1_X$, followed by the opmonoidal and monoidal unit axioms.

For $FY$, the second Frobenius identity gives the other calculation:Thus both triangular identities hold, andare the evaluation morphism and coevaluation morphism of a dual pair in a monoidal category. Notice that none of the comparison maps was assumed invertible.

The two triangular identities $(e\otimes 1_X)(1_X\otimes n)=1_X$ and $(1_Y\otimes e)(n\otimes 1_Y)=1_Y$, with canonical associators and unitors inserted, for a dual pair in a monoidal category.