I'm trying to find a simple proof that a monoid under Day convolution is equivalent to a lax monoidal functor (see nCatLab). For simplicity, consider functors from $C$ to $Set$. For $F$ to be a monoid there has to be a natural transformation:

$ \mu : F \otimes F \to F $

where the tensor product is the Day convolution:

$F\otimes F := \int^{x y} C(x \otimes y, -) \times F(x) \times F(y)$

A lax monoidal functor has a natural transformation:

$F(x) \times F(y) \to F(x \otimes y)$

which we can plug in to get:

$\int^{x y} C(x \otimes y, -) \times F(x \otimes y)$

If I could only make a "change of variables" from $(x, y)$ to $x\otimes y$, like this:

$\int^{x \otimes y} C(x \otimes y, -) \times F(x \otimes y)$

I could use the ninja Yoneda lemma to perform the integral and get $F$. How do I convert this handwaving argument to a proof?

  • $\begingroup$ The case of sets does not simplify the question. The general case works exactly the same. $\endgroup$ – HeinrichD Mar 10 '17 at 11:04

This can be seen via a sequence of isomorphisms involving ends and co-ends, using the presentation of natural transformations via ends:

$$ \begin{array}{cl} & \int_{xy} Fx \times Fy \to F (x \otimes y) \\ \cong& \int_{xy} Fx \times F y \to (\int_z C(x \otimes y,z) \to Fz) & (1) \\ \cong& \int_{xyz} Fx \times Fy \to C(x \otimes y,z) \to Fz & (2) \\ \cong& \int_{xyz} Fx \times Fy \times C(x \otimes y,z) \to Fz & (3) \\ \cong& \int_z (\int^{xy} Fx \times Fy \times C(x \otimes y,z)) \to Fz & (4) \\ \cong& \int_z (F \otimes F)z \to Fz & (5) \\ \cong& F \otimes F \Rightarrow F & (6) \end{array} $$

where $(1)$ is by Yoneda; $(2)$ is commuting of ends with exponentials; $(3)$ is currying; $(4)$ is currying with ends/co-ends; $(5)$ is the definition of the Day product; and $(6)$ is natural transformations as ends.


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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