nLab
funny tensor product

Funny tensor products

Funny tensor products

Definition

For categories C,DC,D, let CDC \Rightarrow D be the category whose objects are functors from CC to DD and whose morphisms are unnatural transformations. This makes CatCat into a closed category. We can then define a tensor product by a universal property and make CatCat into a symmetric monoidal category (Cat,)(Cat,\Box); this tensor product \Box is called the funny tensor product. This constitutes one of the precisely two symmetric monoidal closed structures on CatCat; the other of course is the cartesian closed category structure on CatCat. Both the funny product and the cartesian product are semicartesian monoidal structures.

More explicitly, the category CDC \Box D can be defined as the pushout

C 0×D 0 C 0×D C×D 0 CD\array{ C_0 \times D_0 & \to & C_0 \times D \\ \downarrow &&\downarrow \\ C \times D_0 & \to & C \Box D }

where C 0,D 0C_0,D_0 are the discrete categories of objects of C,DC,D and the maps are the inclusions.

The funny tensor product can also be generalized to higher categories.

Separate functoriality

A functor F:CDEF : C \Box D \to E can be described as being a functor of 2-variables that is “separately” functorial in the CC and DD arguments, in analogy with separate continuity. That is it has an action on objects F:C 0×D 0E 0F : C_0 \times D_0 \to E_0 and for each object cCc \in C, a functorial action F(id c,):DEF(id_c,-) : D \to E and for each object dDd \in D, a functorial action F(,id d):CEF(-,id_d) : C \to E, both of which agree on objects with FF.

Contrast this to a “jointly” functorial functor of 2-arguments, also known as a bifunctor, which is equivalent to a functor from the cartesian product F:C×DEF : C \times D \to E where we have to define for any f:ccf : c \to c' and g:ddg : d \to d' a morphism F(f,g):F(c,d)F(c,d)F(f,g) : F(c,d) \to F(c',d'). With a separately functorial FF, there are two candidates for this morphism: F(f,id)F(id,g)F(f,id) \circ F(id,g) and F(id,g)F(f,id)F(id,g) \circ F(f,id) that are not in general equal.

For a simple example of a separately functorial action that is not a bifunctor, consider the identity functor on 222 \Box 2 where 22 is the walking arrow category. If we label one copy of 22 as \top \to \bot and the other as lrl \to r then 222 \Box 2 is a non-commuting square:

(,l) (,r) (,l) (,r)\array{ (\top,l) & \to & (\top,r) \\ \downarrow &&\downarrow \\ (\bot,l) & \to & (\bot,r) }

then viewing the identity as a functor of 2-arguments, we get an obvious separately functorial action, but since the square does not commute, it is not a bifunctor.

  • Gray tensor product
  • Separately functorial functors arise naturally when studying effectful languages where the two sequencings of F(f,id)F(f,id) and F(id,g)F(id,g) correspond to the choices of order of evaluation of the two functions. See premonoidal category.

References

Last revised on June 16, 2019 at 02:06:10. See the history of this page for a list of all contributions to it.