Being (co)cartesian as a property (rather than structure) of a plain monoidal category

Question

It's well-known that being cocartesian is a property of a symmetric monoidal category: $(\mathcal C,I,\otimes,\sigma)$ is cocartesian if and only if the following conditions are satisfied:

1. Every object $C \in \mathcal C$ has a commutative monoid structure $I \xrightarrow {u_C} C \overset{m_C}{\leftarrow} C \otimes C$;

2. With respect to the commutative monoid structures of (1), every morphism is a homomorphism (in other words, $u: const_I \Rightarrow 1_{\mathcal C}: \mathcal C \rightrightarrows \mathcal C$ and $m: \otimes \circ \Delta \Rightarrow 1_{\mathcal C}: \mathcal C \rightrightarrows \mathcal C$ are natural transformations -- here $\Delta: \mathcal C \to \mathcal C \times \mathcal C$ is the diagonal functor);

3. The commutative monoid structures of (1) satisfy $u_{C \otimes D} = u_C \otimes u_D$ and $m_{C \otimes D} = m_C \otimes m_D \circ (1_C \otimes \sigma_{D,C} \otimes 1_D)$ (in other words, $u$ and $m$ are monoidal natural transformations, where $\otimes$ has been made into a monoidal functor in the canonical way using the symmetry $\sigma$).

More precisely, if the data of (1,2,3) exists, then it is essentially unique, and exhibits $(\mathcal C, I, \otimes, \sigma)$ as cocartesian in the sense that $I$ is initial, and the maps $C \xrightarrow{1_C \otimes u_D} C \otimes D \overset{u_C \otimes 1_D}{\leftarrow} D$ are coproduct coprojections.

---

But what if $(\mathcal C, I,\otimes)$ is monoidal but not known to be symmetric monoidal?

Questions:

1. Is the forgetful 2-functor from cocartesian monoidal categories to monoidal categories fully faithful?

I believe the answer to (1) is yes, as I'll sketch below. If this is correct, then "being cocartesian" is a property of a monoidal category. We can then ask:

2. What is this property, explicitly?

---

Partial progress:

One might guess that the following conditions suffice:

1. Every object $C \in \mathcal C$ is a monoid object $(C,u_C,m_C)$.

2. Every morphism is a morphism of monoid objects.

Under these conditions, I can show that

• The unit $I$ is the initial object;

• There is a functorial construction of a morphism $C \otimes D \xrightarrow{m_E\circ(f\otimes g)} E$ from morphisms $f: C \to E, g: D \to E$, which restricts appropriately along the "candidate coproduct inclusions" $C \xrightarrow{1_C \otimes u_D} C \otimes D \overset{u_C \otimes 1_D}{\leftarrow} D$;

• (If $\mathcal C$ has split idempotents) binary coproducts $C \amalg D$ exist, and are functorially split subobjects of $C \otimes D$, splitting the idempotent $m_{C \otimes D} \circ (1_C\otimes u_D \otimes u_C \otimes 1_D)$.

So I can show that $\mathcal C$ is cocartesian iff (1,2) hold and in addition the following condition is satisfied:

3. For all $C,D \in \mathcal C$, $m_{C \otimes D} \circ(1_C \otimes u_D \otimes u_C \otimes 1_D) = 1_{C\otimes D}$

But I'm not quite sure how to motivate (3), nor am I sure whether it is superfluous.

Answer 1

I don't have a counterexample to show that (3) is not superfluous, but I can provide some motivation for it. First, let us recall what is probably the most well known characterisation of cartesian monoidal categories in this spirit.

Proposition A. A symmetric monoidal category $(\mathcal M, \otimes, I)$ is cartesian if and only if there exist monoidal natural transformations $\varepsilon : ({-}) \Rightarrow I$ and $\delta : ({-}) \Rightarrow ({-}) \otimes ({-})$ equipping each object with the structure of a counital comagma.

This, for instance, is the version of the characterisation that is currently mentioned on the nLab page for semicartesian monoidal categories. In particular, note that cocommutativity and coassociativity are redundant.

If we permit ourselves to indulge in some centipede mathematics, we are led to wonder whether there are any other redundant assumptions in the proposition above. If we carry out the usual proof, we notice a few things.

1. Associativity of $\otimes$ is never used. Thus, it suffices to take $\mathcal M$ to be a unital magmal category.
2. In proving terminality of $I$, we only need that $\varepsilon$ satisfies the unit part of the monoidal natural transformation laws. Thus, it suffices to take $\varepsilon$ to be a unital natural transformation.
3. In proving that $\otimes$ is the cartesian product, we only need that $\delta$ satisfies the multiplication part of the monoidal natural transformation laws. Thus, it suffices to take $\delta$ to be a magmal natural transformation.

Unfortunately, this seems as far as we can go. In particular, we need a symmetry $\sigma$ in order that $({-}) \otimes ({-})$ be a monoidal functor, which is necessary to ask that $\delta$ is a magmal natural transformation. However, if we examine the proof further, we see that magmality of $\delta$ is used in exactly one place: to establish commutativity of the following diagram (the magmality condition is precisely the commutativity of the left-hand triangle). However, the top composite in the diagram above admits a simpler description that does not involve the symmetry. Thus, rather than require symmetry of $({-}) \otimes ({-})$ and magmality of $\delta$, it suffices to ask for the outer triangle above (which I shall call $(*)$) to commute. This eliminates the dependency on the symmetry, allowing for the original proposition to be simplified further.

Proposition A'. A unital magmal category $(\mathcal M, \otimes, I)$ is cartesian if and only if there exists a unital natural transformation $\varepsilon : ({-}) \Rightarrow I$ and a natural transformation $\delta : ({-}) \Rightarrow ({-}) \otimes ({-})$ equipping each object with the structure of a counital comagma, such that $(*)$ commutes for all $A, B \in \mathcal M$.

What does this tell us? In addition to requiring each object to be a counital comagma, and each morphism to be a homomorphism (this is naturality of $\varepsilon$ and $\delta$), we require two compatibility conditions: a compatibility condition of $\varepsilon$ with the unit $I$, and a compatibility condition of $\delta$ with the tensor $\otimes$. These are both natural conditions. However, when we drop symmetry, the compatibility condition for $\delta$ is no longer directly expressible. This necessitates its rewriting into the form $(*)$. Therefore, $(*)$ is essentially the compatibility condition between $\delta$ and $\otimes$. Of course, $(*)$ is precisely your condition (3). In fact, it is also possible to drop the unitality condition on $\varepsilon$, as this may be derived from naturality.

(Incidentally, Proposition A' appears to be more general than any other characterisation I can find in the literature. This extra generality does seem to actually be useful, too: for instance, it facilitates a direct proof that a monoidal category whose tensor product has a right adjoint is cocartesian, without using Day convolution or the Eckmann–Hilton argument.)

---

Update: I have since found almost exactly the same characterisation in Melliès's Categorical Semantics of Linear Logic (Proposition 16 and the following remark). However, he doesn't observe that unitality of $\varepsilon$ may be derived, and associativity of the tensor product is never used.