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: why some initial algebras define monads?

fosco (Jul 12 2022 at 14:11):

Some initial algebras for endofunctors depend on a parameter object: for example, $List(A)$ is the initial algebra for the endofunctor $X\mapsto 1+A\times X$, and $Tree(A)$ (binary trees) is the initial algebra for $X\mapsto 1+A\times X^2$. In such cases, with just the universal property that defines them in terms of algebras, one can show that the assignments $A\mapsto List(A)$ or $A\mapsto Tree(A)$ are functors and in fact more is true, they are monads; my question is: why?

Is there a way to prove, using only the universal property that defines $List(A)$, that $A\mapsto List(A)$ is a monad?

And what about a more general question? Let $T_\bullet : {\cal E} \to [{\cal E},{\cal E}]$ be a functor: is there any known assumption on it so that $A\mapsto \text{fix}(T_A)$ (where $\text{fix}(T_A)$ is the initial algebra of $T_A$) is a monad on $\cal E$?

(Evidently the first question is motivated by the second: knowing nothing about the family of endofunctors $T_A$, I was looking for a formal way to see what in the shape of the functor $X\mapsto 1+A\times X$ makes $\text{fix}(T_\bullet)$ a monad.)

Certainly, you can construct $List(A)$ with the recipe that computes initial algebras, but this is not what I want, and I am clueless even when it comes to define the unit $\eta : A\to List(A)$, because the initiality property of $List(A)$ conflicts with the fact that $\eta$ must map into $List(A)$...

Nathanael Arkor (Jul 12 2022 at 15:42):

You may find some answers in Fiore–Saville's List Objects with Algebraic Structure. They mostly consider list-like structures, but the techniques they use are rather general.

fosco (Jul 12 2022 at 17:54):

I see that this is certainly relevant to my question, but skimming very rapidly it seems that the proof that $A\mapsto \mu A.(1+A\times X)$ is a monad is omitted...

fosco (Jul 12 2022 at 17:54):

...is it so obvious?

Mike Shulman (Jul 12 2022 at 18:15):

I doubt there's going to be any general answer to this. In a way it's sort of an accident that the free-monoid monad (for instance) can be presented as the initial algebra of an endofunctor -- you can think of it as a simple form of cut-elimination. Most monads involve some quotienting as well, to impose the axioms of the theory.

Mike Shulman (Jul 12 2022 at 18:16):

I realize you're asking the dual question, of when an initial algebra for a parametrized endofunctor happens to be a monad, but it seems to me like sort of the same thing.

Tobias Schmude (Jul 12 2022 at 20:54):

This question puts into words nicely why I'm not feeling quite comfortable with (parametrized) inductive types!
To me it smells like the transfinite construction of free algebras/monads should play a role here: the way the free monoid monad is generated from the endofunctors $X \mapsto 1 + A \times X$ is given by a special case of it (Adamek's theorem), and the construction of free algebras is also mentioned in the Fiore-Saville paper above (Example 3.5.). I can't connect the dots either though.

Tobias Schmude (Jul 12 2022 at 20:54):

Btw: can someone explain how in Example 3.5. the list object on $F$ induces a monad structure on $T_F$? The unit is directly given, but I don't see how $\varphi$ induces a multiplication.

Tobias Schmude (Jul 12 2022 at 20:55):

Mike Shulman said:

In a way it's sort of an accident that the free-monoid monad (for instance) can be presented as the initial algebra of an endofunctor -- you can think of it as a simple form of cut-elimination.

The accident being that the free monoid on a set $A$ can be obtained by iterating a (polynomial) endofunctor, in this case $X \mapsto 1 + A \times X$, right? What's the connection to cut-elimination?

Reid Barton (Jul 12 2022 at 21:06):

What's the monad structure you have in mind on $\mathit{Tree}(A)$?

Jacques Carette (Jul 12 2022 at 21:45):

$Tree(A)$ is the free Magma Monad.

Mike Shulman (Jul 12 2022 at 21:47):

If you write down a unary type theory for presenting the free category on a graph, whose derivations are therefore lists of composable arrows, then the cut-elimination algorithm is essentially the same as the definition of multiplication that makes ${\rm List}(A)$ into a free monoid. I wrote at length about this in section 1.2 of my categorical logic notes.

Jacques Carette (Jul 12 2022 at 21:50):

The underlying phenomenon seems to arise when the axioms of a theory are affine and don't permute (i.e. each variable is used at most once and in the same order as they are given in the context, on both sides of $=$). I've seen a paper study this in depth, but lost the reference sadly, and have been looking for it again the last 2 years!

Basically, the forgetful functors from such theories have a right adjoint that's given by a polynomial functor because the induced term algebra has normal forms. There's more to it than that, but that's the intuition.

This explains why, for example, the commutative monoid monad doesn't arise as an inductive type. Axioms like commutativity and idempotence give rise to quotients that can't be normalized so easily, unlike unitality and associativity.

Reid Barton (Jul 12 2022 at 21:55):

Jacques Carette said:

$Tree(A)$ is the free Magma Monad.

I think this is for a different "binary tree" (fixed point of $F(X) = A + X^2$).

Jacques Carette (Jul 12 2022 at 21:59):

Ah, you're right, it's for a slightly different notion of tree.

Mike Shulman (Jul 12 2022 at 22:12):

I'd love to see that paper! Let me know if you find it.

fosco (Jul 12 2022 at 22:27):

@Jacques Carette I think that paper is an answer to my question, at least as much as it can be answered...

fosco (Jul 12 2022 at 22:28):

(also: whoops, did I get the tree example wrong?)

Jacques Carette (Jul 12 2022 at 22:32):

There are different flavours of trees. Many of them end up isomorphic, but some 'fit' better than others. Same with Species.

Fabrizio Genovese (Jul 12 2022 at 22:41):

fosco said:

(also: whoops, did I get the tree example wrong?)

I may be wrong but I don't see how trees with decorated nodes (here "decorated" = "what you are annotating with stuff of type $A$") can form a monad.

Fabrizio Genovese (Jul 12 2022 at 22:43):

How do you define multiplication? $TTX$ are trees whose nodes are decorated with trees. The shape of the tree in the decoration may not match the "shape" of the node it is decorating. How do you flatten that?

Fabrizio Genovese (Jul 12 2022 at 22:43):

Reid Barton said:

Jacques Carette said:

$Tree(A)$ is the free Magma Monad.

I think this is for a different "binary tree" (fixed point of $F(X) = A + X^2$).

This clearly works instead, because you are decorating only the leaves. :smile:

Jacques Carette (Jul 13 2022 at 00:06):

Aha, I think I've found (some of) the papers & a presentation:

• Monads of Regular Theories
• presentation: Categories of Equational Theories
• Theories of Analytic Monads

I think affine (not just linear-regular) and rigid are the key terms here. But it appears no one has yet considered the affine case (it just came up in examples that I was doing of explicit adjoints).

Jacques Carette (Jul 13 2022 at 00:16):

There are also related things in term rewriting, called left-linear and right-linear terms - they show up in a categorical setting in for example Guiraud's Termination orders for three-dimensional rewriting.

Morgan Rogers (he/him) (Jul 13 2022 at 08:46):

@Jacques Carette several of those links don't work :octopus:

Jacques Carette (Jul 13 2022 at 11:21):

@Morgan Rogers (he/him) Very strange. I had posted proper links. Anyways, they should be fixed now.

Morgan Rogers (he/him) (Jul 13 2022 at 12:09):

Thanks :)