# Are all binoidal categories (in the literature) actually strict?

There is a very good description of binoidal categories on the nlab.

Briefly, a binoidal category consists of a category $C$ and, for each $A\in Ob(C)$ a pair of functors $A\rtimes -$ and $- \ltimes A$ whose action on objects agrees in the following sense: $A\ltimes B=A\rtimes B$; we write this object $A\otimes B$. Note that the $\otimes$ notation applies only to objects; the closest equivalent for morphisms has two possibilities, which may not be equal. Given $f:A\to B$ and $g:C\to D$, the composites $A\otimes C\to B\otimes D$

$$f\ltimes D \circ A \rtimes g$$ and $$B \rtimes g \circ f \ltimes C$$

need not be equal.

Question 1: is it a consequence of the above definition of binoidal categories that $$f\ltimes(A\otimes B) = (f\ltimes A)\ltimes B$$ and $$(A\otimes B)\rtimes f = A\rtimes (B\rtimes f)$$

I suspect not: any monoidal category is a binoidal category via $-\otimes\text{id}_A$ and $\text{id}_A\otimes -$, and in a non-strict monoidal category the two morphisms "equated" above might not even have the same domain and codomain. Or perhaps I have made a mistake?

If so, this means that the equation above (and the corresponding rule for $\rtimes$) must be added as an additional part of the definition of a binoidal category. I have not found this mentioned in the literature. One is then led to a "weak" version where the equation is replaced with a natural isomorphism as below

Question 2: is it a consequence of the above definition of binoidal categories that $$\left(-\ltimes(A\otimes B)\right) \simeq \left((-\ltimes B)\circ(-\ltimes A)\right)$$ and $$\left((A\otimes B)\rtimes -\right) \simeq \left((A\rtimes -)\circ(B\rtimes -)\right)$$

Finally,

Question 3: if the answer to either (1) or (2) is "no", what is the name for a binoidal category in which the equation of (1) holds, and what is the name for a binoidal category in which the equation of (2) holds?

By analogy to monoidal categories, it would seem that the answer to (3) involves the use of the adjectives "strict" and "non-strict"; this is where the title of my question comes from.

Side note: I'm not sure that any of the above is necessarily implied by the associator of a premonoidal category; in the non-strict case that is a natural isomorphism relating the "left product" with the "right product" as shown below, rather than relating one of them to itself.

$$\left((B\rtimes -)\circ(-\ltimes A)\right) \simeq \left((-\ltimes A)\circ(B\rtimes -)\right)$$

Edit 2-Apr: what was previously the sole question is now "Question 1"; I have added "Question 2" and "Question 3", which were implicit in the original posting, but which I should have made explicit. Question 3 is the real goal, but might be ill-posed or trivial based on the answers to 1+2.

