Closed monoidal category

In mathematics, especially in category theory, a closed monoidal category is a context where we can take tensor products of objects and also form 'mapping objects'. A classic example is the category of sets, Set, where the tensor product of sets A and B is the usual cartesian product $A \times B$, and the mapping object B^A is the set of functions from A to B. Another example is the category FdVect, consisting of finite-dimensional vector spaces and linear maps. Here the tensor product is the usual tensor product of vector spaces, and the mapping object is the vector space of linear maps from one vector space to another.

Technically, what we have been calling a 'mapping object' is called the 'internal Hom'.

Definition

A closed monoidal category is a monoidal category C such that for every object A the functor given by left tensoring with A

$B\mapsto A\otimes B$

has a right adjoint, written

$B\mapsto (A \Rightarrow B).$

This means that there exists a bijection between the Hom-sets

$\mathbf{C}(A\otimes B, C)\cong\mathbf{C}(B,A\Rightarrow C)$

that is natural in both B and C.

Equivalently, a closed monoidal category C is a category equipped, for every two objects A and B, with

• an object $A\Rightarrow B$,
• a morphism $\mathrm{eval}_{A,B} : A\otimes (A\Rightarrow B)\to B$,

satisfying the following universal property: for every morphism

$f : A\otimes X\to B$

there exists a unique morphism

$h : X \to A\Rightarrow B$

such that

$f = \mathrm{eval}_{A,B}\circ(\mathrm{id}_A\otimes h).$

It can be shown that this construction defines a functor $\Rightarrow : C^{op} \otimes C \to C$. This functor is called the internal Hom functor, and the object $A \Rightarrow B$ is called the internal Hom of A and B. Many other notations are in common use for the internal Hom. When the tensor product on C is the cartesian product, the usual notation is B^A.

Strictly speaking, we have defined a left closed monoidal category, since we required that left tensoring with any object A has a right adjoint. In a right closed monoidal category, we instead demand that the functor of right tensoring with any object A

$B\mapsto B\otimes A$

have a right adjoint

$B\mapsto(B\Leftarrow A)$

(Beware: almost all authors use the opposite terminology.)

A biclosed monoidal category is a monoidal category that is both left and right closed.

A symmetric monoidal category is left closed if and only if it is right closed. Thus we may safely speak of a 'symmetric monoidal closed category' without specifying whether it is left or right closed. In fact, the same is true more generally for braided monoidal categories: since the braiding makes $A \otimes B$ naturally isomorphic to $B \otimes A$, the distinction between tensoring on the left and tensoring on the right becomes immaterial, so every right closed braided monoidal category becomes left closed in a canonical way, and vice versa.

We have described closed monoidal categories as monoidal categories with an extra property. One can equivalently defined a closed monoidal category to be a closed category with an extra property. Namely, we can demand the existence of a tensor product that is left adjoint to the internal Hom functor. In this approach, closed monoidal categories are also called monoidal closed categories.

Examples

• The monoidal category Set of sets and functions, with cartesian product as the tensor product, is a closed monoidal category. Here $A \Rightarrow B$ is the set of functions from A to B. This example is a cartesian closed category.
• More generally, every cartesian closed category is a symmetric monoidal closed category, when the monoidal structure is the cartesian product structure. Here the internal hom $A \Rightarrow B$ is usually written B^A.
• The monoidal category FdVect of finite-dimensional vector spaces and linear maps, with its usual tensor product, is a closed monoidal category. Here $A \Rightarrow B$ is the vector space of linear maps from A to B. This example is a compact closed category.
• More generally, every compact closed category is a symmetric monoidal closed category, in which the internal Hom functor $A\Rightarrow B$ is given by $B\otimes A^*$.

References

• Kelly,G.M. "Basic Concepts of Enriched Category Theory", London Mathematical Society Lecture Note Series No.64 (C.U.P., 1982)
• Paul-André Melliès, Categorical Semantics of Linear Logic, 2007