4
$\begingroup$

The nLab states that a semicartesian monoidal category equipped with natural transformations $\delta_x : x \to x \otimes x$ such that $\pi_1 \circ \delta_x = 1_x$ and $\pi_2 \circ \delta_x = 1_x$ (where $\pi_1$ and $\pi_2$ are the definable projections), is automatically cartesian.

I'm looking for a proof of this statement.

I managed to show that given $f_1 : a \to b_1$ and $f_2 : a \to b_2$, we can construct a map $(f_1, f_2) : a \to b_1 \otimes b_2$ as $(f_1, f_2) = (f_1 \otimes f_2) \circ \delta_a$, and this map projects appropriately: \begin{equation} \pi_i \circ (f_1 \otimes f_2) \circ \delta_a = f_i \circ \pi_i \circ \delta_a = f_i. \end{equation}

Now I'm trying to show that $(f_1, f_2)$ is the unique map with this property. However, I seem to require that $(\pi_1 \otimes \pi_2) \circ \delta_{x \otimes y} = 1_{x \otimes y}$. Then if there is another function $h : a \to b_1 \otimes b_2$ such that $\pi_i \circ h = f_i$, we have \begin{equation} h = (\pi_1 \otimes \pi_2) \circ \delta_{b_1 \otimes b_2} \circ h = (\pi_1 \otimes \pi_2) \circ (h \otimes h) \circ \delta_a = (f_1 \otimes f_2) \circ \delta_a = (f_1, f_2). \end{equation} Is it correct that we need to postulate this "$\eta$-equality"? I have an intuition that it may somehow follow from the unit laws (since it already holds if either $x$ or $y$ is the terminal object), but I don't know how to prove that.

$\endgroup$
4
  • 2
    $\begingroup$ The statement on the nlab requires that the diagonal be a monoidal natural transformation, not just a natural transformation. That ought to give the identity you’re after. $\endgroup$ – Dylan Wilson Dec 16 '19 at 14:21
  • 2
    $\begingroup$ Thanks, I had indeed read over the word "monoidal". However, it seems to me that the functor $x \mapsto x \otimes x$ is not in general a monoidal functor; one needs to assume that the category is symmetric monoidal. $\endgroup$ – dremodaris Dec 16 '19 at 15:48
  • 1
    $\begingroup$ From the looks of things, the writers of the nlab article seem to mostly have symmetric monoidal examples in mind. It's quite possible that this hypothesis was inadvertently left out. It's certainly necessary, as a cartesian monoidal structure is in particular symmetric. I might guess that the data of a symmetry on a semicartesian monoidal category is equivalent to the data of a strong monoidal structure on the diagonal functor, but I haven't checked this. $\endgroup$ – Tim Campion Dec 16 '19 at 17:05
  • 3
    $\begingroup$ I think that yes, the monoidal category should be assumed symmetric. At least, that adjective is present in the notes cited (p47), and you're right that only when the categoris symmetric (or at least braided) is the tensor a monoidal functor. I've added the word "symmetric" to the nLab page, thanks. $\endgroup$ – Mike Shulman Dec 17 '19 at 4:02
2
$\begingroup$

As pointed out by Dylan Wilson, the nLab postulates that $\delta$ be a monoidal natural transformation. This requires that the functor $Gx = x \otimes x$ be a (lax/oplax) monoidal functor. Let us assume that the category is symmetric monoidal, then $G$ is strong (in the sense of non-lax) monoidal. Then we have an isomorphism \begin{equation} \iota : G(x \otimes y) = (x \otimes y) \otimes (x \otimes y) \cong (x \otimes x) \otimes (y \otimes y) = Gx \otimes Gy \end{equation} Of course the symmetric structure provides multiple such morphisms, but naturality w.r.t. $x \to \top$ and $y \to \top$ implies that $\pi_i \circ \iota = G\pi_i = \pi_i \otimes \pi_i$, which reveals that $\iota$ swaps the middle two components.

Then we have \begin{align*} (\pi_1 \otimes \pi_2) \circ \delta_{x \otimes y} &= (\pi_1 \otimes \pi_2) \circ \iota \circ \delta_{x \otimes y} \\ &= (\pi_1 \otimes \pi_2) \circ (\delta_x \otimes \delta_y) \\ &= (1 \otimes 1) = 1, \end{align*} proving the equation that was missing in the question.

$\endgroup$
1
  • $\begingroup$ In retrospect, I do not see how to prove $(\pi_1 \otimes \pi_2) \circ \delta_{x \otimes y} = (\pi_1 \otimes \pi_2) \circ \iota \circ \delta_{x \otimes y}$, unless by circular reasoning. $\endgroup$ – dremodaris Jan 27 at 19:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.