Explicit left adjoint to forgetful functor from Cartesian to symmetric monoidal categories

Question

There is a forgetful functor from the category of (small) Cartesian monoidal categories (a symmetric monoidal category in which the tensor product is given by the categorical product) to the category of symmetric monoidal categories. This functor is known to have a left adjoint and right adjoint. The right adjoint is easy to describe: it takes a symmetric monoidal category to its category of cocommutative coalgebras. I am looking for an explicit description of the left adjoint though. Does anyone know what it is?

There is a MO question about this, but it does not give an explicit description: Cartesian envelope of a symmetric monoidal category

I am also interested in the left adjoint of the forgetful functor with domain semi-Cartesian monoidal categories, which are symmetric monoidal categories in which the tensor unit is terminal.

Another way to look at this is from the point of view of the "commutative algebra of categories," as described (in the quasicategorical case) here: https://arxiv.org/abs/1606.05606. Using that machinery, i.e. knowing that Cartesian monoidal categories are precisely the symmetric monoidal categories which are modules over the solid semi-ring category $Fin^{op}$, it would suffice to have an explicit description of the tensor product on (presentable) symmetric monoidal categories (that recovers the structure described in the above reference). So maybe this is known?

Answer 1

I don't know the answer, although I've thought about this quite a bit. I think the best that can be said in general is that the free cartesian monoidal category on $\mathcal{C}^\otimes$ is a full subcategory of $\text{Fun}^\otimes(\mathcal{C}^\otimes,\text{Set}^\times)^\text{op}$, which is the category of symmetric monoidal functors. That is Theorem 3.10 of https://arxiv.org/abs/1606.05606.

There is some hope of giving a more explicit description if we know something about maps into tensor products. Here are three examples. (I would love to understand what they have in common.)

Baby example: If $\mathcal{C}^\times$ is already cartesian monoidal, then $\mathcal{C}_{/Y\times Z}\cong\mathcal{C}_{/X}\times_\mathcal{C}\mathcal{C}_{/Y}$. That is, a map $X\rightarrow Y\times Z$ corresponds to two maps $X\rightarrow Y$ and $X\rightarrow Z$. In this case, the free cartesian monoidal category on $\mathcal{C}$ is $\mathcal{C}$ itself.

Example 2: If $\mathcal{C}^\amalg$ is cocartesian monoidal, we may ask whether the coproduct behaves like a disjoint union (that is, $\mathcal{C}$ is disjunctive) in the following sense: any map $X\rightarrow Y\amalg Z$ decomposes canonically as the coproduct of two maps $X_Y\rightarrow Y$ and $X_Z\rightarrow Z$. That is, $\mathcal{C}_{/Y\amalg Z}\cong\mathcal{C}_{/Y}\times\mathcal{C}_{/Z}$. In this case, I believe that the free cartesian monoidal category can be described as a category of spans, something like the following:

Objects are just objects of $\mathcal{C}$. Morphisms from $X$ to $Y$ are spans $X\leftarrow T\rightarrow Y$, such that $T$ admits a decomposition $T_1\amalg\cdots\amalg T_n$ with each $T_i\rightarrow X$ an inclusion of a direct summand; that is, $T_i\amalg T_i^\prime\cong X$.

For example, when $\mathcal{C}=\text{Fin}$, the category of finite sets, the free cartesian monoidal category is spans of finite sets. The $\mathcal{C}=\text{Fin}$ case is a main result of the paper cited above (at the level of $\infty$-categories). The general case is not written down anywhere, as far as I know.

Example 3: Given an operad $\mathcal{O}$, there is a category $[\mathcal{O}^\otimes]$, whose objects are finite sets. A map from $S$ to $T$ is a function $f:S\rightarrow T$ and an $|f^{-1}(t)|$-ary operation for each $t\in T$. Concatenation gives $[\mathcal{O}^\otimes]$ a symmetric monoidal structure.

Note that $[\mathcal{O}^\otimes]$ is disjunctive (in the sense of Example 2) but not cocartesian monoidal. In this case, the free cartesian monoidal category is the full subcategory of $$\text{Fun}^\otimes([\mathcal{O}^\otimes],\text{Set}^\times)^\text{op}=\text{Alg}_\mathcal{O}(\text{Set})^\text{op}$$ spanned by the free $\mathcal{O}$-algebras. Classically, the free $\mathcal{O}$-algebra on $n$ generators is $$\coprod_{k\geq 0}\mathcal{O}(k)\times_{\Sigma_k}n^k.$$ That effectively computes the free cartesian monoidal category on $[\mathcal{O}^\otimes]$ as a type of span construction, similar to Example 2. See the paper above, Remark 5.1 (also Example 3.16). The span construction can be made precise without much difficulty for ordinary categories, but it is an open problem for $\infty$-categories.

Answer 2

Here I conjecture an answer to the question above.

I describe a tensor product of symmetric monoidal categories, which I claim makes the 2-category $\mathrm{SMC}$ into a symmetric monoidal 2-category. I call this $\boxtimes$.

I claim that the free cartesian closed category on a symmetric monoidal category $C$ is

$$F \boxtimes C$$

where $F$ is the free cartesian category on one object, namely the opposite of $(\mathrm{FinSet}, +)$. So, I'm claiming that the left pseudoadjoint of the forgetful 2-functor

$$ U : \mathrm{Cart} \to \mathrm{SMC} $$

is the 2-functor $F \boxtimes -$.

Part of the point is that tensoring $C$ with $F$ shouldn't change the objects of $C$: it should just add extra morphisms and equations between morphisms. It should give each object $x \in C$ a morphism $x \to x \otimes x$ and a morphism $x \to I$ which make $x$ into a cocommutative comonoid, and these morphisms should be natural, making a bunch of squares commute. By Fox's theorem, the resulting category $F \boxtimes C$ will be cartesian.

I also claim that the right pseudoadjoint of $U$ is the 2-functor $[F, -]$, where the square brackets denote the internal hom adjoint to the $\boxtimes$ tensor product.

My post and the comments say a lot about what has and hasn't yet been proved. But I just learned about Berman's important article:

• John Berman, The commutative algebra of categories.

and hopefully this will help push things forward.