In mathematics, especially in , a closed monoidal category (or a monoidal closed category) is a that is both a and a in such a way that the structures are compatible.
A classic example is the , Set, where the monoidal product of sets and is the usual cartesian product , and the internal Hom is the set of functions from to . A non- example is the , K-Vect, over a field . Here the monoidal product is the usual tensor product of vector spaces, and the internal Hom is the vector space of linear maps from one vector space to another.
The internal language of closed symmetric monoidal categories is linear logic and the type system is the linear type system. Many examples of closed monoidal categories are . However, this need not always be the case, as non-symmetric monoidal categories can be encountered in category-theoretic formulations of linguistics; roughly speaking, this is because word-order in natural language matters.
A closed monoidal category is a such that for every object the functor given by right tensoring with
has a right adjoint, written
This means that there exists a bijection, called 'currying', between the Hom-sets
that is natural in both A and C. In a different, but common notation, one would say that the functor
has a right adjoint
Equivalently, a closed monoidal category is a category equipped, for every two objects A and B, with
an object ,
a morphism ,
satisfying the following universal property: for every morphism
there exists a unique morphism
such that
It can be shown that this construction defines a functor . This functor is called the internal Hom functor, and the object is called the internal Hom of and . Many other notations are in common use for the internal Hom. When the tensor product on is the cartesian product, the usual notation is and this object is called the exponential object.
Strictly speaking, we have defined a right closed monoidal category, since we required that right tensoring with any object has a right adjoint.