Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have added to algebra for an endofunctor a remark on the relation to algebras over free monads. While I think that’s pretty obvious, I notice that a) recently somebody has blogged about that here, b) here it says that it’s not true :-) (but I think it’s not meant to be read that way).
The existence of free monads depends on a category in question doesn’t it ? There are also algebras over nonunital monads for which there are important applications. While I am happy you added this content I am unhappy with the statement that the algebra over an endofunctor is less natural notion than an algebra over a monad. It is like saying that a semigroup (nonunital monoid) is less natural notion than a group. Group has more structure and we like it more, but it is really not a defendable statement.
I agree with Zoran. One might as well say (more precisely than Zoran’s analogy) that the concept of a function is odd, since the more natural notion is the action of the free monoid on the set . Monoid actions are pretty nice (although some people would prefer to think of the algebra acting on the vector space , even with the need to specify extra properties in that case), but simple functions are nice too.
I’ve made edits reflecting this.
Looks good, Thanks!
While one can argue endlessly about what is “natural”, I think Urs’ point was more that to an arbitrary mathematician (especially one who knows some category theory), the notion of algebra over a monad may be more familiar than that of an algebra over an endofunctor, and so it may be comforting to know that the one is a special case of the other. I edited the page trying to make this meaning more apparent.
There is also some potential for confusion about the various meanings of the term “free monad”, so I have added some clarification there too.
Maybe to clarify: I came from the point of view that I looked at where these things arise in contexts that are not already intended to be about inductive definitions. Where might the mathematician who is not actively looking for inductive types be secretly using them? That generic mathematician seems to be very unlikely to consider algebras over endofunctors, or algebras over free monads, whereas he is more likely to be considering algebras over non-free monads. That may be because he is only familiar with the latter, but then: that may not be without reason.
I think your comment, Mike, that algebras over endofunctors are really to be thought of as truncated version of -algebras over -monads very much strengthens this intuition.
I like what you did, Mike. But I still don’t understand why a category theorist would find monad algebras more natural than endofunctor algebras. More familiar, sure; that’s sociological. But what could be more natural than an endofunctor algebra?
To some people, “natural” implies in particular “naturally occurring”. Monad algebras clearly occur all over the place in mathematics. Endofunctor algebras could be argued to occur in many places (anywhere that inductive definitions do), but are rarely made explicit; thus monad algebras may seem to occur more commonly than endofunctor algebras.
The same with groups versus semigroups, Mike, especially fo rmainstream mathematicians and physicists.
If one looks at nonunital monads (what is generality in between), modules (you say algebras, but I prefer geometrical language) over nonunital graded monads correspond to (a generalization) of qcoh sheaves on projective cones of graded rings as appearing in algebraic geometry. Saying that projective geometry is less natural than affine is quite an offense for an algebraic geometer.
I guess we cannot settle how we all feel about this. I would just like to appeal to everyone to try to see Lab entries in context. For instance we still have to rectify that the term “initial algebra” currently redirects to the notion over an endofunctor. With all the notions of algebras in common and widespread use – over operads, over monads, over algebraic theories – it seems strange to behave as if the notion over endofunctors were a default notion of algebra.
Who said default notion ? One should say nothing about what is default or natural in such situations when there are several levels of generality (and it is a partially ordered said of generalities, only). Did somebody say that semigroup is a default algebraic structure or that a group is ? I actually never thought somebody would ask for a default algebraic structure or default type of a module.
Who said default notion ?
As I said, the words initial algebra still redirect to initial algebra over an endofunctor. That entry used to be titled initial algebra, in fact, until I renamed it.
I actually never thought somebody would ask for a default algebraic structure or default type of a module.
I don’t want to dwell on it further, but I think you all know that if you go into some math department and start talking about an algebra, the last thing that people expect you to mean is a morphism out of the image of a random endofunctor.
But enough of that, let’s turn to something more constructive now!
The justification for redirecting initial algebra to initial algebra of an endofunctor is (or could be) that this is the only case where people make a big deal out of initial algebras. The initial unital (possibly also associative, commutative) algebra over a field (or even commutative rig) is itself, so people just call it that. The initial non-unital (possibly also associative, commutative) algebra over is , so people just call it that. These are by far the most common uses of ‘algebra’ in my experience, but other uses also have fairly trivial notions of the initial algebra. Only for algebras over an endofunctor (as far as I know) is the initial algebra particularly interesting, such that one wants to refer to it as such.
Compare Wikipedia.
But if there other cases where people refer to initial algebras as such, or in any case if the redirection is confusing, then we should make initial algebra into a more general page.
@Toby 14: That’s what I was going to say.
@Mike #9: Naturally implicitly occurring is still naturally occurring, I would argue even more natural since people didn’t even have to think hard (and make it explicit). I’ll change ‘common and natural’ to ‘familiar’, and that will make me happy.
We are still talking past each other, I think.
Toby writes:
But if there other cases where people refer to initial algebras as such, or in any case if the redirection is confusing, then we should make initial algebra into a more general page.
Right, so that’s what I am trying to get at, this has already happened: we have initial algebra of a presentable (infinity,1)-monad.
I thought what happened was this:
I asked Mike something like “Isn’t the concept of initial algebra over an endofunctor strange, for instance what happens when we pass with it to -categories?”
Mike replied something like yes, indeed, there one sees that it is really a shadow of the notion of initial algebra over a presentable -monad.
To quote from that reply:
I feel like to a category theorist, at least (I can’t say about type theorists), this point of view implies that restricting yourself to ordinary inductive types — initial algebras for free monads — is a weird and artificial restriction.
At that point I thought we already agreed: the notion of initial algebra over a free monad regarded not in the context of initial algebras over general monads (and more generally -monads) is “weird and artificial”.
So what is it we are now disagreeing about? But maybe that’s not so important. Let’s rather move on:
concerning the question of what examples we have for interesting initial algebras over non-free monads: this is precisely what I set out to understand here: in the context of that discussion on the Café titled “What is homotopy type theory good for?” I wanted next to find naturally but unnoticed occurences of higher inductive types. I started thinking: where might we already be studying initial agebras over monads/-monads without realizing that there is a logical/type theoretical interpretation to what we are doing?
Mike has given examples of interesting initial algebras over genuine and non-free -monads. But I guess from that that there must also be plenty of non-free 1-monads that have interesting initial algebras. We should look for them!
Urs, I basically agree with you. I was agreeing with Toby #14 about why initial algebra currently redirects to initial algebra over an endofunctor; I think I agree with you that now it would be better to make it a disambiguation page.
@Toby 16: sure.
Thanks, Urs, now I understand. It isn’t endofunctor vs monad (and still less endofunctor/monad vs -algebra) but endofunctor/monad vs endo--functor/-monad. Then I think that we agree.
I’ll create a disambiguating initial algebra now if I can; but I may be interrupted soon, so if nothing happens within half an hour, then somebody else could make it instead.
Done.
Okay, thanks!
But is it clear that there are no interesting initial algebras for non-free 1-monads? Why?
There are! Every free algebra for a nice 1-monad on a nice 1-category is an initial algebra for some other 1-monad, typically not free (it is the monad-coproduct of with the algebraically-free monad on the constant endofunctor at ). Surely free algebras for 1-monads are interesting.
I’m sure that they’re interesting, just “less common and natural”. (-_^)
than what?
Initial algebras on non-free -monads are also interesting, but they’re less familiar than initial algebras on algebraically free -monads, aka initial algebras on endo--functors.
Maybe secretly they are familiar, but have not been identified as such? Let’s try to identity some!
Say we have a locally connected topos. What’s the initial algebra over the induced monad on the topos?
Personally, I think free abelian groups are plenty familiar to many mathematicians. Probably more familiar than abstract W-types.
As initial algebras of monads, these aren’t familiar by the standard of familiarity that you applied in #9.
Toby,
not sure what the discussion is still about. Maybe to clarify:
you are absolutely right that traditionally the most familiar initial algebras of monads are those of free monads.
But while true, that need not stop us from going beyond! Certainly not once we have realized that traditional thinking here is subject to “weird and articifical restrictions”! :-)
My comment in #23 was facetious, whence the winking smile emoticon. To disrespect initial algebras of monads because they are less traditionally familiar than initial algebras of endofunctors would be silly … as silly as disrespecting algebras of endofunctors because they are less traditionally familiar than algebras of monads. That’s the joke; at least, I found it funny.
Okay, I was reacting to the latest #28, not to #23. It seemed to me that in #28 you were still arguing against something. But if not, then just ignore my previous comment!
Okay, I think this discussion has gone on long enough. (-:
We could still find interesting examples of initial algebras of non-free -monads. Unfortunately, the examples of monads that I mostly know are those cooked up to give familiar objects as their algebras, and the initial algebras there tend to be fairly vacuous. So I only know one good example (really a parametrised infinitude of examples): #22.
Well, since the initial algebra of a 1-monad is also a free algebra of that monad (free on the initial object of the base category), I think #22 encompasses all examples. (-:
On the other hand, one does occasionally find monads that are “cooked up” as you describe in #33 but whose initial algebras are highly non-vacuous. For instance, the category of elementary toposes is monadic over categories, or over graphs, but its initial algebra — the free topos — is highly nontrivial (it knows all about higher-order logic!).
I’ve added a redirect from F-algebra, since I was surprised to not find such an entry already extant, and didn’t immediately think to look at the entry algebra for an endofunctor.
I’ve also added a comment about noting initial algebras for endofunctors’ relationship to inductive types.
If all this is okay, I’d like to make analogous updates re. F-coalgebra and coalgebra over an endofunctor.
That sounds reasonable to me. We also have the page initial algebra of an endofunctor.
As for the ’co-’ case, terminal coalgebra for an endofunctor comments on coinductive types.
I guess redirects are needed for the range of prepositions used: of, for and over
Well, the problem with “F-algebra” is that nowhere is it decreed that an object called must be an endofunctor. But I suppose F is used more often for endofunctors than for other things that have algebras, like monads and rings and theories.
Hmm. Given Mike’s comment, I’m wondering if it might be better to create a new page for ’F-algebra’. (Particularly given that a search for ’F-algebra’ doesn’t show that ’F-algebra’ is a redirect to ’algebra for an endofunctor’, so that if one is looking for a definition of an F-algebra, the search results don’t make it obvious which entr(y|ies) contains such a definition. Perhaps if a search is for a term that has a redirect, that redirect should be noted in the search results?)
My point is that there is no definition of “an F-algebra” until you know the type of F, so it doesn’t make sense as a thing to search for.
Okay, sorry for my misunderstanding.
Here’s the context of why I’ve been looking at this: in reading discussions about Haskell, I’ve encountered people talking using ’F-algebra’ as a category-theoretic concept. My first thought was to come to the nLab for an explanation of this concept. i did a search, and was surprised to find no specific entry for ’F-algebra’ in the search results; and as I alluded to in an earlier comment, not knowing what an F-algebra is, I didn’t know which of the entries listed in the search results I should look at for further information. I ended up doing a search on Wikipedia, and found the F-algebra entry. Now having a general sense about F-algebras, I ended up at the nLab ’algebra for an endofunctor’ page, and thought it would be helpful for other people in my situation to be directed to that page.
If people who want to know about F-algebras should only be directed to the ’algebra for an endofunctor’ page, then I certainly think the suggestion I made in #39, about search result listings, should be implemented at some point. Having said that, I’m not sure I understand why having a page for ’F-algebra’ is substantially different from having a page for (say) (n,r)-category - in both cases, it seems to me we’re talking about a ’type’ that needs to be ’instantiated’. Is this incorrect?
Hi Alexis, I missed your suggestion about searching first time around. At first glance, it sounds good to me. Please add it to the Technical TODO list (nlabmeta).
@Richard: Done - thanks. :-)
It would certainly be nice to include redirects in search results, I’ve wished for that before. However, I do note that https://www.google.com/search?q=site:ncatlab.org+F-algebra gets you to algebra for an endofunctor as the top hit, and this is the search that’s done by the green “Search the nLab” box on the HomePage. Possibly we should consider putting the google search box at the top of every page instead of or in addition to the built-in instiki one.
You’re right that there is no qualitative difference between -category and -algebra; both are names that contain a variable. In practice, however, when we write -category there is practically no potential for confusion: the only other name of the form “?-category”, with ? a variable, that I can think of is -category for an enriched category, and the chances of someone using lowercase to denote a monoidal category are slim to none. Even given that, I would have preferred to name the page n-category as something not including a variable, were it not for the fact that there is really no other option available.
With algebras, in contrast, there are oodles of different kinds of algebras: in addition to algebras for endofunctors we have algebras for monads, algebras for pointed endofunctors, algebras for rings and fields, algebras for algebraic theories, and probably others; all of which are commonly denoted by “?-algebra”, and in many cases the ? might quite reasonably be denoted by the letter (particularly, for instance, a pointed endofunctor or a field). Moreover, algebra for an endofunctor is a quite reasonable and unambiguous alternative page name.
Re #43: Thanks Alexis!
@Mike:
Ah, now I get what you’re saying - thanks for taking the time to elaborate!
In the referenced Maciej Piróg’s blog post, there is a construction of just before the Eilenberg-Moore Algebra section. The construction seems problematic to me. In particular, , and does not seem to type-check there. If I understand the matter correctly, the multiplication should be given by initiality, probably not expressible by without further assumption.
If the above is correct, maybe it is better to have a note next to the reference to remind the reader.
– Anonymous Coward
I think you’re right that the author slightly misspoke, or elided over something you’re pointing out, but to me what he was trying to say is clear enough.
So is the initial algebra for the endofunctor . Meanwhile there is an algebra structure on for that endofunctor, i.e., a map , and that’s given by . Thus by initiality, we have a map that is induced by the algebra structure . That’s what he meant to say, no?
Another thing to point out is that he’s overloading the notation . The first time appears, I guess he wants to denote the initial algebra of the endofunctor . (I don’t recall seeing that notational convention before; is it well known?) On the other hand, denotes the monad multiplication.
One could try writing him about these issues, but let me think about a graceful way of handling it at the nLab.
(I don’t recall seeing that notational convention before; is it well known?)
is often used in computer science to denote least fixed points (with being used for greatest fixed points), for example in the modal μ-calculus, and by extension initial (and final co)algebras, for instance in Algebras, Coalgebras, Monads and Comonads.
Thanks for that information, varkor.
@Todd_Trimble, thanks for clarifying. I was slow in filling in the details, and did not realize (forgot) that denotes the unique homomorphism to the algebra among some researchers 1 2. I have seen the notation before, so the misunderstanding is my own fault.
Bird and Moore, The algebra of programming, in Deductive Program Design. google book preview ↩
1 to 55 of 55