# Cartesian envelope of a symmetric monoidal category

Is there a left adjoint to the forgetful functor from cartesian monoidal categories to symmetric monoidal categories? And if so: how can it be described explicitely.

In more detail: Given a symmetric monoidal category $\mathbb V$ i am looking for a monoidal functor

$$\chi:\mathbb V \to \mathcal C(\mathbb V)$$

into a cartesian monoidal category $\mathcal C(\mathbb V)$ such that every other monoidal functor

$$\varphi:\mathbb V \to \mathbb C$$

into a cartesian monoidal category $\mathbb C$ factors 'uniquely' over $\chi$.

-
what is a cartesian monoidal category? Do you mean a (symmetrical) monoidal closed one? –  Buschi Sergio Jun 2 '13 at 21:31
"A cartesian monoidal category (usually just called a cartesian category), is a monoidal category whose monoidal structure is given by the category-theoretic product (and so whose unit is a terminal object)." -- ncatlab.org/nlab/show/cartesian+monoidal+category –  Garlef Wegart Jun 3 '13 at 8:15
You look for a $2$-adjoint, right? See also the comments in Chris' answer. You don't want that $\hom(V,U(C))$ and $\hom(C(V),C)$ are isomorphic, but rather that they are equivalent. –  Martin Brandenburg Jul 15 '13 at 20:48

Yes, there is a left adjoint. Both the category $\textbf{Mon}$ of (symmetric) monoidal categories, and the category $\textbf{Cart}$ of Cartesian categories, are algebraic over the category $\textbf{Cat}$ of categories. That is, there are monads on $\textbf{Cat}$ whose categories of algebras are $\textbf{Mon}$ and $\textbf{Cart}$, respectively.

More interestingly, there is also a right adjoint, that sends a monoidal category $\textbf{C}$ to the category of comonoids in $\textbf{C}$. This is a classic result by Thomas Fox.

-
Shouldn't Mon and Cart be treated as 2-categories as opposed to 1-categories? Or is there some magic working behind the scenes that ensures that issues with higher coherences do not arise? –  Dmitri Pavlov Jun 3 '13 at 0:28
Dmitri, definitely they are 2-cateogries. I'm pretty sure that 1-categorically those algebraicity statements are false. E.g. associators correspond to associativity conditions in algebraic 2-theory, cartesian structure is encoded in adjunction between diagonal and multiplication, etc. But formally this doesn't seem to change anything, classical adjunction proofs can be repeated 2-categorically. –  Anton Fetisov Jun 3 '13 at 11:44
I should have specified that Fox uses strict monoidal functors as the morphisms. As Dmitri points out and Anton mentions, lax (or even strong) monoidal functors require 2-categories. –  Chris Heunen Jun 3 '13 at 14:11
Thanks for the link; how can said monads - and the left adjoint - be described explicitly? Any reference? –  Garlef Wegart Jun 4 '13 at 16:19
As usual with these abstract proofs you can trace them back and find explicit constructions - which are not really useful. Here, when your monoidal category is given by generators and relations, you just replace $\otimes$ by $\times$ in each relation. A basic example is the ($2$-)free symmetric monoidal category on one object, which is the permutation groupoid. Then the left adjoint maps it to the free cartesian category on one object, which should be $\mathsf{FinSet}^{\mathsf{op}}$. Such things get interesting when you really work out specific examples where no presentation is given. –  Martin Brandenburg Jul 15 '13 at 21:03

Edit I had developed a demonstration of the inexistence of the 'left adjoint funtor, this demonstration shows an error (sneaky) in the final, then (since it was long) I removed this part as unuseful.

EDIT I did this ultimate proof:

Premises:

1) We call a category with finite product (and final object, or empty product) cartesian, i.e. a category with a finite product monoidal structure, call a functor cartesian is it preserve finite product (and final object).

