5
$\begingroup$

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?

$\endgroup$
  • $\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
8
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

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.