-
I his work "Formal Category Theory: Adjointness for 2-Categories, Lecture Notes in Mathematics 391" J.W Gray define the notion of quasi-functor on two variables (p. 56), and this is a family of (2-) funtors that resemble a bit the binoidal category axiom. Then Gray come to define a monoidal structure on 2-Cat (different from the cartesian one) we call it $(2-CAt, \bigotimes)$, and the tensor product is a quasi-functor (on two varibles), and from tha top diagram p. 57 I seems that this can help you – Buschi Sergio Apr 2 '11 at 11:08
Are you sure that your last isomorphism is the associator? It seems to me (looking at Power and Robinson's paper) that the associator does exactly what you want. Incidentally, I don't think there's any reason why binoidal categories proper should obey your axiom in general. – Finn Lawler Apr 2 '11 at 14:32
Yes Finn, I'm sure. Look carefully at the Power+Robinson paper: they don't actually say which functors the associator establishes a natural isomorphism between -- they only give the domain and codomain of its components, and this is somewhat ambiguous because the "action on objects" notation for the left-product and right-product functors is the same. You have to work backwards to figure out the actual functors which are naturally isomorphic; these turn out to be the ones in the last display of my question. – Adam Apr 2 '11 at 17:18
@Buschi, yes, a binoidal category B looks a bit like a quasi-functor B×B→B, except it doesn't have the 2-cell $\gamma_{f,g}$ (which would be from the first math display of my question to the second)... unfortunately, leaving that out is what makes binoidal categories useful in modeling of effects. But thanks for pointing out the connection! – Adam Apr 2 '11 at 20:12

As for the question on prominent display, you've answered it yourself (in other words, no, you did not make a mistake).

However, I don't understand why such an equation "must" be added to the definition of binoidal category; I don't think it should be added at all! I am guessing that your problem is not so much with the notion of binoidal category, as it is with an alleged incompleteness of the notion of premonoidal category.

Here's how I see it. Let $\otimes$ denote the non-cartesian symmetric monoidal product on the 1-category $Cat$. A binoidal category is then a category $C$ equipped with a "magma" structure

$$m: C \otimes C \to C.$$

The definition of premonoidal category then involves a (central) natural transformation $\alpha$ between two functors shown below:

$$[(C \otimes C) \otimes C \stackrel{m \otimes 1_C}{\to} C \otimes C \stackrel{m}{\to} C] \stackrel{\alpha}{\Rightarrow} [(C \otimes C) \otimes C \stackrel{\text{assoc}}{\to} C \otimes (C \otimes C) \stackrel{1_C \otimes m}{\to} C \otimes C \stackrel{m}{\to} C]$$

Now, given $f: x \to x'$ in $C$, there is a well-formed morphism

$$(f \otimes y) \otimes z: (x \otimes y) \otimes z \to (x' \otimes y) \otimes z$$

in $(C \otimes C) \otimes C$. The associativity of the monoidal category $(Cat, \otimes)$ is a functor that takes this morphism to a morphism

$$f \otimes (y \otimes z): x \otimes (y \otimes z) \to x' \otimes (y \otimes z)$$

in $C \otimes (C \otimes C)$. It looks like the thing you are asking about has to do with the application of the natural isomorphism $\alpha$ to $(f \otimes y) \otimes z$ in the triple tensor power of $C$. The other instances contained in your query box on the nLab article would be handled similarly; they all devolve on the non-cartesian symmetric monoidal structure on $Cat$.

P.S.: Who is the mathematician displayed in your avatar/icon?

-
@Todd, the definition you give for a binoidal category -- as a property of the non-cartesian symmetric monoidal structure of Cat rather than a family of endofunctors -- is quite different from the one which is standard in the literature (dx.doi.org/10.1007/BFb0014560 or dx.doi.org/10.1017/S0956796809007308 for example). Are you saying that the one currently in use cannot be repaired without completely rephrasing? – Adam Apr 2 '11 at 18:00
@Adam: the definition I used is precisely definition 3.2 in the paper by Power and Robinson. – Todd Trimble Apr 2 '11 at 18:33
(Unfortunately, I cannot view the papers you linked to from where I am; they are behind a pay-wall.) – Todd Trimble Apr 2 '11 at 18:38
@Todd, that is the only place where that definition (in terms of the auxiliary Cat-prime) appears. The paragraph immediately following Definition 3.2 is the definition used in every other paper, since it doesn't require the (lengthy) formal definition of Cat-prime, the proof that it is a category, the proof that it is a monoidal category, and so forth -- all of the things needed to make Definition 3.2 make sense. – Adam Apr 2 '11 at 19:58
There's an analogy here to the definition of monoidal categories. I suppose that category theorists more advanced than I intuitively think of a (strict) monoidal category as a monoid internal to Cat. But the "first order" definition which doesn't refer to large categories is useful in practice for a number of reasons. It seems that binoidal categories similarly have two definitions; my question relates to the correctness/adequacy of the "first order" version of the definition – Adam Apr 2 '11 at 19:58