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: distributive laws and monadic functors

Jonas Frey (Dec 04 2023 at 06:04):

Given monads $L,\Sigma:\mathbb C\to\mathbb C$ and a distributive law $\delta : L\circ\Sigma\to\Sigma\circ L$ of $L$ over $\Sigma$, the monad $\Sigma$ 'lifts' to $L$-algebras, $L$ 'extends' to the Kleisli category of $\Sigma$, and the composite functor $\Sigma\circ L$ is a monad, whose algebras are (equivalent to) the algebras of the lifted monad on $L$-algebras.

Thus, we have a commutative triangle of monadic functors

$$\begin{matrix} \mathbb C^{\Sigma L} & \to & \mathbb C^L \\ & \searrow & \downarrow \\ && \mathbb C \end{matrix}$$

which is nice, since monadic functors don't compose in general.

However, it seems that in the most well-known example --- namely the distributivity of the monoid monad over the abelian group monad on $Set$ --- we seem to have a commutative square

$$\begin{matrix} Ring & \to & Mon \\ \downarrow & & \downarrow \\ Ab &\to & Set \end{matrix}$$

of monadic functors?

Is this special to this case (maybe because the Ab-monad is commutative), or is $\mathbb C^{\Sigma L}$ always monadic over $\mathbb C^\Sigma$ (besides being monadic over $\mathbb C^L$?

Ralph Sarkis (Dec 04 2023 at 06:56):

Are you sure that $\mathbf{Ring} \to \mathbf{Ab}$ is monadic? I thought that would imply the free abelian group monad distributes over the free commutative monad (which is not the case, they distribute only the opposite way).

Jonas Frey (Dec 04 2023 at 07:08):

No I'm not sure, but I think it has a left adjoint, given by the tensor algebra formula. Maybe it's only enriched monadic?

Tom Hirschowitz (Dec 04 2023 at 07:39):

Indeed, it should have a left adjoint, by the [[adjoint lifting theorem]].

John Baez (Dec 04 2023 at 08:10):

Since rings are monoids in $(\mathsf{Ab}, \otimes)$ and some other nice things hold ($\mathbb{Ab}$ has colimits and $\otimes$ distributes over colimits) we can build the free ring on an abelian group using a standard trick for building the free monoid in a monoidal category $(\mathsf{C}, \otimes)$, which works when this monoidal category has colimites and the tensor product distributes over them:

• Steve Lack, A note on the construction of free monoids.

John Baez (Dec 04 2023 at 08:11):

This standard trick is the "tensor algebra formula" @Jonas Frey mentioned.

John Baez (Dec 04 2023 at 08:11):

I think this gives a left adjoint to the forgetful functor $\mathsf{Ring} \to \mathsf{Ab}$.

John Baez (Dec 04 2023 at 08:13):

But if this forgetful functor really has a left adjoint and is really not monadic, we get an interesting puzzle! What is the Eilenberg-Moore category of this adjunction between $\mathsf{Ring}$ and $\mathsf{Ab}$?

Mike Shulman (Dec 04 2023 at 08:53):

It's monadic. For instance, it's a special case of the fact that the category of algebras for an enriched operad is monadic. But I don't think this is true for a general distributive law; note that the monad here on Ab is not really built in any obvious way out of the two original monads on Set.

Ralph Sarkis (Dec 04 2023 at 09:01):

Mike Shulman said:

[...] note that the monad here on Ab is not really built in any obvious way out of the two original monads on Set.

Ok, so this is why we do not get a distributive law of the other type out of this monadicity.

John Baez (Dec 04 2023 at 10:04):

So we've got a monadic right adjoint $\mathsf{Ring} \to \mathsf{Set}$ that's the composite of monadic right adjoints $\mathsf{Ring} \to \mathsf{Ab} \to \mathsf{Set}$ (first forget the multiplication, then the addition) even though addition doesn't distribute over multiplication? If so, this is a nice counterexample to keep in mind.

(For beginners: of course $\mathsf{Ring} \to \mathsf{Set}$ is also the composite of monadic right adjoints $\mathsf{Ring} \to \mathsf{CommMon} \to \mathsf{Set}$ (first forget the addition, then the multiplication) where we do have a distributive law that explains why the composite is monadic.)

Mike Shulman (Dec 04 2023 at 17:13):

It's funny, because to me the composite $\rm Ring \to Ab \to Set$ feels more "natural" than $\rm Ring \to CMon \to Set$. I think more naturally of a ring as "an abelian group with the extra structure of a multiplication" than as "a commutative monoid with the extra structure of an addition". But distributive laws disagree...

Todd Trimble (Dec 04 2023 at 17:45):

John Baez said:

So we've got a monadic right adjoint $\mathsf{Ring} \to \mathsf{Set}$ that's the composite of monadic right adjoints $\mathsf{Ring} \to \mathsf{Ab} \to \mathsf{Set}$ (first forget the multiplication, then the addition) even though addition doesn't distribute over multiplication? If so, this is a nice counterexample to keep in mind.

(For beginners: of course $\mathsf{Ring} \to \mathsf{Set}$ is also the composite of monadic right adjoints $\mathsf{Ring} \to \mathsf{CommMon} \to \mathsf{Set}$ (first forget the addition, then the multiplication) where we do have a distributive law that explains why the composite is monadic.)

There are various theorems about when monadic functors compose, that have nothing to do with distributive laws. One is that if $U: A \to B$ and $V: B \to C$ both have left adjoints, both reflect isomorphisms, and both preserve reflexive coequalizers, then of course the same is true of their composite $VU: A \to C$. But this trio of conditions is sufficient for monadicity; this result is called the "crude monadicity theorem". Hence $VU$ is monadic as well.

Todd Trimble (Dec 04 2023 at 17:45):

As a matter of fact, if $U$ is crudely monadic and $V$ is merely monadic, then $VU$ is also monadic. This, together with some related results, is stated as a theorem in Toposes, Theories, and Triples by Barr and Wells. (But alas, with a one-word proof: "Easy".)

Todd Trimble (Dec 04 2023 at 17:46):

In the go-to example where monadic functors do not compose, namely the pair of forgetful functors

$\mathrm{Cat} \to \mathrm{RefGph} \to \mathrm{Set}$

where the first functor takes a category to its underlying reflexive graph and the second takes a reflexive graph to its set of edges, the first functor does not preserve reflexive coequalizers. Indeed, coequalizers in $\mathrm{Cat}$ can introduce some complications due to looping: the categories $\{\ast\}$ and $\mathbf{2} = (0 \to 1)$ are finite and rather simple, but the coequalizer of the two functors $0, 1: \{\ast\} \rightrightarrows \mathbf{2}$ is infinite (the additive monoid $\mathbf{N}$ as a one-object category).

Mike Shulman (Dec 04 2023 at 17:59):

In my head, the "default" is that the composite of two monadic functors should be monadic, and counterexamples like that are "pathological". I don't know whether that's justified though.

Todd Trimble (Dec 04 2023 at 19:03):

Yeah, it could be fun to think up more such counterexamples. I haven't thought about it, though.

Jonas Frey (Dec 04 2023 at 21:40):

Thanks for your all your input! Here's how I see the situation now:

• Given a distributive law $L\circ \Sigma\to\Sigma\circ L$, we always have a commutative square of forgetful functors

$$\begin{matrix} \mathbb C^{\Sigma L} & \to & \mathbb C^L \\ \downarrow & \searrow & \downarrow \\ \mathbb C^L&\to& \mathbb C \end{matrix}$$

where the diagonal, and all sides except the left one are monadic.

• Using the [[adjoint lifting theorem]] that @Tom Hirschowitz pointed out, we get a left adjoint to the left side as soon as certain coequalizers exist, which is a pretty weak assumption.
• if the left adjoint exist, then it is automatically monadic because monadic functors satisfy a cancellation property which is Proposition 3.3 here (and which I learned from Mathieu Anel).

Jonas Frey (Dec 04 2023 at 21:41):

So to me it seems like we get a square of monadic functors "almost always", and to find a counterexample we'd have to look at categories with very few colimits. Does anybody know a counterexample?

Jonas Frey (Dec 04 2023 at 21:44):

In particular, I think that the cancellation property for monadic functors implies that for every morphism $L\to M$ of Lawvere theories the induced adjunction between L-models and M-models is monadic, which gives a large class of "composable" monadic functors, including everything in this square:

$$\begin{matrix} Ring & \to & Mon \\ \downarrow & & \downarrow \\ Ab &\to & Set \end{matrix}$$

Mike Shulman (Dec 04 2023 at 23:30):

Jonas Frey said:

So to me it seems like we get a square of monadic functors "almost always", and to find a counterexample we'd have to look at categories with very few colimits.

Nice observation. I can't think of a counterexample offhand, but note that it could still happen that $\mathbb{C}$ has lots of colimits, as long as $\Sigma L$ doesn't preserve them so that they don't lift to $\mathbb{C}^{\Sigma L}$.

Jonas Frey (Dec 05 2023 at 01:15):

Mike Shulman said:

Jonas Frey said:

So to me it seems like we get a square of monadic functors "almost always", and to find a counterexample we'd have to look at categories with very few colimits.

Nice observation. I can't think of a counterexample offhand, but note that it could still happen that $\mathbb{C}$ has lots of colimits, as long as $\Sigma L$ doesn't preserve them so that they don't lift to $\mathbb{C}^{\Sigma L}$.

Ahh right, over base categories other than Set, cocompleteness is not automatically inherited by the algebras (see here)

Tom Hirschowitz (Dec 05 2023 at 06:48):

Mike Shulman said:

Jonas Frey said:

So to me it seems like we get a square of monadic functors "almost always", and to find a counterexample we'd have to look at categories with very few colimits.

Nice observation. I can't think of a counterexample offhand, but note that it could still happen that $\mathbb{C}$ has lots of colimits, as long as $\Sigma L$ doesn't preserve them so that they don't lift to $\mathbb{C}^{\Sigma L}$.

Sorry, not following: where is preservation of colimits involved in @Jonas Frey's proof?

Mike Shulman (Dec 05 2023 at 06:51):

The adjoint lifting theorem requires $\mathbb{C}^{\Sigma L}$ to have certain coequalizers. Usually the way to show that a category of algebras for a monad has colimits is to show that the base category $\mathbb{C}$ has colimits and the monad preserves certain colimits.

Mike Shulman (Dec 05 2023 at 06:53):

The simplest version is if $\mathbb{C}$ has a certain kind of colimit and the monad $T$ preserves that colimit, then $\mathbb{C}^T$ also has that colimit. But you can do better than that, e.g. IIRC as soon as $T$ preserves reflexive coequalizers, if $\mathbb{C}$ is cocomplete then so is $\mathbb{C}^T$. And by a different argument, if $\mathbb{C}$ is not just cocomplete but locally presentable, and $T$ is accessible (preserves sufficiently-highly-filtered colimits), then $\mathbb{C}^T$ is also locally presentable and hence cocomplete.

Tom Hirschowitz (Dec 06 2023 at 06:43):

Ok, so you if I understand correctly, you meant to point out that the hypothesis is not so mild, right?

Jonas Frey (Dec 08 2023 at 00:51):

Tom Hirschowitz said:

Ok, so you if I understand correctly, you meant to point out that the hypothesis is not so mild, right?

Yes that's how I understood Mike's comment as well. In particular, it's not only a condition on the underlying category, but also on the monads.

Still, I'd like to see an explicit counterexample!

Mike Shulman (Dec 08 2023 at 01:25):

Well, it's still relatively mild. Most of the "naturally occurring" monads I can think of are either accessible or preserve reflexive coequalizers.

Mike Shulman (Dec 08 2023 at 01:26):

In fact I can't right now think of any example of a monad on a cocomplete category whose category of algebras is not also cocomplete. (I feel like this is the sort of thing I should know, but apparently I don't.)

