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: Pullback of monads

Harrison Grodin (Jan 02 2025 at 21:09):

I've noticed that you can (seemingly rather canonically?) combine two monads by taking their pullback. Let $T$ and $U$ be monads. I believe the following pullback is also a monad:

pullback pointwise
or, applied to $X$:
applied to X

I've seen this pattern in @Egbert Rijke - @Mike Shulman - @Bas Spitters's "Modalities in HoTT", where $\bigcirc \times_{♢ \circ \bigcirc} ♢$ is written as the "join" $\bigcirc \lor ♢$, and the [[fracture theorem]] says that (under some conditions) $\bigcirc \lor ♢ = \text{Id}$.

I have recently found this construction to be useful in cases where the monads in question aren't idempotent, too. Is this construction studied (or even named/written down) anywhere else?

(I would assume so, but unfortunately looking up "monad join" and "monad pullback" lead me to other things!)

John Baez (Jan 02 2025 at 21:28):

Wow, this is weird! I'll temporarily take your word for it that it works. I note it's not symmetrical in the two monads $U$ and $T$, or at least it doesn't look like it. What's the pullback of (say) the monad for groups and the monad for groups?

Ryan Wisnesky (Jan 02 2025 at 21:39):

I've always heard that monads don't compose, but to define pullback one must use composition?

Harrison Grodin (Jan 02 2025 at 21:42):

John Baez said:

Wow, this is weird! I'll temporarily take your word for it that it works. I note it's not symmetrical in the two monads $U$ and $T$, or at least it doesn't look like it. What's the pullback of (say) the monad for groups and the monad for groups?

Agreed, it's definitely not symmetric in $U$ and $T$!

If $T$ and $U$ are both the free monoid monad $\mathbf{Set} \to \mathbf{Set}$, then I think the pullback should be the identity monad - an element would have to be a pair of lists $(l_1 : \text{List}(X), l_2 : \text{List}(X))$ such that $[l_1] = \text{List}([-])(l_2)$, which I believe is equivalent to requiring that both $l_1$ and $l_2$ are equal singleton lists (with a single element of $X$) by injectivity of $[-]$. I think the free group monad should be the same story?

If $T$ is the free group monad and $U$ is some open modality on a topos (cf RSS), though, the story is more interesting - the pullback classifies group syntax that collapses in the open subtopos to a generator, eg strings like $x_1 \cdot x_2^{-1} \cdot y$ that cancel to just $y$ in the open subtopos (assuming $x_1 = x_2$ in the open subtopos).

Harrison Grodin (Jan 02 2025 at 21:44):

Ryan Wisnesky said:

I've always heard that monads don't compose, but to define pullback one must use composition?

Right, I'm using $U \circ T$ here, but I'm not assuming that it forms a monad! I'm just composing the endofunctors and using their composite to "connect" the two "components" of the pullback. (Or maybe this isn't what you're saying?)

Chris Grossack (they/them) (Jan 02 2025 at 21:54):

It doesn't look like there's anything special about monads here... As we famously know, a monad is just a monoid in $\text{End}(C)$, with it's (noncommutative!) monoidal structure coming from composition. If your observation works, it'll probably work at the level of "the pullback of monoids in a monoidal category along their tensor product is again a monoid"

Chris Grossack (they/them) (Jan 02 2025 at 21:55):

