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: colimits of Lawvere theories

fosco (Aug 31 2022 at 14:42):

The category of Lawvere theories is cocomplete, and in fact locally finitely presentable. However, I cannot find an explicit description of how to construct colimits in it. In particular, even in the case of finite coproducts, I have trouble describing $L+L'$ for two Lawvere theories $p,q:Fin^o \to L, L'$.

Since one can define the category of Lawvere theories starting from the coslice $Fin^o/Cat$ I can imagine the coproduct $p+q$ is the pushout of $p,q$ along $Fin^o$ ($p,q$ are bijective on objects and this property is still true for the pushout $Fin^o \to L+_{Fin^o}L'$...)

But what if instead I wanted to describe the coproduct of finitary monads on $Set$? The pointwise coproduct of two monads is not even a monad...

fosco (Aug 31 2022 at 16:04):

Ah! Consider the coproduct of the underlying endofunctors of two monads $T,S$; is the free monad on the endofunctor $T+S$ the monad I am looking for?

Mike Shulman (Aug 31 2022 at 16:04):

No, that forgets all information about the monad structures on $T$ and $S$.

Mike Shulman (Aug 31 2022 at 16:05):

In general, colimits of monads don't admit explicit descriptions, but have to be constructed by some kind of iterative procedure like a [[transfinite construction of free algebras]].

fosco (Aug 31 2022 at 16:10):

Is it that difficult even with binary coproducts?

fosco (Aug 31 2022 at 16:13):

If not the free monad on $T+S$, my other candidate would have been something like the coproduct of all $S^{n_1}T^{m_1}\dots S^{n_r}T^{m_r}$ where one uses the multiplication of the two monads to "reduce" from $S^k$ to $S$ and $T^h$ to $T$

fosco (Aug 31 2022 at 16:15):

I can try to be more precise, but I need a concrete example: fix a set $A$ and $STT(A)$; "terms" $x$ of type $STTA$ can be sent to $S\mu_A^T(x) \in STA$

fosco (Aug 31 2022 at 16:17):

similarly with iterated compositions of multiplications you can pass from $S^2T^3S^2TA$ to $STSTA$ and from $T^4S^5T^2S^3A$ to $TSTSA$, etc

Mike Shulman (Aug 31 2022 at 16:20):

A coproduct isn't going to cut it, you need some kind of quotient to take account of the monad structures on $S$ and $T$.

fosco (Aug 31 2022 at 16:26):

Indeed! That's why I was trying to use the monad structure of $T,S$ reducing "words"

fosco (Aug 31 2022 at 16:26):

I'm trying to abstract from how you build a coproduct of monoids, but maybe too naively?

Mike Shulman (Aug 31 2022 at 16:26):

How do you build a coproduct of monoids?

Mike Shulman (Aug 31 2022 at 16:26):

I'm pretty sure there is a quotient there too.

fosco (Aug 31 2022 at 16:27):

words in te underlying sets, modulo reduction where contiguous elements from the same monoid are multiplied, and identities are canceled

Mike Shulman (Aug 31 2022 at 16:29):

Exactly. "Modulo" is a quotient.

fosco (Aug 31 2022 at 16:29):

Exactly!

fosco (Aug 31 2022 at 16:29):

I don't see where we disagree :smile:

Mike Shulman (Aug 31 2022 at 16:30):

Oh, so when you said "the coproduct of all $S^{n_1}T^{m_1}\dots S^{n_r}T^{m_r}$" you mean "the quotient of the coproduct..."?

fosco (Aug 31 2022 at 16:31):

Yes, I worded it in a confusing way probably

fosco (Aug 31 2022 at 16:32):

What I mean is the coproduct of all such things, modulo the fact that $\mu^T,\mu^S$ allow to "reduce terms" from (e.g.) $S^3T^2A$ to $STA$

fosco (Aug 31 2022 at 16:33):

by the monad law $\mu^T \circ$ {something obtained whiskering $\mu^T$ and $T$} is the same arrow for all choices of something

fosco (Aug 31 2022 at 16:34):

so you have only one way to descend from $S^3T^2A$ to $STA$ and you coequalize it? I'm writing the idea without checking if it's true, because I have an intuition that I'd like to make more precise

fosco (Aug 31 2022 at 16:34):

well, it doesn't make sense to coequalize it if there's only one map

Ralph Sarkis (Aug 31 2022 at 16:38):

Do you have an intuition for what algebras of $T+S$ should be?

fosco (Aug 31 2022 at 16:39):

At the level of Lawvere theories, yes; a model of $L+L'$ is a set that is both a L-structure and a L'-structure

fosco (Aug 31 2022 at 16:44):

So, it seems to me that there are at least two non-equal maps $S^3T^2A\to STA$, and now the naive idea would be to coequalize them

Mike Shulman (Aug 31 2022 at 16:45):

More generally, you want colimits of monads to be algebraic colimits.

Mike Shulman (Aug 31 2022 at 16:49):

It's possible that some construction like that would work if your monads preserve enough colimits. The main difference between free monads and free ordinary monoids is that ordinary monoids are defined with respect to the monoidal structure of cartesian product of sets, which preserves all colimits in each variable, whereas free monads are defined with respect to the monoidal structure of endofunctor composition, which preserves all colimits in the left variable but only those colimits in the right variable that are preserved by the monads themselves qua functors. Generally we assume our monads to be accessible, or even finitary, which means that they preserve filtered colimits but not arbitrary ones (and in particular, not coequalizers). So you need to express the construction of free monads in such a way that preservation of filtered colimits suffices, which usually means constructing it using primarily filtered colimits. That's what the construction at [[transfinite construction of free algebras]] does. Your approach may also work if you're sufficiently careful about phrasing it, and it might even turn out to be a $\beta$-reduced version of the former.

Amar Hadzihasanovic (Aug 31 2022 at 18:35):

Ghani and Uustalu gave some explicit formulas to compute coproducts of a special kind of monads on $\textbf{Set}$ called ideal monads. Basically an ideal monad is one where the image of the unit is “neatly separated” from its complement, in the sense that the monad multiplication never sends anything outside the image of the unit to the image of the unit.

Amar Hadzihasanovic (Aug 31 2022 at 18:38):

I think some of their results were generalised in this other paper but I am less familiar with it and the characterisations provided are somewhat less explicit (they are in the form of least solutions to some systems of equations of functors, if I remember correctly)

Tom Hirschowitz (Sep 01 2022 at 08:24):

Probably obvious to everyone here, but just in case: if both monads are free on some endofunctors, say $F$ and $G$, then you do have a formula: $(F+G)^*$.

fosco (Sep 01 2022 at 08:57):

Can a monad be free and finitary?

Dan Marsden (Sep 01 2022 at 09:19):

Any monad generated by a signature of operations and equations where the operations have finite arity is finitary. If you have no equations, such a functor is equivalent to the free functor generated by a polynomial functor. So there's lots, if I've understood the question? A concrete example would be the exception monad.

fosco (Sep 01 2022 at 09:33):

so.. is the monad of magmas (just a binary operation, no eqns) a free monad? (I'm sorry if the question sounds dumb, I know very little about free monads!)

Dan Marsden (Sep 01 2022 at 09:45):

Yes, that's correct. For an endofunctor F, if the forgetful functor R from the category of F-algebras to the base category has a left adjoint L, then the resulting monad RL is the free monad over F. If the base category is complete, then all free monads essentially arise this way. This is a more convenient way of describing free monads on categories such as Set than going via the standard definition. If F is a polynomial functor on Set, an F-algebra is a set with some finite operations and no equations, and in this case, the resulting monad is always finitary, via the correspondence with Lawvere theories.

Joe Moeller (Sep 01 2022 at 13:35):

Remember: no question is dumb in this stream! Relatedly, it's always good to say the thing that's probably obvious, because there's always someone lurking who doesn't know that obvious thing, but they don't even feel justified in asking.

fosco (Sep 01 2022 at 18:25):

That is a very clear way to put it, thanks!

fosco (Sep 01 2022 at 18:25):

(^ replying to @Dan Marsden )

fosco (Sep 01 2022 at 18:30):

yet, I still feel I'm far from grasping the problem at the core. I'd love to learn how to reason in this kind of situation and (for example) I'd like to see a computation done in detail and in a concrete case: take two Lawvere theories $L,L'$, and compute their coproduct when

1. $L$ is a "sub-theory" of $L'$, when every L-algebra is a particular kind of L'-algebra; for example when $L'$ is semigroups and $L$ is groups
2. $L$ and $L'$ are "very different" theories (something like, for example, magmas and [[convex spaces]]?)

Nathanael Arkor (Sep 01 2022 at 18:34):

As has been pointed out, describing colimits of algebraic theories is difficult. However, describing colimits of presentations of algebraic theories is easy: the coproduct is the presentation with the operations and equations of both presentations, and coequalisers are described by adjoining equations.

Nathanael Arkor (Sep 01 2022 at 18:35):

(Conversely, describing limits of presentations is difficult, but describing limits of algebraic theories is easy.)

fosco (Sep 01 2022 at 18:45):

Nathanael Arkor said:

As has been pointed out, describing colimits of algebraic theories is difficult. However, describing colimits of presentations of algebraic theories is easy: the coproduct is the presentation with the operations and equations of both presentations, and coequalisers are described by adjoining equations.

I understand

John Baez (Sep 01 2022 at 18:45):

I think somewhat concretely but also a wee bit vaguely we create the Lawvere theory $L + L'$ by taking all the operations of $L$, all the operations of $L'$, and letting them generate a huge wad of other operations while imposing no interesting relations except those that hold among operations of $L$ and those that hold among operations of $L'$.

John Baez (Sep 01 2022 at 18:46):

The vagueness is the word "interesting". There are some relations that automatically hold among any operations of any Lawvere theory and I'm calling those "uninteresting".

fosco (Sep 01 2022 at 18:46):

But I still would like to see a precise computation on the lines of "as complicated as it may be, the coproduct is the colimit of this huge diagram"

fosco (Sep 01 2022 at 18:47):

"good luck looking inside it, but at least you have a formula"

Mike Shulman (Sep 01 2022 at 18:48):

You should be able to extract a precise computation using colimits from the [[transfinite construction of free algebras]].

fosco (Sep 01 2022 at 18:49):

Yes. Yet, that's a notoriously difficult read, few people have command of its content and it is not written in a way that you can read it with a modular approach

John Baez (Sep 01 2022 at 18:50):

I can't help you with that colimit stuff, since that's not how I like to think about coproducts of Lawvere theories. In addition to the syntactic description of these coproducts I just sketched, there's the semantic description which is much nicer. For example if $L$ is the theory of monoids and $L'$ is the theory of real Lie algebras, an algebra of $L+L'$ (in Set) is a monoid that's also a real Lie algebra.

And the words "monoid" and "real Lie algebra" are irrelevant here: you can replace them with any other two gadgets that can be described as algebras of Lawvere theories.

John Baez (Sep 01 2022 at 18:52):

But in this example, we see an algebra $L + L'$ will be equipped with the operations of a monoid, obeying the monoid relations, and the operations of a real Lie algebra, obeying the real Lie algebra relations... and no other interesting relations.

John Baez (Sep 01 2022 at 18:53):

Anyway, if you find this stuff intuitive and obvious, you understand coproducts of Lawvere theories as well as I do so I can't help you further. :upside_down:

Mike Shulman (Sep 01 2022 at 18:53):

fosco said:

Yes. Yet, that's a notoriously difficult read, few people have command of its content and it is not written in a way that you can read it with a modular approach

I'm sad to hear that. All of those things are true about Kelly's original paper, but I'd hoped that the nLab page was an improvement. Can you suggest ways to make it more readable?

fosco (Sep 01 2022 at 18:59):

I wasn't talking about the nlab article, of course, I was talking about Kelly's paper.

I can suggest the following: you give me a more precise idea of how to adapt what I gather is Theorem 7.2 in the nlab page to my case, and I will type up an addition to the nlab: "As an example, let's compute the coproduct of finitary monads on Set in painstaking detail" :-) this way everybody wins

fosco (Sep 01 2022 at 19:00):

(you is a plural you, I didn't want to leave the entire burden on Mike)

Mike Shulman (Sep 01 2022 at 19:00):

What is currently imprecise that you need a more precise idea about?

fosco (Sep 01 2022 at 19:05):

and @John Baez yes, this looks relatively intuitive to me; I'm glad I understand coproducts as well as you do, but this gave me an idea to formulate my question more precisely:

A "lawvere theory" is any of the following gadgets

1. A bijective-on-objects, product preserving functor $p : Fin^o\to L$
2. A finitary monad on $Set$
3. A cartesian operad
4. A monoidal promonad on $Fin^o$, regarded as an object of the bicategory of profunctors
5. A left adjoint $T : [Fin,Set] \to [Fin,Set]$ which is strong monoidal with respect to the Day convolution product on $PSh(Fin^o)$

With appropriate definitions of morphisms of lawvere theories, each of these classes becomes a category, and they are all equivalent to each other.

They are, furthermore, all locally finitely presentable categories, so in particular they are all cocomplete.

I think I understand coproducts only in the first category: pushouts in the coslice $Fin^o/Cat$. So my question is:

Is it possible to describe "concretely" the coproduct operation in any of the other categories?

fosco (Sep 01 2022 at 19:10):

@Mike Shulman Nothing is unclear strictly speaking, I probably just feel a bit overwhelmed by all the symbols I'm seeing when I try to parse the page and I'd love someone to sit by my side and do the math with me.
But that's my problem and I don't want to impose on your patience. :smile:

I'll try alone tomorrow (it's night in my timezone) when $K$ in theorem 7.2 is discrete with two objects, and let's see how ugly the diagram becomes... pray for me!

Mike Shulman (Sep 01 2022 at 19:10):

In (1), don't you need to require that $p$ preserves finite products?

fosco (Sep 01 2022 at 19:11):

right, fixed (but now product preserving functors are not closed under pushout...?)

Mike Shulman (Sep 01 2022 at 19:11):

Right! So it's more complicated in (1) too.

fosco (Sep 01 2022 at 19:11):

The horror, the horror!

Mike Shulman (Sep 01 2022 at 19:12):

fosco said:

Nothing is unclear strictly speaking, I probably just feel a bit overwhelmed by all the symbols I'm seeing when I try to parse the page and I'd love someone to sit by my side and do the math with me.

Ok, that's fair. I've certainly felt that way myself when trying to learn something new. Good luck!

fosco (Sep 01 2022 at 19:13):

it's not even feeling baffled by something totally "new". It's just surprisingly intricate and difficult to prove stuff about Lawvere theories explicitly.

fosco (Sep 01 2022 at 19:14):

anyway :smile: thanks for your help!

John Baez (Sep 01 2022 at 22:02):

Is it possible to describe "concretely" the coproduct operation in any of the other categories?

I guess my approach is this: if I have a bunch of equivalent categories and I know a nice description of a construction (e.g. coproducts) in one, I declare myself satisfied unless I darn well need to transfer that description to one of the others. I.e. I don't go out of my way looking for trouble... at least not in this way.

John Baez (Sep 01 2022 at 22:10):

I like to say that in math it's good to get yourself into trouble if you know how to get back out of it.

John Baez (Sep 01 2022 at 22:11):

So it is good to have general heuristics for coming up with questions which you can answer in principle but may not know how to answer in practice.

John Baez (Sep 01 2022 at 22:12):

And computing co/limits in a category equivalent to some other category where you know how to compute those co/limits is a good example.

John Baez (Sep 01 2022 at 22:14):

Somehow this particular sort of challenge is not one that I've embraced. But luckily I know people who are good at this stuff.

Tom Hirschowitz (Sep 02 2022 at 07:43):

@fosco I reckon that specialising Theorem 7.2 to coproducts goes as follows.

• We use an additional category equivalent to your five ones above, the category of monadic functors over $\mathbf{Set}$.

• Your two monads, say $T$ and $T'$, correspond to two monadic functors, say $U\colon E \to \mathbf{Set}$ and $U'\colon E' \to \mathbf{Set}$.

• If the coproduct $T+T'$ exists, then taking the pullback in $\mathbf{CAT}$ of $U$ and $U'$, the diagonal is again monadic, and the induced monad is canonically isomorphic to $T+T'$.

• In particular, if both monads are accessible, then the coproduct exists, hence the pullback is monadic. Furthermore, the coproduct is again accessible.

(Is this right? It'd be nice if some real expert could confirm!)

fosco (Sep 02 2022 at 08:10):

Tom Hirschowitz said:

fosco I reckon that specialising Theorem 7.2 to coproducts goes as follows.

• We use an additional category equivalent to your five ones above, the category of monadic functors over $\mathbf{Set}$.

• Your two monads, say $T$ and $T'$, correspond to two monadic functors, say $U\colon E \to \mathbf{Set}$ and $U'\colon E' \to \mathbf{Set}$.

• If the coproduct $T+T'$ exists, then taking the pullback in $\mathbf{CAT}$ of $U$ and $U'$, the diagonal is again monadic, and the induced monad is canonically isomorphic to $T+T'$.

• In particular, if both monads are accessible, then the coproduct exists, hence the pullback is monadic. Furthermore, the coproduct is again accessible.

(Is this right? It'd be nice if some real expert could confirm!)

Thanks, this is another perspective I didn't think about!

fosco (Sep 02 2022 at 08:33):

@Mike Shulman now I see where the exposition in the page can be improved:

When speaking of colimits of monads, we are not interested merely in colimits in the category of monads, but algebraic colimits

I understand we do because they are better behaved, but in what sense precisely? And what does one lose in restricting colimits in this way? Also, I don't really understand what is the definition of a $V$-algebra: say $V : {\cal K}\to Mnd({\cal A})$ is a functor. Then a $V$-algebra should be an object $A$ of $\cal A$ with a structure of $V_k$-algebra for every monad $V_k$ image of $k$ under $V$, such that for every $\varphi : k\to k'$ in $\hom({\cal K})$ the $k'$-algebra $a_{k} : V_{k}A\to A$ results as the composition $V_kA \to V_{k'}A\to A$; in other words a $V$-algebra is an object $A\in\cal A$ equipped with a $V_k$-algebra structure $a_k : V_kA\to A$ for every $$k\in\cal K$, and such that these algebras are assigned "compatibly with reindexings", i.e. the functor $V_\varphi : V_{k'}\text{-Alg} \to V_k\text{-Alg}$ sends $a_{k'}$ to $a_k$. In other words, a $V$-algebra is a lifting $\bar V : {\cal K}\to \text{Alg}$ of $V : {\cal K}\to Mnd({\cal A})$ along the "fibration of algebras" $\begin{smallmatrix} \text{Alg} \\ \downarrow \\ Mnd({\cal A})\end{smallmatrix}$ such that the composition ${\cal K} \to \text{Alg} \to {\cal A}$ is the constant functor at $A$.

If all these equivalent descriptions are true i would be helpful to have them written.

Now, an algebraic colimit is meant to capture the idea that the colimit of $V : {\cal K}\to Mnd({\cal A})$ is the monad whose category of algebras is the category of $V$-algebras, and $V$-algebras are some sort of $\lim\big(V_k\text{-Alg}\big)$, so $\lim\big(V_k\text{-Alg}\big)\cong (\text{colim }V_k)\text{-Alg}$. (The condition that defines an object in $V$-algebras reminds me of a limit, you only consider algebras $a_k$ compatible with the morphisms in $\cal K$).

Is this correc? Too sloppy? This notion of colimit seems very rigid, are there interesting colimits of monads that are not algebraic?

fosco (Sep 02 2022 at 08:38):

@John Baez Indirect as it may be as a reply, my comment to Mike can show you what instead is my approach. Unless I'm able to answer these questions at this exact level of detail, in this order (informal intuition > formalization > computation without leaving holes) I don't feel I understood an idea. :smile:

fosco (Sep 02 2022 at 08:41):

(All the more because it doesn't seem that an explicit formula for the colimit is available in any of the categories I listed above...)

Tom Hirschowitz (Sep 02 2022 at 09:51):

Regarding algebraic colimits, I think this is indeed the idea, but it doesn't look rigid to me.
It is rather non-algebraic colimits that look pathological.

Indeed, on the "monadic functors" side of the equivalence, algebraic colimits are the limits (because the equivalence is contravariant) which are created by the forgetful functor $\mathbf{Monadic}/\mathbf{Set} \to \mathbf{CAT}/\mathbf{Set}$.

The limit in $\mathbf{CAT}/\mathbf{Set}$ is the $V$-alg of Theorem 7.2, and to me it is a natural candidate limit: a $V$-algebra is an object with a compatible family of algebra structures for each of the involved monads.

fosco (Sep 02 2022 at 09:53):

I see, thanks.

fosco (Sep 02 2022 at 10:00):

Now let's get to the coproduct of two finitary monads: I will try to rephrase the proof when $K \to Mnd$ is a discrete diagram...

Without loss of generality one can assume $K$ has an initial object, so instead of the coproduct of monads $T,S$ one can start considering the pushout of $T \leftarrow 1\to S$ in the category of pointed endofunctors. Let's call this pushout $H=T+_1 S$.

In this particular case an algebra for the diagram in question consists precisely of an object $A$ of the base category which is at the same time a $T$-algebra $a_T : TA \to A$ and an $S$-algebra $a_S : SA\to A$ (the compatibility with the morphisms $A\to TA, A\to SA$ is just one of the requirements for $a_T,a_S$ to be algebras for $T,S$ qua monads).

fosco (Sep 02 2022 at 10:06):

The next step of the proof is to show that these algebras are a reflective subcategory of $H/{\cal A}$. To build the reflection, the nlab considers the joint coequalizer of a certain family of maps; call $r_S,r_T$ respectively the coprojections into $H$, and then for every $(A,B,c:HA\to B)$ define a certain coequalizer of all paraller pairs [...]

I don't understand why these arrows are parallel, because they have different domains: in my case, it seems that the arrows boil down to be $TTA\xrightarrow{T(a.r_T)}TB\xrightarrow{r_T} HB$ and $SSA\xrightarrow{S(a.r_S)}SB\xrightarrow{r_S} HB$.

fosco (Sep 02 2022 at 10:08):

[No, this did not make sense.]

fosco (Sep 02 2022 at 10:13):

So here's a first point where I stop.

A second problem is: let's say I have built a reflection onto $V$-algebras. The next step is to invoke another theorem that through a transfinite construction builds the free monad on a certain pointed endofunctor, which (by yet another theorem) is going to be accessible.

fosco (Sep 02 2022 at 10:18):

All this line of reasoning is immensely laborious, scattered with small and big leaps of faith, mostly based on implicit constructions, and the whole discussion is held at a level of generality that I would define "counterproductive".

At this point, I accept this is not an easy question to solve at the level of detail I'd like; but I can probably turn this discussion into a more sociological one because this is an instance of a general phenomenon I've experienced through the years. My insistence in understanding this specific argument comes in large part from a concrete desire other than "evolve" a little bit my way of thinking categorically, and to -finally!- grok at least part of the content of Kelly's notoriously difficult paper.

fosco (Sep 02 2022 at 10:24):

So one problem is that I must confess that I simply can't follow this level of generality, and I'm asking for advice on how to address the issue. Or rather, I know how to address the issue, take baby steps, since the construction is so convoluted because it's very general, let's make it less general:

• instead of a generic domain category for the diagram $V : K \to Mnd({\cal A})$ let's consider a discrete category with two objects
• instead of a generic base category $\cal A$ let's consider $\bf Set$

The line of reasoning that works for every diagram must become a little bit simpler now, right? Yet I can't see how to simplify it, and in fact as it is written, the construction doesn't even typecheck

John Baez (Sep 02 2022 at 10:28):

fosco said:

John Baez Indirect as it may be as a reply, my comment to Mike can show you what instead is my approach. Unless I'm able to answer these questions at this exact level of detail, in this order (informal intuition > formalization > computation without leaving holes) I don't feel I understood an idea. :)

I have much lower standards for claiming to understand an idea in category theory - basically, just enough to limp by. I've always been mainly interested in applying category theory to physics and other external topics, so I try to avoid questions like how you compute colimits in some category until I absolutely need to answer them for some external reason. Luckily there are people like you who tackle such questions!

fosco (Sep 02 2022 at 10:35):

A second problem is purely sociological: I find the general attitude towards these questions a bit cavalier (I'm not talking about someone's behaviour specifically, let alone the participants to this conversation. It's a general attitude of category theorists, especially the brilliant ones, who tend to forget how difficult it is to enter their train of thoughts from a distance... Kelly and Freyd are the examples I have in mind, calling them brilliant would be an understatement, and yet reading them is often so, so painful).

perhaps Mac Lane's quote about the "right" level of generality should be amended saying that sometimes too much generality is very distracting: I entered this problem with a curiosity (and maybe a mild motivation in terms of a problem I'm trying to work on), and now I find myself I lost two days to penetrate an argument that is ten times more general than I need, and also badly exposed.

You're helping a lot, but this is annoying :grinning:

fosco (Sep 02 2022 at 10:41):

At this point I wonder, is there any chance that the "words-modulo-reduction" approach leads to something?

I can believe it is a very particular case of Kelly's and-so-on, but knowing this at the moment doesn't add anything to my understanding of the problem, and of the solution. Not to mention, other people might benefit from a different, more elementary point of view, since transfinite arguments in the "and-so-on" ballpark keep popping up from many disparate parts of CT.

fosco (Sep 02 2022 at 10:44):

John Baez said:

fosco said:

John Baez Indirect as it may be as a reply, my comment to Mike can show you what instead is my approach. Unless I'm able to answer these questions at this exact level of detail, in this order (informal intuition > formalization > computation without leaving holes) I don't feel I understood an idea. :smile:

I have much lower standards for claiming to understand an idea in category theory - basically, just enough to limp by. I've always been mainly interested in applying category theory to physics and other external topics, so I try to avoid questions like how you compute colimits in some category until I absolutely need to answer them for some external reason. Luckily there are people like you who tackle such questions!

My approach does not stem from overzealousness, and I often adopt also your point of view. But I believe "understanding" can be done at different scopes. My point is very simple: if trying to wrap your head around concept X you can't work out at least a couple of specific nontrivial examples of an X, what do you know about X and how can you use an X proficiently?

Zhen Lin Low (Sep 02 2022 at 11:05):

All this line of reasoning is immensely laborious, scattered with small and big leaps of faith, mostly based on implicit constructions, and the whole discussion is held at a level of generality that I would define "counterproductive".

When I was doing research I had similar frustrations. Eventually I found that I could make more progress by proving things myself than trying to read and digest the published proofs.

Zhen Lin Low (Sep 02 2022 at 11:08):

Regarding this particular matter of the coproduct of two Lawvere theories: I would prove it along the lines Tom suggests. It is easy to show that the pullback satisfies the conditions of Beck's monadicity theorem except for the existence of the left adjoint. Then I would use the theory of locally presentable categories to get the left adjoint. I'm not sure how I would prove that the result is locally _finitely_ presentable but I have no problem believing it to be true – because it is morally true when thinking from the syntactic perspective.

Morgan Rogers (he/him) (Sep 02 2022 at 11:23):

fosco said:

(All the more because it doesn't seem that an explicit formula for the colimit is available in any of the categories I listed above...)

I found myself experiencing frustration at the absence of explicit colimit computations in the category of categories with pullbacks/finite limits (and functors preserving these). This is still unresolved. I have a plan to make it more explicit, but it's firmly relegated to a backburner for now. I'll be curious to see if you come out with some answers for the finite products case which might make my life easier :grinning:

Zhen Lin Low (Sep 02 2022 at 11:42):

I vaguely recall hearing that the category of cartesian monoidal categories has biproducts...

Martti Karvonen (Sep 02 2022 at 12:13):

Zhen Lin Low said:

I vaguely recall hearing that the category of cartesian monoidal categories has biproducts...

The 2-category of symmetric monoidal categories has (2-categorical) biproducts as worked out in the appendix of this paper, and this restricts to cartesian monoidal categories just fine.

Morgan Rogers (he/him) (Sep 02 2022 at 19:07):

So the coproduct coincides with the product for @fosco 's problem?

Mike Shulman (Sep 02 2022 at 20:36):

@fosco Yes, your description of the $V$-algebras is right. Feel free to add that to the page! I think the notion of "algebraic colimit" is best regarded as a "niceness condition" that's satisfied by nearly all naturally-occurring colimits of monads. (Similar to how the "nice" limits and colimits in functor categories are pointwise -- it's possible for a functor category to have a non-pointwise limit or colimit in weird or pathological cases, if the codomain category is not (co)complete, but nearly always we mainly care about the pointwise ones.) In fact, I think the argument given here for algebraically-free monads should also apply to show that if the category is locally small and complete, then all small colimits of monads are algebraic colimits.

Mike Shulman (Sep 02 2022 at 20:41):

fosco said:

To build the reflection, the nlab considers the joint coequalizer of a certain family of maps; call $r_S,r_T$ respectively the coprojections into $H$, and then for every $(A,B,c:HA\to B)$ define a certain coequalizer of all paraller pairs [...]

I don't understand why these arrows are parallel, because they have different domains: in my case, it seems that the arrows boil down to be $TTA\xrightarrow{T(a.r_T)}TB\xrightarrow{r_T} HB$ and $SSA\xrightarrow{S(a.r_S)}SB\xrightarrow{r_S} HB$.

This is definitely a deficiency of the exposition: the phrase "joint coequalizer" is not defined. What it means is that you have two (or more) pairs of arrows, all with the same codomain, and so that the two arrows in each pair have the same domain, but the two pairs may have different domains. So in your case you have two arrows $TTA \rightrightarrows HB$ and two more arrows $SSA \rightrightarrows HB$. Then the "joint coequalizer" is the colimit of the diagram consisting of all four arrows.

Someone should write an nLab page [[joint coequalizer]]!

Mike Shulman (Sep 02 2022 at 20:43):

fosco said:

sometimes too much generality is very distracting

I'm reminded of John's remark that "category theorists are dual to ordinary people: they get confused if you surround a nice abstract concept with lots of distracting specifics." (-:O

Zhen Lin Low (Sep 02 2022 at 22:32):

Morgan Rogers (he/him) said:

So the coproduct coincides with the product for fosco 's problem?

Unfortunately, no. The coproduct for single-sorted Lawvere theories would be more closely related to the pushout under the initial Lawvere theory.

Morgan Rogers (he/him) (Sep 03 2022 at 11:40):

Ah right, it does make more sense that the colimit for luntisorted theories would be easier to compute, since then we're looking for separate models of the two theories rather than a single carrier of the structure coming from both theories...