Todd Trimble (Dec 08 2023 at 02:49):

Well, I couldn't have either; all I knew is where I'd look it up. An example where cocompleteness fails is given here; see their III.10. But it's not easy.

Jonas Frey (Dec 08 2023 at 02:51):

Hmm, their monad is on the category of "posets and isotonic maps". Is isotonic the same as monotone?

Todd Trimble (Dec 08 2023 at 03:04):

I believe so.

They also refer to some other counterexample due to Adamek.

Mike Shulman (Dec 08 2023 at 03:29):

That sure isn't easy. So I guess the question is, can one make an example like that arise from a distributive law?

Todd Trimble (Dec 18 2023 at 02:43):

Mike Shulman said:

In my head, the "default" is that the composite of two monadic functors should be monadic, and counterexamples like that are "pathological". I don't know whether that's justified though.

Just ran across this example from Toposes, Triples and Theories: the full inclusion of torsion-free abelian groups in abelian groups is reflective, hence monadic, but the composite

$\mathrm{TorFree} \hookrightarrow \mathsf{Ab} \overset{U}{\to} \mathsf{Set}$

is not monadic. I'm imagining that there could be plenty of examples that utilize reflective subcategories of categories monadic over $\mathsf{Set}$. For example, I'm guessing that commutative rings with no nonzero nilpotents, as a full subcategory of commutative rings, is not monadic over $\mathsf{Set}$.

