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 bistrong monad on a monoidal category CC (e.g. a strong monad on a braided monoidal category), 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.

Morphisms

A notion of (non-strict) premonoidal functor is somewhat tricky to define. Part of the definition is clear: it should be a functor that preserves the tensor product up to specified coherent central isomorphism. However, the tricky part is whether it should also be required to preserve centrality of morphisms (or even just isomorphisms). Desiderata pulling in opposite directions include:

  1. If a premonoidal functor is not required to preserve centrality at least of isomorphisms, then premonoidal functors may not be closed under composition, since we may not be able to define central coherence isomorphisms for GFG \circ F if GG does not preserve the centrality of the coherence isomorphisms for FF.

  2. A morphism T 1T 2T_1 \to T_2 of bistrong monads on a monoidal category CC induces a functor C T 1C T 2C_{T_1} \to C_{T_2} which preserves the premonoidal structures strictly, hence clearly up to coherent central isomorphism. However, such a functor does not in general preserve centrality even of isomorphisms; a counterexample can be found in SL13, section 5.2.

It seems unlikely that these desiderata can be reconciled purely in the world of premonoidal categories as usually defined. One solution is to pass to Freyd-categories, which are essentially premonoidal categories equipped with a family of “special” central morphisms forming a cartesian monoidal category with the same tensor product. Morphisms of Freyd-categories are easy to define, and include all the morphisms C T 1C T 2C_{T_1} \to C_{T_2} if CC is cartesian (and if it isn’t, then there should be a suitable non-cartesian generalization of Freyd-categories). Other solutions that use different ways of representing a “special subfamily of central (iso)morphisms” are to consider the tensor product functor of a premonoidal category to be a not-necessarily-saturated anafunctor, or (in homotopy type theory) to allow the underlying category of a premonoidal category to be merely a precategory.

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

  • Sam Staton and Paul Blain Levy, Universal Properties of Impure Programming Languages. ACM Sigplan Notices, 2013, doi.

Last revised on February 19, 2021 at 11:28:41. See the history of this page for a list of all contributions to it.