nLab
premonoidal category

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.

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 monoidal 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 premonoidal category is a monoid in another symmetric monoidal category whose underlying category is also CatCat.

Given categories C,DC,D and functors F,G:CDF,G\colon C \to D, a (not necessarily natural) transformation from FF to GG consists of, for each object xx of CC, a morphism from F(x)F(x) to G(x)G(x) in DD. (So a natural transformation is a transformation that satisfies an extra property.) We can compose transformations using vertical composition (but not horizontal composition).

Given categories C,DC,D, let CDC \Rightarrow D be the category whose objects are functors from CC to DD and whose morphisms are transformations between these functors. This makes CatCat into a closed category. We can then define a tensor product by a universal property and make CatCat into a monoidal category (Cat,)(Cat,\otimes) which is in fact symmetric.

Then a strict premonoidal category is precisely a monoid object in (Cat,)(Cat,\otimes).

It may be possible to weaken the above make (Cat,)(Cat,\otimes) a symmetric monoidal 2-category, in which a monoid object is precisely a 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,\otimes). For instance, a binoidal structure on CC is precisely a functor CCCC\otimes 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\otimes C\otimes 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.

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 may define an adjoint functor to the inclusion MonCatPreMonCatMonCat \hookrightarrow PreMonCat (I haven't actually checked this).

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

Revised on May 8, 2014 23:28:49 by Tim Porter (2.27.158.77)