Tom Hirschowitz (Dec 18 2023 at 07:50):

Until recently, I also thought of monadic functors not composing as pathological. But ongoing work with @Ambroise and my dad makes me perceive the phenomenon as a side effect of “type dependency”. I know it's probably unclear, but maybe the following example (found by Ambroise) will convey the idea.
It's like models of type theory with a universe and a decoding function, except you don't even need to index over contexts, you merely consider families.
The example is the composite

$$(U,\mathit{El})\text{-Fam} \to U\text{-Fam} \to \text{Fam}\rlap{,}$$

where

• $U\text{-Fam}$ denotes the category of families $X$ with a distinguished type $U \in X[0]$,
• $(U,\mathit{El})\text{-Fam}$ denotes the category of families $X$ with a distinguished type $U \in X[0]$, and a map $\textit{El}\colon X_U \to X[0]$.
  Both functors have left adjoints, and the monad induced by the composite is in fact the same as the one induced by $U\text{-Fam} \to \text{Fam}$: it maps any family $X$ to $X + \mathbf{y}_{[0]}$, i.e., $X$ with an extra type, say $U$. So its algebras are $U$-families, not $(U,\mathit{El})$-families.

Tom Hirschowitz (Dec 18 2023 at 07:52):

(The reason the “composite” monad does this is: the first left adjoint maps $X$ to $X + \mathbf{y}_{[0]}$; the second left adjoint throws in as many new types as there are elements in the fibre over $U$, i.e., in this case, none!)

Mike Shulman (Dec 18 2023 at 11:24):

Can you explain your notation? What is $X[0]$?

Tom Hirschowitz (Dec 18 2023 at 11:36):

Oh sorry: I'm thinking of families as presheaves over $[0] \to [1]$, so $X[0]$ denotes the set of “types” of a family $X$, and $X[1]$ denotes its set of terms. Additionally, I'm writing $X_A$ for the fibre of $X$ over any $A \in X[0]$. Does this help?

Tom Hirschowitz (Dec 18 2023 at 11:37):

And of course $𝐲_{[0]}$ denotes the family with just one type.

Mike Shulman (Dec 18 2023 at 11:50):

Oh, I see -- mixing "indexed" and "fibered" notation.

Tom Hirschowitz (Dec 18 2023 at 13:31):

Huh, you're right, hadn't noticed this, thanks.

Todd Trimble (Dec 18 2023 at 14:48):

So the commonality between Tom's example and the one I gave can be abstracted like this: if $U_1, U_2$ in

$C \overset{U_1}{\to} D \overset{U_2}{\to} E$

are monadic, with left adjoints $F_1, F_2$ respectively, and if the unit map $\eta_1 F_2: F_2 \to U_1 F_1 F_2$ is an isomorphism, then the monads $(U_2 U_1) (F_1 F_2)$ and $U_2 F_2$ on $E$ are isomorphic, so that $U_2 U_1$ is monadic only when $U_1$ is an equivalence.

In Tom's example, the map $\eta_1 F_2: F_2 \to U_1 F_1 F_2$ is an isomorphism essentially because the fiber $y_{[0]}(1)$ over $y_{[0]}(0)$ is empty. In the example of torsion-free abelian groups, it's an isomorphism because free abelian groups have the property of being torsion-free. (This sort of example can be multiplied at will, by finding suitable "reflective" properties satisfied by free algebras of whatever ilk.)

Mike Shulman (Dec 18 2023 at 14:50):

Nice examples both of you, thanks. I may have to change my intuition.

Mike Shulman (Dec 18 2023 at 14:51):

Can anyone give an example of a non-monadic composite of monadic functors where the monad induced by the composite adjunction doesn't coincide with the one induced by the second factor?

Todd Trimble (Dec 18 2023 at 15:29):

Just a quick note that the famous pair of monadic functors, one the forgetful functor from categories to reflexive graphs, the other the edge functor from reflexive graphs to sets, doesn't give an example that Mike wants. (The free reflexive graph on a set $X$ is an $X$-indexed copower of copies of the reflexive graph $\mathbf{2}$, and the free category on that is an $X$-indexed copower of the category $\mathbf{2}$, so we're in the situation of $\eta_1 F_2$ being an iso.)

