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.
There are a few places in the nCommunity where some doubt is cast on the idea that compact Hausdorff spaces can be seen as models of a large Lawvere theory. Since this was something I had in mind in a recent post to the Categories mailing list, I thought I’d take it up here.
In fact, I would like to work more generally with monads on . My tentative claim is that algebras for an arbitrary monad can be seen as algebras for a large Lawvere theory. Since this may seem set-theoretically dubious, I’ll sketch some things out here and see whether someone can point out a mistake in my thinking.
Let be a monad. (You can take it to be the ultrafilter monad if you like, but I’ll work more generally.) Take the large Lawvere theory to be , the opposite of the Kleisli category. This has small products, and the claim is that the category of -algebras is equivalent to the category of functors that preserve (small) products.
One direction is easy. The inclusion preserves coproducts, so if is a -algebra, the composite
preserves products. For , this gives a functor .
In the other direction, given a product-preserving functor , the “underlying set” is [the 1 here is the free algebra on one element], and we would like to produce a -algebra structure on . This should be the composite
where everything looks set-theoretically respectable to me so far. I will omit the details that this really is a -algebra structure, because I think they are tedious but straightforward. So it looks as though we get in this way a functor .
There are further details to check of course. One is that if we start with a model of , pass to the associated -algebra, and pass back to a product-preserving functor as prescribed above, we get the original model back up to isomorphism. I have in mind a Yoneda-like argument for this. Just to bolster one’s confidence slightly that this won’t run into problems, I’ll note that is locally small because the underlying-set functor is faithful: a natural transformation is determined uniquely from its value if , are product-preserving.
Does anyone see any problems with this? I am not yet claiming that (locally small) large Lawvere theories are essentially the same thing as monads on (although I’d like to look into this more carefully as well).
I didn’t even know that this was controversial. The pages Lawvere theory and infinitary Lawvere theory assert your last claim.
Toby and I (and a few others) had some discussions on this (or at least, it feels as though it’s closely related, if not, I’d like to know why not) back in August: see this discussion.
The page infinitary Lawvere theory was involved in that discussion.
(I’d like it clear that I welcome reopening this discussion, btw - it’s something that’s been on my mind again recently)
Finn, there seems to be some conflict with a statement on the page algebraic theory, which leads to a thread here which also seems to cast some doubt. As Mike has thought more closely and deeply about the interaction between set theory and category theory than I have, I am leaving open the possibility that I am making a subtle error.
Andrew, I didn’t read through the nForum discussion in its entirety, but I did skip ahead to see that Sridhar Ramesh made some statements which are aligning with what I’m thinking here, and which looked agreed upon.
So if we define a large (one-sorted) Lawvere theory as a category with small products in which every object is isomorphic to a small power of , then it would seem that locally small large Lawvere theories are essentially equivalent to monads on . Let me look again at the page infinitary Lawvere theory…
Okay, the section Algebraic Categories in infinitary Lawvere theory looks a bit tentatively written (“conjecture”, not “theorem”). I’ll have to go through the proof carefully, but it looks at a glance (having thought about it a bit already now) like it’s going to hold up.
I think I saw, it was you Finn?, someone make reference to Fred Linton’s old article (which I’ve never read myself) which I am supposing might be where all this is originally found, but it doesn’t seem to be too well-advertised. Stuff should be better known; it’s important.
Looking at the history of the page, I see that I was responsible for the bulk of the “Algebraic Categories” section (see, the edit history is useful - it tells me what I was thinking about all of … three months ago!) which would explain the tentative nature as I’m much less sure of my ground in these matters than the rest of you (I’m a topologist!). I would very much appreciate someone looking over it again (Toby had a look at it back then, but more eyes make better proofs, as the proverb goes).
Linton’s paper (in LNM 80, TAC reprint here) does go into this, I think, in the context of structure–semantics adjointness. The formulation is quite general, but I think that his idea of semantics is just a functor , with everything done relative to a subcategory/functor of arities (perhaps dense in ). The theory corresponding to (its structure) is then the full image of . He shows in section 8 that if has a codensity monad then this theory (where ) is equivalent to the opposite of .
As for size issues, what I took from the exchange you linked to between Mike, Sridhar and me was that the problem is not so much with theories as with presentations of theories: Mike said
The case of complete Boolean algebras, for instance, is one where a system of ‘generators and relations’ for a monad fails to actually present one.
I recall being convinced by that discussion that indeed, monads on Set are the same as (locally small) infinitary Lawvere theories, and the only difference is that, as Finn says, you can’t necessarily “present” an infinitary theory by an infinite number of generators and relations, since it might no longer be locally small.
I think there is a nice abstract viewpoint on this in terms of generalized multicategories. Ordinary Lawvere theories are “categories with virtual finite products”—i.e. normalized multicategories over the monad T for finite products on Prof—which have only one object (otherwise you get multi-sorted Lawvere theories). That is to say, they are monoids in the monoidal category of profunctors , where the monoidal structure is composition of profunctors plus the multiplication of T. But T1 is easily seen to be equivalent to (that is, is the result of freely adding finite coproducts to the terminal category), so the objects in this category are simply functors , or equivalently finitary functors , in which case the monoidal structure can be identified with ordinary composition of finitary endofunctors. This shows that ordinary Lawvere theories are the same as finitary monads on Set.
This whole picture works just as well in the infinitary case. Infinitary Lawvere theories are likewise one-object “categories with virtual small products,” hence normalized multicategories over the monad on Set for small products. Hence they are monoids in the monoidal category of profunctors . But now we can easily identify with (that is, Set is the result of freely adding small coproducts to the terminal category), so that this category is precisely the category of functors , and its monoidal structure is identified with ordinary composition of functors. Thus, an infinitary Lawvere theory is exactly a monad on Set.
Where does size play a role? Well, unlike , the monad doesn’t live on the bicategory Prof of small categories and profunctors, but on the virtual double category of locally small categories and locally small profunctors. In general, the proarrows in that vdc can’t be composed, since the composite of locally small profunctors between large categories may no longer be locally small. That means that a priori, the putative “monoidal category” of profunctors in which an infinitary Lawvere theory is to be a monoid is actually only a multicategory. However, the above argument which identifies it with shows that in this case, it is actually a monoidal category.
Quoth Todd:
Finn, there seems to be some conflict with a statement on the page algebraic theory, which leads to a thread here which also seems to cast some doubt.
A very minor edit to bother announcing, but I’ve gone ahead and rewritten what I suspect was the misleading statement on the algebraic theory page (to note that while there is no small Lawvere theory of compact Hausdorff spaces, there is a large locally small one).
There is a nice paper by Martin Hyland and John Power here.
I seem to be confused. What are many sorted theories called and where do they sit in all this? Lawvere theories are singly generated. The theories I am using in spherical object are many sorted.
I don’t know what anything is to be called, but a locally small category L with small products generated by a K-indexed collection of objects, for small K, amounts to the same thing as a monad M on Set^K (with, as before, Prod[L, Set] being equivalent to the Eilenberg-Moore category of M). This is all in exactly the same way as before; e.g., L is the dual of M’s Kleisli category.
We can push this even further by taking K to not necessarily be small; in that case, L needs more than just small products; it needs specifically the product of any multiclass of the generating objects which includes any particular generating object only a small number of times (i.e., the product of any assignment of small powers to each of the generating objects).
(Edit: crossed with Sridhar’s response)
I for one would call them just ‘many-sorted Lawvere theories’. You can view them as singly-sorted theories over , where is the set of sorts.
I’ll probably need to do a little more rewriting of algebraic theory to be satisfied. (I might mention that the Café thread that the article points to needs to be read past the particular branch of the thread it points to, in order to get the full picture.)
Here is a personal gloss on many-sorted theories. A finitary Lawvere theory can be described as a category with finite products together with an object for which every object is a product of finitely many copies of . Or, if you prefer, together with a finite-product-preserving functor which is essentially surjective (the opposite of finite sets can be identified with the free category-with-finite-products generated by an indeterminate , identified with the set of ).
A multi-sorted finitary Lawvere theory on a set of sorts is similarly a category with finite products together with a function for which every object is a product of finitely many copies of objects of the form . Equivalently, it is a category with finite products together with an essentially surjective finite-product-preserving functor , where is the free category-with-finite-products generated by . Here can be formed explicitly: the free category-with-finite coproducts is a comma category or wreath product construction whose objects are , where is the set of sorts and is a finite set. A morphism in consists of a function such that for all . Then
We can even extend this to consider the case where the sorts are conceived as forming a category . Then the free category-with-finite-products on the category is where a morphism of the wreath product consists of and together with morphisms in . A Lawvere theory over the category is again a category with finite products together with an essentially surjective functor which preserves finite products.
We can also extend to the infinitary case, by replacing by and considering a similar wreath-product construction as the free category-with-small-coproducts on a (set or category) . A multi-sorted infinitary Lawvere theory consists of a category with small products together with an essentially surjective functor which preserves small products.
@all That helps. My point was that the current entries on algebraic theory and Lawvere theories etc are confusing (not up to the usual high standards of exposition, … blah blah blah :-)) i.e. I could not decide which entry to link that new stuff on spherical objects to as algebraic theories is a bit ’chatty’ and Lawvere theories is definitely single sorted and although I used to have a knowledge of this stuff (and a copy of Kock and Wraith from 1970!) plus hand written notes on lectures of Chris Mulvey on this etc. the theory has passed on, developed and terminology has changed. I did not feel that I was competent to rework the current entries to where I could use them without mucking them up for others who need them for other things.
Adam’s stuff on PROs is also useful and once honed up a bit will be worth linking to. BTW he has a query there whoch is related to my question here.
I have made some changes and rearrangements in algebraic theory where I tried to address my own concerns. Please let me know if you disagree with anything I’ve done. There is more to add in terms of technical details.
Any chance of (i) a definition of an algebraic theory (as requested at the bottom of the entry), (ii) a mention of the many sorted version, and (iii) a comparison with ideas using sketches.
I like the new structure. It fits better the subject matter.
Excellent suggestions, Tim. I intend to look into this.
I think the page is very nice now, although more precise details would of course also be nice to have.
Yes, it’s looking better already.
I don’t have the time to go into it myself at the moment, but it would definitely be worth expanding on Linton’s paper in LNM 80. It doesn’t seem to be widely known, as you said above, Todd, but it seems (to me, prima facie) to be the right stuff to use if we want a definition of algebraic theories that’s agnostic w.r.t. monads vs. Lawvere theories vs. whatever anyone else comes up with.
Just a thought : there is a link between the categorical shape theory of a functor and the Kleisli category of the codensity monad generated by the functor (as a profunctor). There is also a link with the ’full clone of transformations ’ that Fred Linton uses. This is all in my book with Cordier (although not all originally done by us). I am not sure if that is relevant here or where?
I am a bit confused. In the -topos setup, Lurie abstracted the strong shape theory. Is there a -topos-theoretic generalization of the usual shape theory ?
Perhaps that would be given by Michael Batanin’s paper: Michael Batanin, Categorical strong shape theory, Cahiers Topologie Géom. Différentielle Catég. 38 (1997), no. 1, 3–66. (link on the Shape theory page). I have not completely followed the way the discussion might go, so cannot be sure (and it is n years since I read Michael’s paper.)
1 to 24 of 24