That's something that might counterintuitively be easier to work out, because there's less baggage about monads and distributive laws (which I guess in this context are kind of like a braiding... I've never noticed that before!) hanging around

Jean-Baptiste Vienney (Jan 02 2025 at 22:30):

Harrison Grodin said:

I've noticed that you can (seemingly rather canonically?) combine two monads by taking their pullback. Let $T$ and $U$ be monads. I believe the following pullback is also a monad:

pullback pointwise
or, applied to $X$:
applied to X

I've seen this pattern in Egbert Rijke - Mike Shulman - Bas Spitters's "Modalities in HoTT", where $\bigcirc \times_{\bigcirc \circ ♢} ♢$ is written as the "join" $\bigcirc \lor ♢$, and the [[fracture theorem]] says that (under some conditions) $\bigcirc \lor ♢ = \text{Id}$.

I have recently found this construction to be useful in cases where the monads in question aren't idempotent, too. Is this construction studied (or even named/written down) anywhere else?

(I would assume so, but unfortunately looking up "monad join" and "monad pullback" lead me to other things!)

I would be surprised that it works without assuming that the pullback is preserved by $T$ and/or $U$.

Same comment for pullbacks of monoids in a monoidal category. It should work with an assomption of the type “pullbacks are preserved by tensor product” or maybe just that the pullback of interest is preserved by tensoring by any of the two monoids on each side.

Jean-Baptiste Vienney (Jan 02 2025 at 22:32):

(I think you will need something like this when you try to prove associativity and unitality)

Mike Shulman (Jan 02 2025 at 22:38):

I would also be surprised if it works without any additional conditions.

But I've been surprised before.

Harrison Grodin (Jan 02 2025 at 22:39):

(Sorry, yes, I should say that I haven't checked all of the conditions in detail! This construction seems to work in the cases I've checked, but I expect there are some conditions required in general.)

Notification Bot (Jan 02 2025 at 23:15):

This topic was moved here from #learning: reading & references > Pullback of monads by Harrison Grodin.

Chris Grossack (they/them) (Jan 02 2025 at 23:16):

I'm trying to work it out right now, and I agree: "flatness" of A and B (in the sense that tensoring with either preserves limits) seems necessary to even get started. But I don't have a full construction yet

Aaron David Fairbanks (Jan 03 2025 at 01:26):

@Sridhar Ramesh and I also have noticed this construction. It works for arbitrary monoids (assuming the pullback exists). I can upload an argument soon.

Aaron David Fairbanks (Jan 03 2025 at 01:51):

Here's an argument with string diagrams that was in my notes. Sorry if this is unreadable, I can translate it into words later.
uAK3gSxn.jpg
Red is T, blue is U, and purple is the relevant pullback. The grey nodes are the pullback projection maps. Points where wires merge/appear are the monoid multiplications/units.

Aaron David Fairbanks (Jan 03 2025 at 01:54):

We also see here that the projections are monoid homomorphisms.

Aaron David Fairbanks (Jan 03 2025 at 02:49):

Now with words:

For convenience denote by $S$ the pullback of $\mathrm{id}_T \otimes \eta_U$ and $\eta_T \otimes \mathrm{id}_U$, and denote by $p_T : S \to T$ and $p_U: S \to U$ the projections.

For each $n$, we have an $n$-ary map $t_n : S \otimes \ldots \otimes S \to T$ obtained by composing $p_T \otimes \ldots \otimes p_T$ with the $n$-ary multiplication for $T$. Similarly, we have an $n$-ary map $u_n : S \otimes \ldots \otimes S \to U$.

Hence we can form maps $t_n \otimes u_m: S \otimes \ldots \otimes S \to T \otimes U$. Observe $t_n \otimes u_m = t_{n'} \otimes u_{m'}$ whenever $n + m = n' + m'$, by repeatedly introducing units and applying the defining equation for the pullback.

In particular, for each $n$,
$t_n ; (\mathrm{id}_T \otimes \eta_U) = t_n \otimes \eta_U = t_n \otimes u_0 = t_0 \otimes u_n = \eta_T \otimes u_n = u_n ; (\eta_T \otimes \mathrm{id}_U)$.
By the universal property of the pullback, we thus obtain a unique map $\mu_n: S \otimes \ldots \otimes S \to S$ such that $\mu_n ; p_T = t_n$ and $\mu_n ; p_U = u_n$. This will be the $n$-ary multiplication for $S$.

The $n$-ary associativity/unit laws say that every $n$-ary map $S \otimes \ldots \otimes S \to S$ obtained as a tree composed of $\mu_i$ maps is itself $\mu_n$. Indeed, any such tree $\mu'_n$ composed of $\mu_i$ maps satisfies $\mu'_n ; p_T = t_n$ and $\mu'_n ; p_U = u_n$, using the associativity/unit laws for $T$ and $U$, and so $\mu'_n = \mu_n$ by uniqueness of the pullback factoring map.

Aaron David Fairbanks (Jan 03 2025 at 02:53):

The proof idea came from @Sridhar Ramesh.

Mike Shulman (Jan 03 2025 at 02:55):

My brain hurts. It's hard to think about this because for the familiar case of monoids in Set (or any cartesian monoidal category), and I think also for monoids in Ab (i.e. rings), this pullback is always trivial. Are there any monoidal categories that are simpler than endofunctors in which this pullback is nontrivial?

Also, is this pullback ever nontrivial for monads on Set?

Mike Shulman (Jan 03 2025 at 03:17):

Trying to understand this some more... generalizing the example of the free group monad and the open modality, I think we can say that if $U$ is a [[semi-left-exact reflection]], then the map $T\times_{U\circ T} U \to T$ is the right half of the $U$-factorization of the unit $\mathrm{Id} \to T$.

Aaron David Fairbanks (Jan 03 2025 at 05:01):

The reason I was interested in this originally was from a conversation with Peter Selinger where we were just looking at the case of monads on Set and where $T = 1$, the terminal monad. So, we were looking at the pullback of $\eta: 1 \to U(1)$ and $U(!): U(X) \to U(1)$.

The new monad $S$ created from this process satisfies $S(1) = 1$, and if $U(1) = 1$ already then we just get $U = S$.

From the powerset monad we get the "nonempty powerset" monad sending a set to the set of its nonempty subsets. As I think is being discussed by @Harrison Grodin and @Mike Shulman in greater generality (but I don't yet understand that level of generality), from the free group monad we get a monad corresponding to an algebraic theory where the operations are group words such that the number of inverted letters is one less than the number of non-inverted letters.

Nathanael Arkor (Jan 03 2025 at 05:45):

Aaron David Fairbanks said:

The new monad $S$ created from this process satisfies $S(1) = 1$, and if $U(1) = 1$ already then we just get $U = S$.

I don't suppose this happens to be the cofree [[affine monad]] on $U$?

John Baez (Jan 03 2025 at 06:08):

What's an affine monad?

Nathanael Arkor (Jan 03 2025 at 06:13):

One that preserves the terminal object.

Nathanael Arkor (Jan 03 2025 at 06:14):

Presumably this forms a monoidal structure, whose unit is the unit monad. What do the monoids with respect to this monoidal structure look like?

Aaron David Fairbanks (Jan 03 2025 at 06:33):

Nathanael Arkor said:

I don't suppose this happens to be the cofree [[affine monad]] on $U$?

Yes, I think so.