Todd Trimble (Dec 20 2023 at 03:37):

I went ahead and posted Mike's question to MathOverflow.

Todd Trimble (Dec 20 2023 at 12:05):

And got an answer from Sridhar Ramesh, which works: consider torsionfree abelian groups as a reflective subcategory of just groups, followed by the forgetful functor from groups to sets. On the one hand we get the free group monad, and on the other we get the free abelian group monad (where free abelian groups are in fact torsionfree).

Mike Shulman (Dec 20 2023 at 23:00):

This example (and others like it) has the interesting property that it's "just one step beyond trivial": we have monadic functors $G$ and $F$ such that $GF$ is not monadic, but we have a factorization $F = KH$ such that $H$, $K$, and $GK$ are monadic.

Mike Shulman (Dec 20 2023 at 23:02):

And the non-monadic composite $GK \circ H$ of monadic functors is "trivial" in that it induces the same monad as $GK$.

Mike Shulman (Dec 20 2023 at 23:07):

But @Jonas Frey suggested a different counterexample in a comment which doesn't seem to have even this property: categories over quivers over $\rm Set\times Set$.

Mike Shulman (Dec 20 2023 at 23:08):

I guess I need to update my intuition!

Tom Hirschowitz (Dec 21 2023 at 07:17):

I didn't take the time to think about it, but in which way are quivers monadic over $𝐒𝐞𝐭 × 𝐒𝐞𝐭$?

John Baez (Dec 21 2023 at 10:28):

A quiver $s,t: E \to V$ is a pair of sets with two functions from the first set to the second, and the forgetful functor sending $s,t: E \to V$ to $(E,V) \in \mathsf{Set} \times \mathsf{Set}$ is monadic.

Nathanael Arkor (Dec 21 2023 at 12:11):

One simple way to see this is that the forgetful functor from graphs/quivers to pairs of sets is given by the reindexing functor between presheaf categories induced by the inclusion of $\{ 0, 1 \}$ into $\{ 0 \rightrightarrows 1 \}$. Since the inclusion is bijective-on-objects, the reindexing functor is monadic.

James Deikun (Dec 21 2023 at 15:04):

A pretty general example: take an essentially algebraic theory that is not monadic over any slice category $\mathsf{Set}/V$. However, its category of models is LFP, so there is some category $\mathcal{V}$ on objects $V$ so that the category of models is reflective in (hence monadic over) $\mathsf{Set}^{\mathcal{V}}$. Moreover by an argument similar to the above, $\mathsf{Set}^{\mathcal{V}}$ is monadic over $\mathsf{Set}/V$.

The composite of the reflection and depresheafification is still a right adjoint and so induces a monad on $\mathsf{Set}/V$. The free presheaves are the small coproducts of representables. There is a set of generating anodyne morphisms for the reflector. We can assume because of how the reflector was constructed that if an anodyne morphism's domain lies over a representable there is already a unique lift within that representable, so if all the generating anodyne morphisms have domains that don't split into coproducts, we have the "trivial" situation. Among other things, this means the theory doesn't have constants, and all totally-defined operations are unary. An example is the theory of categories.

James Deikun (Dec 21 2023 at 15:07):

Jonas Frey's example avoids being trivial by refactoring the monads so that the totally-defined, unary operation of identity lives along with the reflector. You can do this because in the essentially algebraic theory of categories the identity operation is not used to define the domain of any operation or equation.

Tom Hirschowitz (Dec 21 2023 at 15:18):

@James Deikun this looks interesting, but I can't follow. Would you please mind breaking it up a bit?

Regarding monadicity of graphs over pairs of sets, for the record: concretely, the monad given by left extension followed by restriction maps any pair $(V,E)$, to $(V+E+E,E)$, and an algebra structure amounts to a pair of maps $E \to V$. The intuitive reason the monad does this is that the left adjoint maps $(0,1)$ to the smallest graph with one edge, i.e., the walking edge, which has two vertices. Hence the monad maps $(0,1)$ to $(2,1)$. The rest should be easy. Didn't know about that one, thanks @Jonas Frey, and @John Baez and @Nathanael Arkor for your help.

James Deikun (Dec 21 2023 at 15:27):

In general I think you can, for any presentation of an EAT on sorts $V$, factor the forgetful functor into monadic functors forgetting one equation or operation at a time to $\mathsf{Set}/V$ along any linearization of its dependency graph, and all the compositions where no "domain dependency" is included will be monadic. Being "trivially non-monadic" depends on:

• breaking the EAT into two pieces which have "domain dependencies" on each other but not within themselves, such that
• every operation and equation of theory 2 has as its "guard" a conjunction of equations at least one of which is independent of theory 1's equations.

Todd Trimble (Dec 21 2023 at 15:31):

James, that's a really cool class of examples -- I'll have to remember that. Of course, $Cat$ is a paradigmatic example.

Tom Hirschowitz (Dec 21 2023 at 15:39):

Oooooh, I think I more or less get the point, very nice, thanks. Am I right that this is fleshing out the vague intuition I mentioned before?

James Deikun (Dec 21 2023 at 15:46):

For example, the EAT of categories on one sort (arrows), has the operations of source/target (no conditions) and the operation $f \circ g$ $f \circ g [sf = tg]$, and the equations $ssf = sf, stf = tf, tsf = sf, ttf = tf, f \circ sf = f, tf \circ f = f, t(f \circ g) = tf [sf = tg], s(f \circ g) = sg [sf = tg], (f \circ g) \circ h = f \circ (g \circ h) [sf = tg \wedge sg = th]$. If you break these into things involving $\circ$ and things not involving it, you get basically the kind of division I mentioned, although there's something I guess I missed: if you can prove an instance of a "guard" for a new operation you can rectify the situation by equating the result to something that doesn't involve the new operations, c.f. $tf \circ f = f$, which rectifies the equation $stf = tf$, an instance of $sf = tg$ that enables you to write $tf \circ f$ in the first place.

