Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Monads with Operations

Joshua Meyers (Oct 28 2023 at 02:40):

Let $\mathcal{T}$ be a Lawvere theory with with generating object $x$. This induces an adjunction $F:\text{Set}\rightleftarrows\mathcal{T}\text{-Alg}:U$ defined by $U(A)\coloneqq Ax$ and $F(S)\coloneqq \mathcal{T}\text{-Alg}(x^S,-)$.

This in turn induces a monad $M\coloneqq UF : \text{Set}\to\text{Set}$, sending $S$ to $\mathcal{T}\text{-Alg}(x^S,x)$. Lots of familiar monads come about this way: the list monad, the free group monad, the Maybe monad, etc.

But when we construct a monad this way, we get an additional structure: For any operation $o:x^n \to x$ of $\mathcal{T}$, we get a morphism $\overline{o}:M^{\times n} \to M$ defined by $(\mathcal{T}\text{-Alg}(x^S,x))^n \cong \mathcal{T}\text{-Alg}(x^S,x^n) \xrightarrow{o_*} \mathcal{T}\text{-Alg}(x^S, x)$. Moreover, these morphisms define a product-preserving functor $\mathcal{T}\to \text{End}(\text{Set})$ sending $x\mapsto M$ and $o\mapsto \overline{o}$

For example, in the case where $\mathcal{T}$ is the theory for a monoid, we find that $M$ (the list monad) is a monoid in the category of endofunctors in two different ways: (1) in the monoidal category $(\text{End}(\text{Set}), \circ, \text{id}_{\text{Set}})$, and (2) in the monoidal category $(\text{End}(\text{Set}), \times, c_1)$.

Does anyone talk about this sort of monad with extra structure? What can be said about it?

Todd Trimble (Oct 28 2023 at 09:43):

It seems to me that all monads $M$ (let's say on $\mathrm{Set}$) bear this type of structure, insofar as all monads on $\mathrm{Set}$ can be construed as infinitary Lawvere theories.

$M(j)$ can be thought of as codifying the set of $j$-ary operations of the monad qua theory, in the sense that if $X$ is an $M$-algebra, then the algebra structure on $X$ induces (via what the nLab calls the "coYoneda lemma") a map

$\int^j M(j) \cdot X^j \cong M(X) \to X$

hence a map $M(j) \cdot X^j \to X$ dinatural in $j$, hence a map $M(j) \to \mathrm{Set}(X^j, X)$ natural in $j$ which interprets elements in $M(j)$ as operations on $X$. And so it would go when we correspondingly think of $M$ itself as an $M$-module via the monad multiplication:

$\int^j M(j) \cdot M(-)^j \cong M \circ M \to M$

which is what you're describing.

Joshua Meyers (Nov 03 2023 at 17:13):

Thanks! This is helpful. The context I'm thinking about is the language NRA in Limsoon Wong's thesis (see https://www.comp.nus.edu.sg/~wongls/psZ/wls-thesis.pdf on page 38). Here I guess we could get the operations $M(-)^j\to M$ by the procedure you are describing but you would need the ambient category to be $\text{Set}$ for sure, and Wong assumes much less in this case --- it is a cartesian category (not even closed!) with a strong monad $M$ and then you have operations $1\to M$ and $M\times M \to M$ forming a monoid.

Todd Trimble (Nov 04 2023 at 01:12):

(Ugh, finally. I thought I had sent this 6 hours ago, but then noticed it in my drafts folder, and have been struggling to send this again for the past 10 minutes.)

Joshua Meyers (Nov 04 2023 at 02:23):

I still only see your message about it

Joshua Meyers (Nov 04 2023 at 02:26):

I got your PM though!

Todd Trimble (Nov 04 2023 at 02:38):

The system seems to be malfunctioning for me.

Todd Trimble (Nov 04 2023 at 02:38):

Let me try something else.

Todd Trimble (Nov 04 2023 at 02:39):

(Original message)

At this point I'm confused as to what you're asking. It's not true that for any strong monad on a cartesian category, you get a (cartesian) monoid structure on $M$ for free: just consider the identity monad.

Todd Trimble (Nov 04 2023 at 02:39):

Something we can say: suppose $M$ is a strong monad on a cartesian category $\mathcal{C}$, and $(X, \alpha: M(X) \to X)$ is an $M$-algebra. Then, if $J$ is an object such that $X^J$ exists (i.e., if there exists a representing object for the functor $\mathcal{C}(J \times -, X)$), then for each morphism $t: 1 \to M(J)$, we have an accompanying operation $X^J \to X$ formed as the composite

$X^J \cong 1 \times X^J \overset{t \times \mathrm{id}}{\to} M(J) \times X^J \to M(J \times X^J) \to M(X) \overset{\alpha}{\to} X.$

where the first unlabeled non-isomorphism comes from the strength, and the second is $M$ applied to the universal arrow $J \times X^J \to X$.

Todd Trimble (Nov 04 2023 at 02:39):

For example, suppose $\mathcal{C}$ has finite coproducts and cartesian product distributes over these coproducts. By abuse of notation, let $j$ denote the $j$-fold coproduct of copies of the terminal object $1$. Then the ordinary cartesian power $X^j$ gives the above representing object, and for every formal "operation" $t: 1 \to M(j)$ we can form an actual operation $X^j \to X$ as above, for every $M$-algebra $X$. This applies in particular to algebras of the form $M(c)$, and we get operations $M(c)^j \to M(c)$ that are natural in $c$, hence a natural operation $M^j \to M$.

Todd Trimble (Nov 04 2023 at 02:39):

I don't immediately see a way of getting rid of the distributivity requirement. But you see that we can make do with far less than $\mathcal{C} = \mathrm{Set}$.

Patrick Nicodemus (Nov 04 2023 at 16:12):

Todd Trimble said:

The system seems to be malfunctioning for me.

I was having problems with Zulip yesterday, for me sending much smaller messages worked.

Todd Trimble (Nov 04 2023 at 16:38):

Thanks, Patrick. That's what I wound up doing.