nLab
premonoidal category

Premonoidal categories

Context

Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

Premonoidal categories

Idea

A premonoidal category is a generalisation of a monoidal category, applied by John Power and his collaborators to denotational semantics in computer science. There, the Kleisli category of a strong monad provides a model of call-by-value? programming languages. In general, if the original category is monoidal, the Kleisli category will only be premonoidal.

Recall that a bifunctor from CC and DD to EE (for C,D,EC,D,E categories) is simply a functor to EE from the product category C×DC \times D. We can think of this as an operation which is ‘jointly functorial’. But just as a function to XX from YY and ZZ (for X,Y,ZX,Y,Z topological spaces) may be continuous in each variable yet not jointly continuous? (continuous from the Tychonoff product Y×ZY \times Z), so an operation between categories can be functorial in each variable separately yet not jointly functorial.

Recall that a monoidal category is a category CC equipped with a bifunctor C×CCC \times C \to C (equipped with extra structure such as the associator). Similarly, a premonoidal category is a category equipped with an operation C×CCC \times C \to C, which is (at least) a function on objects as shown, but one which is functorial only in each variable separately.

Definition

A binoidal category is a category CC equipped with

  • for each pair x,yx,y of objects of CC, an object xyx \otimes y;
  • for each object xx a functor xx \rtimes - whose action on objects sends yy to xyx \otimes y
  • for each object xx a functor x- \ltimes x whose action on objects sends yy to yxy \otimes x

A morphism f:xyf\colon x \to y in a binoidal category is central if, for every morphism f:xyf'\colon x' \to y', the diagrams

xx xf xy fx fy yx yf yy \array { x \otimes x' & \overset{x \rtimes f'}\to & x \otimes y' \\ \mathllap{f \ltimes x'}\downarrow & & \downarrow\mathrlap{f \ltimes y'} \\ y \otimes x' & \underset{y \rtimes f'}\to & y \otimes y' \\ }

and

xx xf xy fx fy yx yf yy \array { x' \otimes x & \overset{x' \rtimes f}\to & x' \otimes y \\ \mathllap{f' \ltimes x}\downarrow & & \downarrow\mathrlap{f' \ltimes y} \\ y' \otimes x & \underset{y' \rtimes f}\to & y' \otimes y \\ }

commute. In this case, we denote the common composites ff:xxyyf \otimes f'\colon x \otimes x' \to y \otimes y' and ff:xxyyf' \otimes f\colon x' \otimes x \to y' \otimes y.

A premonoidal category is a binoidal category equipped with:

  • an object II;
  • for each triple x,y,zx,y,z of objects, a central isomorphism α x,y,z:(xy)zx(yz)\alpha_{x,y,z}\colon (x \otimes y) \otimes z \to x \otimes (y \otimes z); and
  • for each object xx, central isomorphisms λ x:xIx\lambda_x\colon x \otimes I \to x and ρ x:Ixx\rho_x\colon I \otimes x \to x;

such that the following conditions hold.

  • all possible naturality squares for α\alpha, λ\lambda, and ρ\rho (which make sense since we have central morphisms) commute. Note that when written out explicitly in terms of the functors xx\rtimes - and x-\ltimes x, we need three different naturality squares for α\alpha. (But it is possible to rephrase α\alpha as a single natural transformation using the slick version below.)
  • the pentagon law holds for α\alpha, as in a monoidal category.
  • the triangle law holds for α\alpha, λ\lambda, and ρ\rho, as in a monoidal category.

A strict premonoidal category is a premonoidal category in which (xy)z=x(yz)(x \otimes y) \otimes z = x \otimes (y \otimes z), xI=xx \otimes I = x, and Ix=xI \otimes x = x, and in which α x,y,z\alpha_{x,y,z}, λ x\lambda_x, and ρ x\rho_x are all identity morphisms. (We need the underlying category CC to be a strict category for this to make sense.)

Similarly, a symmetric premonoidal category is a premonoidal category equipped with a central natural isomorphism xyyxx\otimes y \cong y\otimes x (as for α\alpha, there are two naturality squares unless we use the slick approach), satisfying the usual axioms of a symmetry.

Slick version

As a strict monoidal category is a monoid in the cartesian monoidal category Cat, so a strict premonoidal category is a monoid in the symmetric monoidal category (Cat,)(Cat,\Box), where \Box is the funny tensor product.

From this point of view, a binoidal category is just a category CC with a functor CCCC \Box C \to C

It may be possible to make (Cat,)(Cat,\Box) a symmetric monoidal 2-category, in which a pseudomonoid object is precisely a non-strict premonoidal category, but if so, nobody seems to have written this up yet. It is possible, however, to describe part of the structure of a non-strict premonoidal category in terms of (Cat,)(Cat,\Box). For instance, a binoidal structure on CC is precisely a functor CCCC\Box C \to C, and the naturality of the associator α\alpha can be expressed by saying that it is a natural transformation (with central components) between functors CCCCC\Box C\Box C \to C.

Examples

  • Every monoidal category is a premonoidal category.

  • If TT is a strong monad on a monoidal category CC, then the Kleisli category C TC_T of TT inherits a premonoidal structure, such that the functor CC TC\to C_T is a strict premonoidal functor. This premonoidal structure is only a monoidal structure if TT is a commutative monad.

  • A strict premonoidal category is the same as a sesquicategory with one object, so any object of a sesquicategory has a corresponding premonoidal category whose objects are endomorphisms and arrows are 2-cells.

Properties

The central morphisms of a premonoidal category CC form a subcategory Z(C)Z(C), called the centre of CC, which is a monoidal category. This defines a right adjoint functor to the inclusion MonCatPreMonCatMonCat \hookrightarrow PreMonCat using the definition of functor of premonoidal categories in Power-Robinson 97.

In the same way that a (strict) monoidal category can be identified with a (strict) 2-category with one object, a strict premonoidal category can be identified with a sesquicategory with one object. In fact, a sesquicategory is precisely a category enriched over the monoidal category (Cat,)(Cat,\otimes) described above.

References

  • John Power and Edmund Robinson, Premonoidal categories and notions of computation, Math. Structures Comput. Sci., 7(5):453–468, 1997. Logic, domains, and programming languages (Darmstadt, 1995).

    PostScript

  • Alan Jeffrey, Premonoidal categories and a graphical view of programs, pdf file

Last revised on June 22, 2019 at 16:21:24. See the history of this page for a list of all contributions to it.