James Deikun (Dec 21 2023 at 15:49):

And yeah, this can be considered a more formal rendering of the intuition that it is "type dependency" that breaks the composition of monadic functors.

James Deikun (Dec 21 2023 at 15:53):

Basically: a forgetful functor can be monadic if structure or properties it forgets depend on structure or properties that it remembers, but not if it forgets something dependent on something else it also forgot!

James Deikun (Dec 21 2023 at 16:00):

Torsion-free Abelian groups also fall into this framework. The theory of torsion-free Abelian groups includes three operations: $0, +, -$ with no conditions, various equations with no conditions, and an infinite series of equations with conditions: $x = 0 [0 = x + x + ... + x \text{(p times)}]$ for all primes $p$. If you divide the conditional equations separate from everything else, you have the standard "trivial" version of this example; if you divide it in other ways like putting $-$ and its equations, or the commutative law, or both, together with the conditional equations you can get non-trivial examples. You can even put together associativity with the conditional equations and you should still get something monadic, but you need Theory 1 to be at least the theory of a pointed magma or the full theory will not be monadic over Theory 1.

James Deikun (Dec 21 2023 at 16:16):

And I would say the intuition should be that monadic functors failing to compose is not "pathological" at all; when $U \circ U'$ is monadic it is because $U$ is somehow ignoring everything about its target category that $U'$ forgets.

James Deikun (Dec 21 2023 at 16:24):

My intuition is also that Cartesian and weakly Cartesian monadic functors compose much better, because they come from kinds of operads and my intuition is that conditional operations and equations are generalized contraction, but as of yet I have less to back up this part.

James Deikun (Dec 21 2023 at 18:45):

Let's make the idea of "ignoring everything" more precise: Say you have a monad $T$ on $\mathcal{C}$ and another monad $T'$ on $\mathcal{C}^T$. I maintain there is a proper "composite monad" $T' \cdot T$ whose monadic adjunction is the composition of $T'$'s and $T$'s iff $T'$ has arities $F_T$.

James Deikun (Dec 21 2023 at 18:46):