2) Given a category $\mathcal{C}$ its cartesian-closure (finite product completion) $Ct(\mathcal{C})$, is the (generalization) of the category $Pro(\mathcal{C})$ where we considering finite discrete diagrams (instead co-direct), its objets are the finite family $(X_i)_{i\in I}$ and its morphisms are $(f, \hat{f} ) : (X_i)_{i\in I } \to (Y_j)_{j\in J}$ with $\hat{f}: J \to I$ and $f=(f_j: X_{\hat{f}(j) } \to Y_j)_{j\in J }$ by composition $(g, \hat{g} )\circ (f, \hat{f} ) : (X_i)_{i\in I } \to (Y_j)_{j\in J}\to (Z_k)_{k\in K}$ as $\hat{f} \circ \hat{g}$ and $(g_k \circ f_{\hat{g}(k)})$. we have a full embedding $\iota: \mathcal{C}\to Ct(\mathcal{C}): X \mapsto (X)$ and we identify $X$ ith $\iota(X)= (X)$, we have that $(X_i)_{i\in I}= \times_{i\in I} X_i$. Then for $F: \mathcal{C} \to \mathcal{A}$ with $\mathcal{A}$ cartesian there exist unique (but isomorphism) $F': C(\mathcal{C}) \to \mathcal{A}$ such that $F=F'\circ \iota$. We have that $C(C(\mathcal{C}))\cong C(\mathcal{C})$ and if $\mathcal{C}$ is cartesian exist $r: C(\mathcal{C}) \to \mathcal{C}$ with $1= r\circ \iota$.\

3) Given a category $\mathcal{C}$, and a class $\Sigma$ of new arrow between object of $\mathcal{C}$, the phrase "add new isomorphisms $\Sigma$ to $\mathcal{C}$" means: add $\Sigma$ to the graph of $\mathcal{C}$, consider the congruences inducted by the composition of morphisms of $\mathcal{C}$ everywhere its possible, and consider the fraction category respect the class of morphisms $\Sigma$. The problem is that in general the Hom-classes of morphisms is a proper class, or in other terms then the new category belong to a more large set-universe.

End of Premises

