I have two questions about this note by T. Trimble, which I warmly invite to answer.

First question

I am trying to prove that these two functors are mutually inverses:

  1. The functor $U\colon \mathbf C\to [\mathbf{Sets}^\mathbf{Fin},\mathbf C]$ which sends $c\in\bf C$ to the functor $F\mapsto \int^nF(n)\cdot c^n$ (given two cmc categories (see Trimble's note), we denote $[\bf C,D]$ the category of product preserving and cocontinuous functors $\bf C\to D$);
  2. The functor $V\colon [\mathbf{Sets}^\mathbf{Fin},\mathbf C]\to \bf C$ which evaluates a functor $\Phi\colon \mathbf{Sets}^\mathbf{Fin}\to \mathbf C$ in $\hom(1,-)\colon \bf Fin\to Sets$.

It is quite obvious that $VU(c)\cong c$ since $$ c\stackrel{VU}{\longmapsto}\int^n \hom(1,n)\cdot c^n\stackrel{\text{Yoneda}} {\cong}c^1=c $$ I am stuck in proving that the composition $U\circ V$ is isomorphic to ${\rm id}_{[\mathbf{Sets}^\mathbf{Fin},\mathbf C]}$: following Trimble's notations $$ \Phi\stackrel{UV}{\longmapsto} \left(F\mapsto \int^n F(n)\cdot \Phi(\hom(1,-))^n\right) $$ now $\int^n F(n)\cdot \Phi(\hom(1,-))^n$ can be simplified since $\Phi$ is product preserving, but I'm not able to find out why it should be equal to $\Phi(F)$.

Second question

Unless a mysterious duality is involved, I think that this construction gives a co-monad. Where am I wrong?

This question was originally posted on math.SE; Martin Brandenburg pointed out that the equivalence ${\rm Cocont}(\mathbf{Sets}^\mathbf{Fin},\mathbf C)\cong {\rm Fun}(\mathbf{Fin}^\text{op},\mathbf C)$ restricts to an equivalence between the sole product-preserving functors, which is sort of the reason this equivalence exists. The fact is that even if it works, I think that the aim of Trimble's note was to give an explicit definition of the functors realizing the equivalence: Instead of finding a formal reason for the equivalence to hold (which is exactly the Universal Property of PSh(C), as Martin Brandenburg said), I would rather know how to manipulate that coend in order to get $\Phi(F)$ back.

  • $\begingroup$ For $F: Fin \to Set$ you have $F(-)= \int_n (n, -)\cdot F(n)$ (cofine expression of $F$ as colimit of representables). Then $\Phi(F)\cong \int_n \Phi((n, -))\cdot F(n) $ but $(n, -)= (\coprod_n 1, -) = \prod_n (1, -)= (1,-)^n$ . $\endgroup$ – Buschi Sergio Jul 18 '13 at 8:41
  • $\begingroup$ Maybe I misunderstood you, but I think that you need some additional hypoteses to do that manipulation: $\Phi$ certainly enters the coend defining $F$ as $\int^n {\bf Sets}(n,-)\cdot Fn$, but now you'll need that $\Phi$ "respects the copower" in the sense that $\Phi\big({\bf Sets}(n,-)\cdot Fn\big)\cong \Phi({\bf Sets}(n,-))\cdot Fn$. Is this always true? Where am I wrong? $\endgroup$ – Fosco Jul 18 '13 at 8:58
  • $\begingroup$ The former proerty is true iff $\Phi$ is a left adjoint, as you can check in proposition 2.2.2 of Gray's "Closed categories". $\endgroup$ – Fosco Jul 18 '13 at 9:08
  • $\begingroup$ $\Phi$ is in $[Set^{Fin}, C]$ the category of cocontinuous (i.e. colimit preserving) and procuct preserving functors, and a copower is a coproduct... $\endgroup$ – Buschi Sergio Jul 18 '13 at 9:27
  • $\begingroup$ Yup, you're right. $\endgroup$ – Fosco Jul 18 '13 at 9:53

For the first question, we have natural isomorphisms

$$U V(\Phi)(F) = \int^n F(n)\cdot \Phi(\hom(1,-))^n \cong \int^n F(n)\cdot \Phi(\hom(1,-)^n) \cong \int^n \Phi(F(n)\cdot \hom(1,-)^n)$$

$$\cong \Phi(\int^n F(n)\cdot \hom(1,-)^n) \cong \Phi(\int^n F(n) \cdot \hom(n, -)) \cong \Phi(F)$$

where the first isomorphism uses the fact that $\Phi$ preserves products, the second and third use cocontinuity of $\Phi$ (I think Buschi Sergio pointed out that the notation $S \cdot G$ indicates a coproduct of copies of $G$ indexed over a set $S$), and the last uses the Yoneda lemma. Being natural in $F$, this shows we have an isomorphism $UV(\Phi) \cong \Phi$ (natural in $\Phi$).

It might help to compare Kelly's theory of operads, where a launching point is a universal property of Day convolution:

  • If $M$ is a symmetric monoidal category, then the Yoneda embedding $y: M \to Set^{M^{op}}$ is a symmetric monoidal functor (where the codomain has been equipped with the Day convolution product induced from the product on $M$), and is universal among symmetric monoidal functors from $M$ to symmetric monoidally cocomplete categories (meaning the monoidal product preserves colimits in each factor).

Here what we are essentially doing is making the observation/calculation that if the monoidal product on $M$ is the cartesian product, then the induced Day convolution is also the cartesian product, and if we replace "symmetric monoidal" by "cartesian monoidal" throughout the displayed statement, the result again holds. Then, parallel to what Kelly does, we observe that $\text{Fin}^{op}$ (the category opposite to finite sets) is the free cartesian monoidal category on one object (i.e., on the terminal category), analogous to the fact that the finite permutation category $\mathbf{P}$ is the free symmetric monoidal category on one object.

So the idea is just to develop a little theory of cartesian operads parallel to Kelly's approach to ordinary permutative operads, and then observe the essential equivalence between cartesian operads and (finitary) Lawvere theories.

By the way, I wouldn't call this "my theory" -- it's my feeling that all the observations I'm making are already well-known to a lot of people, but it seems to be very hard to find a source where it's all written down. More on this in a moment.

For the second question, it might help to remember that on $Cat$ (2-category of small categories, say), the functor $X^-: Cat^{op} \to Cat$ for a given category $X$ reverses the direction of 1-cells but preserves the direction of 2-cells. (This is an easy exercise.) So given say a 2-cell $F G \to H$, we would get an induced 2-cell $X^G X^F \to X^H$. Similarly, if $M$ is a monad on $C$ with multiplication $m: MM \to M$, we get an induced monad (not comonad) on $X^C$ with multiplication $X^m: X^M X^M \to X^M$.

On similar grounds, given a cartesian operad $M$, inducing a (cocontinuous product-preserving) monad $- \odot M: \text{Set}^{\text{Fin}} \to \text{Set}^{\text{Fin}}$, we get an induced monad

$$[- \odot M, C]: [\text{Set}^{\text{Fin}}, C] \to [\text{Set}^{\text{Fin}}, C]$$

for any cartesian monoidally cocomplete $C$.

Finally, I'd like to say what spurred me to start writing the note referred to in the OP. It was really this question of Martin Brandenburg, where my answer involved a coend formula for monads $T$ based on a Lawvere theory $\theta$. Martin asked for a proof of the coend formula (which he said he knew in the case where $C = \text{Set}$, but not for general cartesian monoidally cocomplete $C$).

I had tried to explain what was behind the coend formula in a string of comments that appealed to an analogy with ordinary permutative operads -- that there is a completely parallel development for cartesian operads and Lawvere theories. Based on Martin's lack of response to that comment string, it seems my arguments didn't convince him -- and unfortunately I couldn't refer to the literature because I don't know of a place where this is spelled out. (Even though I believe it has to be well-known to people who have studied Kelly's work on operads. There's an article by Hyland and Power which comes pretty close to being a reference for what Martin wants, but not quite.)

Thus, I began writing all this stuff down, out of a belief that it's all very soft and conceptual and ought to be recorded. I just hadn't announced it to anyone at MO yet.

Now, spurred by yet another MO question, I may get back to that note (which was left in a slightly incomplete state)!

| cite | improve this answer | |
  • $\begingroup$ Richard Garner recently talked about the connection between finitary monads and Lawvere theories via categories enriched over $[\mathbf{FinSet}, \mathbf{Set}]$ (or equivalently, finitary endofunctors on $\mathbf{Set}$). $\endgroup$ – Zhen Lin Jul 18 '13 at 14:54

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.