In mathematics, especially in category theory, a closed monoidal category (or a monoidal closed category) is a category that is both a monoidal category and a closed category in such a way that the structures are compatible.
A classic example is the category of sets, Set, where the monoidal product of sets
A
B
A x B
BA
A
B
K
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 symmetric. 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.
l{C}
B
B
A\mapstoA ⊗ B
A\mapsto(B ⇒ A).
Homl{C}(A ⊗ B,C)\congHoml{C}(A,B ⇒ C)
- ⊗ B:l{C}\tol{C}
[B,-]:l{C}\tol{C}
Equivalently, a closed monoidal category
l{C}
A ⇒ B
evalA,B:(A ⇒ B) ⊗ A\toB
f:X ⊗ A\toB
h:X\toA ⇒ B
f=evalA,B\circ(h ⊗ idA).
It can be shown that this construction defines a functor
⇒ :l{C}op x l{C}\tol{C}
A ⇒ B
A
B
l{C}
BA
Strictly speaking, we have defined a right closed monoidal category, since we required that right tensoring with any object
A
A
B\mapstoA ⊗ B
B\mapsto(B\LeftarrowA)
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 ⊗ B
B ⊗ A
We have described closed monoidal categories as monoidal categories with an extra property. One can equivalently define 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.
BA
A ⇒ B
A
B
M ⇒ N
\operatorname{Hom}R(M,N)
K
A ⇒ B
A* ⊗ B
\Z
\operatorname{Hom}(R,S)\cong\operatorname{Hom}(\Z ⊗ R,S)\cong\operatorname{Hom}(\Z,R ⇒ S)\cong\{\bullet\}