Let $\textbf{V}$ monoidal. Let $\iota: \textbf{V} \to Ct(\textbf{V})$ the cartesian closure of the underling category (we exclude the final object given by the empty family, we'll see how get the final object in more useful way). Given a strict-monoidal functor $F: \textbf{V} \to \mathscr{A}$ with $\mathscr{A}$ cartesian, exist a (iso)unique cartesian functor $F': Ct(\textbf{V}) \to \mathscr{A}$ with $F= F' \circ W$, and for each such $F$ if $X \cong A_1 \otimes \ldots \otimes A_n$ then $F(X) \cong F(A_1) \times \ldots \times F(A_n)$, and also our reflector $\chi$ (see original question above) must have this property .

Then for each isomorphism $X \cong A_1 \otimes \ldots \otimes A_n$ in $\textbf{V}$, we have to add to $C(\textbf{V})$ a formal isomorphism $X \cong A_1 \times \ldots \times A_n$, we get a new (large) category $\widehat{\mathcal{C}}$ that still have the universal property for functors like $F$ before, then also its cartesian closure $C(\widehat{\mathcal{C}})$ have this property. Now, observe that the finite product of $C(\widehat{\mathcal{C}})$ are identified with the old finite product of $C(\mathcal{C})$ (identify singletons (or double singletons) with the object, and a finite family od finite families as a global finite family). Now make the quotient for the congruence generated by the identification of the natural projection $I\times I \to I$ by $I\times I \cong I\otimes I \cong I$, then follow that $I$ is the final object.

In fact from $A \cong A\otimes I\cong A\times I\to I$ follow a morphism $A \to I$, given $f, g: A \to I$ the couple of these are just a morphism $A \to I \times I \cong I\otimes I \cong I$ but the projections $I\times I \to I$ are both the composition $I\times I \cong I\otimes I\cong I$, then $f=g$.

Observing that the final $\widehat{\mathcal{C}}$ (with the final congruence) is in generale a LARGE category, then cannot be a result that come from theorem of existence of (left) adjoint based on properties of monadic functors or algebraic theory properties.

In the case of monoidal functors (original question), I claim that exist a left inverse:

to the (monoidal simmetric) category $\textbf{V}$ add a new object $e$ the arrow identity $1_e: e \to e$, for each $X \in \textbf{V}$ a new arrow $e^X: X \to e$ and a arrows family $(e_f: e \to A)_{f : I \to A }$ and let $\textbf{V}_e$ the category generated by all these new arrows: the morphisms are concatenation of some arrows of $\textbf{V}$ and some new arrows, where we compose arrows of $\textbf{V}$ whenever is possible, and the composition is for concatenation, in this category consider the congruence that identify all endomorphisms $e \to e$ to $1_e$, and $e^B\circ g\cong e^A$ and $e_{g\circ f}\cong g\circ e_f$ for $g: A\to B$, and let $\widehat{ \textbf{V}} := \textbf{V}_e/ \cong$ the quotient category.

Consider the category named "theory of $\widehat{ \textbf{V}}$-algebras" (see [LPAC] p. 146): the sorts are the object of $\widehat{\textbf{V}}$ and operators (of sort $B$): $A_1 \times \ldots \times A_n \to B$ are (formal labels of) morphisms $f: A_1\otimes \ldots \otimes A_n \to B$ in $\widehat{ \textbf{V}}$ where indicate the sequence of sorts as a (formal) product, and where the monoidal tensor is thinked with brackets (all moved to the left). Briefly this category has for object the finite sequences of objects of $\textbf{V}$ (write as formal product): $X_1\times \ldots \times X_n$, the product of these objects is defined for sequences concatenation. Morphism are defined (as formal strings) for induction as follow:

operators labels as above $f: A_1 \times \ldots \times A_n \to B$ (for $f: A_1\otimes \ldots \otimes A_n \to B$ in $\widehat{ \textbf{V}}$) are morphisms of $C(\textbf{V})$.

(formal) projections $\pi_k : A_1 \times \ldots \times A_n \to A_k$ are morphisms of $C(\textbf{V})$.

Give morphisms $h: Y_1 \times \ldots \times Y_n \to X$ and morphisms $k_i: X_i \to Y_i$ $1 \leq i \leq n$ then the formal string $h(k_1,\ldots, k_n)$ is a morphisms of $C(\textbf{V})$.

Morphisms $A \to (X_1\times\ldots \times X_n)$ are just sequences $h_i: A \to X_i$ $1 \leq i \leq n$ of morphisms.

Now, let $C(\widetilde{V})$ the full subcategory with object the product $X_1\times \ldots \times X_n$ where $X_i\in \textbf{V}$ $1\leq i\leq n$, plus the object $e$ and define $X\times e= e\times X= X$ for any $X\in C(\widetilde{V})$ (then $e\times\ldots \times e= e$), and define the compositions $e \xrightarrow{(e_{f_1},\ldots, e_{f_n})} A_1\times\ldots \times A_n \xrightarrow{g} B$ as $e_{g\circ (f_1\odot \ldots \odot f_n)}$ where $f_1\odot \ldots \odot f_n: I \cong I\otimes\ldots \otimes I \xrightarrow{(f_1,\ldots, f_n)}A_1\otimes\ldots \otimes A_n$

. We have that $e$ is a final object of $C(\widetilde{V})$ and this category has finite product.

The monoidal functor $\chi: \textbf{V}\to C(\textbf{V})$ map objects and morphisms in themselves, with $\widetilde{\chi}_{A, B}: \chi(A, B) \to \chi(A) \times \chi(B)$ given by $1_{A\otimes B}$, and $\chi_o: e \to \chi(I)$ given by $e_{1_I}$. For $F: \textbf{V}\to \mathcal{C}$ monoidal, where $\mathcal{C}$ is cartesian, $\widetilde{F}: C(\textbf{V})\to \mathcal{C}: X_1\times\ldots \times X_n \mapsto FX_1\times\ldots \times FX_n$ is the only cartesian functior such that $\widetilde{F}\circ \chi = F$.

Biblio:

[LPAC] : "locally presentable and accessible categories". Adámek , Rosický. Cambridge University Press 1994

-