Say $T'$ does have such arities. Then for $X$ in $\mathcal{C}^T$ consider the large canonical diagram for $F_T$ over $X$. It is shaped like the comma category $F_T \downarrow X$ which is isomorphic to $\mathcal{C} / U_T X$. The diagram itself is the composition of the forgetful functor from this slice and $F_T$. If we further compose it with $T'$ and $Y \mapsto \mathcal{C}^T(F_T -,Y)$, we get a diagram that looks like $f \mapsto \mathcal{C}^T(F_T -,T'(F_T(\mathrm{dom} \; f)))$ or in other words $f \mapsto \mathcal{C}(-,(U_T \circ T' \circ F_T) (\mathrm{dom} \; f))$ and its colimit must be $\mathcal{C}(-,(U_T \circ T') X)$.

Nathanael Arkor (Dec 21 2023 at 19:57):

James Deikun said:

Let's make the idea of "ignoring everything" more precise: Say you have a monad $T$ on $\mathcal{C}$ and another monad $T'$ on $\mathcal{C}^T$. I maintain there is a proper "composite monad" $T' \cdot T$ whose monadic adjunction is the composition of $T'$'s and $T$'s iff $T'$ has arities $F_T$.

I believe this is essentially (a consequence of) Theorem 5.5 in Relative monadicity (though phrased, more generally, in terms of relative monads rather than monads with arities).

James Deikun (Dec 21 2023 at 19:57):

I hope so, since it saves me finishing this proof!

Nathanael Arkor (Dec 21 2023 at 20:02):

James Deikun said:

In general I think you can, for any presentation of an EAT on sorts $V$, factor the forgetful functor into monadic functors forgetting one equation or operation at a time to $\mathsf{Set}/V$ along any linearization of its dependency graph, and all the compositions where no "domain dependency" is included will be monadic. Being "trivially non-monadic" depends on:

• breaking the EAT into two pieces which have "domain dependencies" on each other but not within themselves, such that
• every operation and equation of theory 2 has as its "guard" a conjunction of equations at least one of which is independent of theory 1's equations.

This intuition is somewhat present in the result that the category of models for an essentially algebraic theory is "essentially monadic", i.e. there exists a (possibly infinite) chain of monadic functors from the category of models to (a power of) the category of sets, e.g. as proven in the one-sorted case in Essentially equational categories. However, I think the perspective via type dependency, and using this as an illustration of the failure of monadic functors to compose is very nice (and probably more naturally suited to generalised algebraic theories than essentially algebraic theories).

Nathanael Arkor (Dec 21 2023 at 20:04):

To be honest, I think this would make for a nice expository note since, as is clear from this discussion, it is a topic that many people do not have a good intuition for.

James Deikun (Dec 21 2023 at 20:36):

The tight connection between monads with arities and relative monads also deserves to be more widely known.

Mike Shulman (Dec 21 2023 at 20:38):

This all sounds really interesting and worthy of some more detailed explanation. Maybe someone could write a blog post? (-:

Nathanael Arkor (Dec 21 2023 at 20:38):

James Deikun said:

The tight connection between monads with arities and relative monads also deserves to be more widely known.

@Dylan McDermott and I will explicate this connection in a forthcoming paper.

Nathanael Arkor (Dec 21 2023 at 20:41):

But it is at least alluded to in Monads need not be endofunctors that the notion of monad with arities $j$ corresponds precisely to the notion of $j$-relative monad (conversely, relative monads are more general, as they require no assumptions on $j$).

James Deikun (Dec 21 2023 at 20:45):

Ah, under "Related Work":

Berger et al. [10, 16] have introduced a generalization of finitary monads, called monads with arities. Monads with arities constitute a special case of relative monads on well-behaved functors.

I guess I simply learned these concepts in the wrong order! :big_smile:

James Deikun (Dec 21 2023 at 22:15):

Connecting this back to the crude monadicity theorem: if a right adjoint functor preserves reflexive coequalizers, then the monad induced by it preserves the standard presentations of algebras for any other monad whose category of algebras it lives on. Now, you can view the elements of $TX$ as the operations of arity $X$ up to the equations of arity $X$. If $X$ preserves the standard presentations, then the operations of any non-free arity are completely determined by the ones on free arities up to the direct consequences of the arity's defining equations. So no matter what monad you use to gin up the base category of $T$, $T$ will still have arities in free objects.

James Deikun (Dec 21 2023 at 22:55):

And just throwing in more ingredients: Using the [[adjoint lifting theorem]] previously mentioned, say we have reflexive coequalizers in $(\mathcal{C}^T)^{T'}$, and we have the wannabe-composite monad $T'' = U_T \circ T' \circ F_T$, then the comparison functor from $U_T \circ U_{T'}$ to $U_{T''}$ is monadic. We can further show using the cancellation property that as soon as $U_{T''}$ factors through $U_T$ the factor is monadic. (Does it always factor? I think so, but I can't immediately think of an argument.) So now we have a situation:

$$\begin{CD} (\mathcal{C}^T)^{T'} @>{U_{T'_{\mathrm{nonfree}}}}>> \mathcal{C}^{T''} @>{U_{T'_{\mathrm{free}}}}>> \mathcal{C}^{T} @>{U_T}>> \mathcal{C} \end{CD}$$

where each arrow shown is monadic.

James Deikun (Dec 21 2023 at 23:01):

In the cases where this works, it gives a factorization so that the composition of the leftmost arrow above with the (monadic) composite of the two others is non-monadic in the "trivial" way. Perhaps this is why we get a lot of real-world examples that are "trivial" even though generically speaking it doesn't happen.

Nathanael Arkor (Dec 22 2023 at 15:11):

James Deikun said:

In general I think you can, for any presentation of an EAT on sorts $V$, factor the forgetful functor into monadic functors forgetting one equation or operation at a time to $\mathsf{Set}/V$ along any linearization of its dependency graph, and all the compositions where no "domain dependency" is included will be monadic.

In the setting of algebraic theories, one can formalise the notion of "forgetting operations/equations" by morphisms of algebraic theories (one could restrict specifically to the monomorphisms, but I think this is unnecessary for the problem at hand). Every morphism $T \to T'$ induces a monadic functor $\mathrm{Alg}(T') \to \mathrm{Alg}(T)$ and, in particular, the monadicity of each category of algebras is exhibited by unique morphism from the initial algebraic theory, whose category of algebras is the category of sets.

I wonder whether one can formalise this intuition about the (non-)composition of monadic functors in a similar way. For instance, we can consider a category of generalised algebraic theories, in which the objects comprise pairs $(S, P)$ where $S$ denotes a category of sorts, encoding the dependency structure, and $P$ denotes an $S$-sorted presentation of a generalised algebraic theory. The morphisms are the usual translations of generalised algebraic theories. Now, it seems natural to imagine that this category is equipped with a factorisation system, in which each morphism factors as one that is trivial on the $S$ component, followed by one that is trivial on the $P$ component. Then, while it is not true that each morphism of GATs induces a monadic functor between categories of algebras, perhaps it is true that each morphism in these two subcategories induces a monadic functor (furthermore functorially). In particular, if we factorise the unique morphism from the initial GAT to any given GAT, this would give a factorisation of the forgetful functor from the category of algebras to a power/slice of Set, into two monadic functors, which aligns with the factorisation induced by the presentation of a locally presentable category as a localisation of a presheaf category. (I should say that I'm thinking aloud, without checking anything, so this may not be at all accurate.)

Sridhar Ramesh (Dec 23 2023 at 23:03):

James Deikun said:

We can further show using the cancellation property that as soon as $U_{T''}$ factors through $U_T$ the factor is monadic. (Does it always factor? I think so, but I can't immediately think of an argument.)

We have a monad morphism from $T = U_T \circ F_T$ to $T'' = U_T \circ U_{T'} \circ F_{T'} \circ F_T$, given by the whiskering $U_T \circ \eta_{T'} \circ F_T$.

This monad morphism induces accordingly a functor from $C^{T''}$ to $C^T$, whose action on objects is given by precomposing any $T''$-algebra $T'' x \to x$ with the corresponding map $T x \to T''x$ (and similarly acting on morphisms by precomposing naturality squares, so to speak). This is as in Remark 3.4 at https://ncatlab.org/nlab/show/monad.

This should provide the appropriate factorization to make the following commutative diagram (where the bottom triangle commutes by the functor we just described leaving underlying carriers of algebras and of algebra morphisms unchanged):

https://q.uiver.app/#q=WzAsNCxbMiwyLCJDIl0sWzIsMCwiQ15UIl0sWzAsMCwiKENeVClee1QnfSJdLFswLDIsIkNee1QnJ30gPSBDXntVX1QgVV97VCd9IEZfe1QnfSBGX1R9Il0sWzIsMSwiVV97VCd9Il0sWzEsMCwiVV9UIl0sWzMsMCwiVV97VCcnfSIsMl0sWzMsMV0sWzIsMywiY29tcGFyaXNvbiIsMl1d

(I don't seem to know how to get Quiver/tikz-cd diagrams to render here on Zulip)

Keep in mind, nothing in this post depends on the presumption of reflexive coequalizers, merely the setup of having two composable monadic functors.

Sridhar Ramesh (Dec 24 2023 at 20:54):

Indeed, we get these same commutative triangles even if we take $U_{T'}$ to be any right adjoint, not necessarily monadic.

Nathanael Arkor (Dec 24 2023 at 21:04):

(I don't seem to know how to get Quiver/tikz-cd diagrams to render here on Zulip)

(I don't think it's possible: I usually just take a screenshot of the diagram in quiver, and paste it, with a link to the diagram.)

James Deikun (Dec 27 2023 at 19:04):

Sridhar Ramesh said:

James Deikun said:

We can further show using the cancellation property that as soon as $U_{T''}$ factors through $U_T$ the factor is monadic. (Does it always factor? I think so, but I can't immediately think of an argument.)

We have a monad morphism from $T = U_T \circ F_T$ to $T'' = U_T \circ U_{T'} \circ F_{T'} \circ F_T$, given by the whiskering $U_T \eta_{T'} F_T$.

This monad morphism induces accordingly a functor from $C^{T''}$ to $C^T$, whose action on objects is given by precomposing any $T''$-algebra $T'' x \to x$ with the corresponding map $T x \to T''x$ (and similarly acting on morphisms by precomposing naturality squares, so to speak). This is as in Remark 3.4 at https://ncatlab.org/nlab/show/monad.

Thanks! I figured out later that the map existed, but not that it came from a monad morphism, so I'm glad I didn't update right away.

James Deikun (Dec 27 2023 at 19:10):

Circling back to the original question, say you have two monads $\Pi$ and $\Sigma$ and $\Pi$ distributes over $\Sigma$. You get a monad $\Sigma^{\Pi}$ on $\mathcal{C}^{\Sigma}$ that is a lift of $\Sigma$ through $U^{\Pi}$ and factors $\Sigma\Pi$ monadically, that's the normal thing. But you also get, by duality, a monad $\Pi_{\Sigma}$ on $\mathcal{C}_{\Sigma}$ that is an extension of $\Pi$ through $F_{\Sigma}$.

James Deikun (Dec 27 2023 at 19:19):

In $\mathrm{Cat}$ and sufficiently similar equipments, there is an inclusion functor from $\mathcal{C}_{\Sigma}$ to $\mathcal{C}^{\Sigma}$ which is fully faithful and dense and factors $F^{\Sigma}$ through $F_{\Sigma}$, call this one $J_{\Sigma}$. Treating $\Pi_{\Sigma}$ as a relative monad, you can extend it through this to get a relative monad $J_{\Sigma}\Pi_{\Sigma}$ over $J_{\Sigma}$. Because it has a dense root, this relative monad extends to a monad on $\mathcal{C}^{\Sigma}$ with arities in $J_{\Sigma}$, and with a little manipulation you can see it also has arities in $F^{\Sigma}$.

James Deikun (Dec 27 2023 at 19:30):

Thanks to that, and the facts unearthed earlier in the thread, the forgetful functor of new monad on $\mathcal{C}^{\Sigma}$ composes with $U^{\Sigma}$ to give a monadic functor. So let's figure out what the monad of the composition is. The new monad arose as $\mathrm{Lan}_{J_{\Sigma}} J_{\Sigma}\Pi_{\Sigma}$, which is a genuine extension. So the full monad is:

$$U^{\Sigma} (\mathrm{Lan}_{J_{\Sigma}} J_{\Sigma} \Pi_{\Sigma}) F^{\Sigma} = U^{\Sigma} (\mathrm{Lan}_{J_{\Sigma}} J_{\Sigma} \Pi_{\Sigma}) J_{\Sigma} F_{\Sigma} \\ = U^{\Sigma} J_{\Sigma} \Pi_{\Sigma} F_{\Sigma} = U^{\Sigma} J_{\Sigma} F_{\Sigma} \Pi = U^{\Sigma} F^{\Sigma} \Pi = \Sigma\Pi$$

James Deikun (Dec 27 2023 at 19:32):

So you actually do have a monadic square as above with no extra assumptions, and the monad on the "wrong side" actually is built from the two given monads in a (fairly) straightforward way!

Nathanael Arkor (Dec 29 2023 at 19:03):

There's something I'm not quite following in the above. If I'm understanding correctly, you're saying that there are two monads on $\mathcal C^\Sigma$: the lifting of $\Sigma$ and a monad with arities in $F^\Sigma$. We can consider the forgetful functors from the categories of algebras for both monads, and compose each with $U^\Sigma$. The induced monad in both cases is $\Sigma\Pi$. However, for the "monadic square" as in the original question, we want to consider a monad on $\mathcal C^\Pi$ to obtain the left/bottom path, rather than two monads on $\mathcal C^\Sigma$. Where does $\mathcal C^\Pi$ come into the picture?

Nathanael Arkor (Dec 29 2023 at 19:06):

Oh, maybe it's just a typo:
James Deikun said:

But you also get, by duality, a monad $\Pi_{\Sigma}$ on $\mathcal{C}_{\Sigma}$ that is an extension of $\Pi$ through $F_{\Sigma}$.

Presumably this should be a monad $\Pi_\Sigma$ on $\mathcal{C}_\Pi$ (and then the relative monad in the following paragraph has codomain $\mathcal{C}^\Pi$ and so on).

Nathanael Arkor (Dec 29 2023 at 19:09):

James Deikun said:

Because it has a dense root, this relative monad extends to a monad on $\mathcal{C}^{\Sigma}$ with arities in $J_{\Sigma}$

Usually, for relative monads to extend to monads, you need the root to be dense and for (sufficient) left extensions along the root to exist. I would have expected this to require some mild cocompleteness assumptions on $\mathcal C^\Pi$, but maybe you're deducing the existence of the monad differently to how I'm imagining?

Nathanael Arkor (Dec 29 2023 at 19:17):

I should have recalled this much earlier, but §3 of Beck's paper on distributive laws is very relevant to this discussion.
image.png

James Deikun (Dec 29 2023 at 21:24):

Nathanael Arkor said:

Oh, maybe it's just a typo:
James Deikun said:

But you also get, by duality, a monad $\Pi_{\Sigma}$ on $\mathcal{C}_{\Sigma}$ that is an extension of $\Pi$ through $F_{\Sigma}$.

Presumably this should be a monad $\Pi_\Sigma$ on $\mathcal{C}_\Pi$ (and then the relative monad in the following paragraph has codomain $\mathcal{C}^\Pi$ and so on).

Oh, actually it's the first monad that is on $\mathcal{C}^{\Pi}$. Edited.

James Deikun (Dec 29 2023 at 22:59):

Nathanael Arkor said:

Usually, for relative monads to extend to monads, you need the root to be dense and for (sufficient) left extensions along the root to exist. I would have expected this to require some mild cocompleteness assumptions on $\mathcal C^\Pi$, but maybe you're deducing the existence of the monad differently to how I'm imagining?

Ugh, you're right. Let's use Beck's formulation of the existence result because it's at least clearer about what colimits need to exist. You need the coequalizer of $\Sigma\Pi x$ and $\mu^\Sigma_{\Pi X} \circ \Sigma \delta_X : F^{\Sigma\Pi} \Sigma X \to F^{\Sigma\Pi} X$ to exist in $\mathcal{C}^{\Sigma\Pi}$ for every $\Sigma$-algebra $(X,x)$.

James Deikun (Dec 29 2023 at 23:03):

It's a reflexive coequalizer (equip it with $\Sigma\Pi\eta^\Sigma_X$).

James Deikun (Dec 30 2023 at 05:51):

(Also: they are respectively the Kleisli extensions of $\eta^{\Sigma\Pi}_X \circ x$ and $\Sigma\eta^{\Pi}_X$...)

Jonas Frey (Jan 15 2024 at 04:56):

Nathanael Arkor said:

James Deikun said:

In general I think you can, for any presentation of an EAT on sorts $V$, factor the forgetful functor into monadic functors forgetting one equation or operation at a time to $\mathsf{Set}/V$ along any linearization of its dependency graph, and all the compositions where no "domain dependency" is included will be monadic.

In the setting of algebraic theories, one can formalise the notion of "forgetting operations/equations" by morphisms of algebraic theories (one could restrict specifically to the monomorphisms, but I think this is unnecessary for the problem at hand). Every morphism $T \to T'$ induces a monadic functor $\mathrm{Alg}(T') \to \mathrm{Alg}(T)$ and, in particular, the monadicity of each category of algebras is exhibited by unique morphism from the initial algebraic theory, whose category of algebras is the category of sets.

I wonder whether one can formalise this intuition about the (non-)composition of monadic functors in a similar way. For instance, we can consider a category of generalised algebraic theories, in which the objects comprise pairs $(S, P)$ where $S$ denotes a category of sorts, encoding the dependency structure, and $P$ denotes an $S$-sorted presentation of a generalised algebraic theory. The morphisms are the usual translations of generalised algebraic theories. Now, it seems natural to imagine that this category is equipped with a factorisation system, in which each morphism factors as one that is trivial on the $S$ component, followed by one that is trivial on the $P$ component. Then, while it is not true that each morphism of GATs induces a monadic functor between categories of algebras, perhaps it is true that each morphism in these two subcategories induces a monadic functor (furthermore functorially). In particular, if we factorise the unique morphism from the initial GAT to any given GAT, this would give a factorisation of the forgetful functor from the category of algebras to a power/slice of Set, into two monadic functors, which aligns with the factorisation induced by the presentation of a locally presentable category as a localisation of a presheaf category. (I should say that I'm thinking aloud, without checking anything, so this may not be at all accurate.)

I've been exploring similar ideas with Mathieu Anel, representing GATs by [[clans]] (see also this), and trying to find a factorization system on the 2-category $Clan$ of clans, one of whose classes induces monadic adjunctions between the associated categories of algebras.

Jonas Frey (Jan 15 2024 at 04:56):

The 2-category $Clan$ contains both the 2-category $FP$ of finite-product categories, and the 2-category $FL$ of finite-limit categories as full sub-2-categories, and in $FP$, the class of essentially surjective (finite-product preserving) functors induces monadic adjunctions and is both the left class of a (pseudo) OFS (with fully ff functors on the right), and the right class of a (pseudo) WFS (generated by $1\to\mathsf{Fin}^{op}$). In $FL$, essentially surjective functors do not induce monadic functors anymore (a counterexample is the inclusion of the FL-theory of Sets into the FL-theory of torsion-free abelian groups), but the free FL-functor on the end-point inclusion
$cod: 1\to (0\to 1)$ of the interval category generates a WFS whose right class is monadic. Finally, on general clans, we haven't been able to find a non-trivial factorization with monadic maps on one side, but we have at least found a criterion on clan-maps that ensures monadicity of the induced forgetful functor between algebras, and is closed under composition: the condition is that the clan map $F:C\to D$ is Cauchy-surjective, and the induced functor $F^*:[D,Set]\to [C,Set]$ between functor categories reflects algebras (algebras are functors preserving the terminal object and pullbacks of display maps).

Nathanael Arkor (Jan 17 2024 at 09:40):

That does sound related. I think the crucial difference between the two perspectives is the distinction between essential surjectivity on objects (say, of a finitely complete category), and bijectivity between the sort-functions of a morphism (say, between essentially algebraic theories). In the setting of algebraic theories, essential surjectivity coincides with bijectivity of sort-functions, because the morphisms in the category do not affect the objects of the category. However, since this is no longer true for finitely complete categories, when one is generalising from algebraic theories to essentially algebraic theories (or similar), one must decide which notion is appropriate. (It could well be that both are interesting for different reasons.)

Nathanael Arkor (Jan 17 2024 at 09:44):

(In fact, the reason I described an approach using presentations, rather than a presentation-free approach like categories with display maps, is that it is much simpler to define what one means by "sort-preserving morphism" in that setting, which seemed crucial.)