In category theory, monoidal functors are functors between monoidal categories which preserve the monoidal structure. More specifically, a monoidal functor between two monoidal categories consists of a functor between the categories, along with two coherence mapsâÂÂa natural transformation and a morphism that preserve monoidal multiplication and unit, respectively. Mathematicians require these coherence maps to satisfy additional properties depending on how strictly they want to preserve the monoidal structure; each of these properties gives rise to a slightly different definition of monoidal functors
Although we distinguish between these different definitions here, authors may call any one of these simply monoidal functors.
Let and be monoidal categories. A lax monoidal functor from to (which may also just be called a monoidal functor) consists of a functor together with a natural transformation
between functors and a morphism
called the coherence maps or structure morphisms, which are such that for every three objects , and of the diagrams
commute in the category . Above, the various natural transformations denoted using are parts of the monoidal structure on and .
If and are closed monoidal categories with internal hom-functors (we drop the subscripts for readability), there is an alternative formulation
of ÃÂ<sub>AB</sub> commonly used in functional programming. The relation between ÃÂ<sub>AB</sub> and ÃÂ<sub>AB</sub> is illustrated in the following commutative diagrams:
Suppose that a functor is left adjoint to a monoidal . Then has a comonoidal structure induced by , defined by
and
If the induced structure on is strong, then the unit and counit of the adjunction are monoidal natural transformations, and the adjunction is said to be a monoidal adjunction; conversely, the left adjoint of a monoidal adjunction is always a strong monoidal functor.
Similarly, a right adjoint to a comonoidal functor is monoidal, and the right adjoint of a comonoidal adjunction is a strong monoidal functor.