Have you tried looking at Linton’s paper An outline of functorial semantics, LNM 80 (TAC reprint)? It’s not an easy one to read, but it seems as though it might help.
]]>Sridhar, in that case I’d ask you to hold off for a moment! I’m learning a lot by working through it for myself. Of course, it would be useful to have your input in the general discussion (both here at at the discussion in the thread titled “infinitary Lawvere theories”).
]]>@Andrew: No, I’m afraid I don’t have any reference; it’s just something I worked out for myself when I was first exposed to the idea of using monads to represent infinitary algebraic theories and needed to get a better grip on it. I could write out the details if you’d like, though.
]]>Thanks, Sridhar. That had eventually become clear to me, but it’s helpful to have your confirmation.
]]>Sridhar: do you have a reference for the correspondence (between such Lawvere theories and monads) and the equivalence of and EM-algebras? I would imagine that both would need only the obvious tweaking to make the corresponding statements in the many-sorted cases.
]]>Just to clarify, though I think it’s probably already become clear by now, the notion of “infinitary Lawvere theory” which I was discussing in the nCafe conversation was “a locally small category whose objects are of the form R^k for each small arity k (i.e., it has small products, and its objects are generated by this from a single object))”. Such unsorted infinitary Lawvere theories L correspond precisely to monads M on Set and furthermore the category Prod[L, Set] is equivalent to the category of Eilenberg-Moore algebras for the corresponding monad M.
]]>(Following on from DR’s two comments)
I’d noticed that message go flying by on the categories mailing list as well and wondered as to its relevance.
Clearly, there’s parts of the story of “infinitary Lawvere theory” that are well-known and well-studied. Things like -algebras are an obvious example of a non-finite Lawvere theory (that is, nonetheless, finitely presented) and compact Hausdorff spaces being another (is that one bounded?), whilst the theory of complete lattices is sort-of similar but not quite. I guess what my plan for this at the moment is:
In #28 I’m assuming that ’large Lawvere theories’ might have something to do with the infinitary theories discussed here. The rest is just context.
]]>Are you getting a permanent job?
No, but my wife is, and in a place where we both really want to live (San Diego). I’ve got 2 years left on my portable NSF postdoc, after which point there are many options. (-:
]]>A possibly relevant example is in the following email from Gordon Plotkin on the categories list (I’ve taken the liberty of texing the asciimaths):
]]>Dear Sergey, In the paper by Hyland, Levy, Power and myself, Combining algebraic effects with continuations, there is a proof that the tensor of the continuations monad with itself, or, indeed with any monad with a constant (i.e. such that is not empty), is the trivial monad.
It is not hard to see this directly, via large Lawvere theories. The large Lawvere theory of the continuations monad has:
and so the constants correspond to maps . Further, using two distinct constants, any two operations can be coded up into one operation and then recovered via the two constants. Given maps of large Lawvere theories such that the images of any two operations in and commute, as has a constant all (the images of) constants in are identified, as usual, but then so are all images of any two operations (which will, for example, include all pairs of projections) and so is trivial.
A more general theorem is also proved in the paper which has as a consequence that the tensor of any monad with rank with the continuations monad exists.
Buying a house ? Are you getting a permanent job ? Did I miss some good news ?
]]>Mike’s been quiet lately.
Mike’s been very busy lately with unrelated stuff, like buying a house.
But I also don’t know whether this stuff is “known” – although I haven’t encountered a lot of people thinking about infinitary Lawvere theories.
I also feel like there is something interesting to be said here relating back to the “levels of embodiment” conclusion we reached back at the Cafe. Saying that the category is locally small and has a small set of sorts is more or less saying that it’s small when considered as a category with virtual finite products, i.e. at one lower level of embodiment. One could then ask for stronger finiteness assumptions like additionally having a small generating set of operations, or also a small generating set of axioms, corresponding to the lower levels of embodiment. It seems like the general fact is that “small theories” at any level of embodiment are well-behaved, but that a small theory at one level of embodiment can become large when embodied further (at least when the doctrine is large, as for the doctrine of finite products).
]]>So presumably there’s a theorem that says that and are locally small if and only if has a small set of sorts.
Your argument in comment #22 generalises to prove that is locally small if has a small set of sorts. The argument from Freyd and Street generalises to prove that has a small set of sorts if both and are locally small.
However, it is possible that has a small set of sorts yet is not locally small; the theory of complete lattices, as defined in my comment #17, is an example.
I would like to prove that has a small set of sorts if alone is locally small, or else find a counterexample, but I haven’t got that yet.
And to check that I understand the example of complete lattices: one just cannot get started with this machinery in that case.
One can get started: one has (although it’s not locally small), and (which is locally small, as it must be since there is only sort). But one can’t go on to prove (as in your comment #12) that the functor from to generated by has a left adjoint, because is not locally small.
So, is this known?
Mike’s been quiet lately. Maybe he knows?
At the very least, we should nLabify it - or am I getting ahead of myself?
I’d like to make sure that we understand everything, but yes. I’ll put a stub at infinitary Lawvere theory, pointing to this discussion.
]]>every object is equivalent to some power of a specified object, say
It used to be . Earlier in the thread it was . I’m going to stick with in this comment.
Sorry! “Mathematics is that which is invariant under change of notation.”
I agree with your definition - that seems a good one. Thinking about the reference Mike added at functor category, we’re effectively saying that when we look at product-preserving functors, then “small” means “set of generators/sorts”. So presumably there’s a theorem that says that and are locally small if and only if has a small set of sorts. And to check that I understand the example of complete lattices: one just cannot get started with this machinery in that case.
That is Fantastic - captial ’F’ for sure - as I wasn’t looking forward to digging deep in the definitions of the morphisms in my category.
So, is this known? Are these definitions and results that we’re rediscovering (at least, for me, the rest of you may know them already)? I want to use this stuff and I’m quite happy to put in a reference, or put in the whole argument.
At the very least, we should nLabify it - or am I getting ahead of myself?
]]>every object is equivalent to some power of a specified object, say
It used to be . Earlier in the thread it was . I’m going to stick with in this comment.
Am I right?
Yes, I think that you’re right!
In #17, I gave an example of a complete, locally small category such that is not locally small, but my example was not an infinitary Lawvere theory, because there was no single object that generated the others. Instead, my example was a many-sorted infinitary Lawvere theory (which I noticed but didn’t mind) with a large number of sorts (which I didn’t really notice). Your proof generalises to any many-sorted infinitary Lawvere theory with a small number of sorts, since then injects into . Conversely, if is locally small, then (by previous arguments) we have a small subcategory that spans , so we can take the sorts to be the objects of , so again we have a many-sorted Lawvere theory with a small number of sorts.
So to sum up, in order to get the best results, we should define a many-sorted infinitary Lawvere theory to be a complete category that is
rather than the naïve definition of any complete category (equipped with a family of sorts if you like, but with the option of letting every object be a sort). Then it is a theorem that is locally small, so it is the category of -modules (aka -algebras or -models). More generally, if is any locally small complete category, then is locally small, so it is the category of -valued -modules.
In the finitary case, if a many-sorted Lawvere theory is equipped with a small family of sorts (and is locally small), then itself must be small; so you can actually take any small finitely-complete category as a many-sorted Lawvere theory, letting every object be a sort by default. When you generalise to infinitary Lawvere theories, will no longer be small (except in a few degenerate cases), but this doesn’t mean that you simply drop the smallness clause; you still have to let the objects of be generated by a small family of sorts. (And you still have to require to be locally small if you want the theorems to generalise, such as the existence of free modules.) This was throwing me off earlier.
]]>Wait, wait, wait … I’ve just confused myself again (easily done, I know).
We have as above: a complete, locally small category wherein every object is equivalent to some power of a specified object, say . We want to consider the category of product-preserving functors , this is what Toby calls . The question is: is that locally small?
I think it is. I think that the natural transformations from to injects in to the set . Firstly, the map is obvious: send to its value at . For the injection, we need to show that if then . This comes from the fact that and are product preserving: for every projection we have a commutative diagram:
As and are product-preserving, and . Hence, by the characterisation of products, is uniquely determined by .
Thus is locally small.
Am I right? Or is there some flaw that I’ve overlooked?
]]>By the way, my uses of ‘is’ should all be interpreted up to isomorphism or equivalence, as appropriate.
I was working under that assumption (Axiom of Toby), but thanks for the confirmation.
Right! This is all looking very nice. I just need to go back to my examples of and see what happens in practice.
]]>Another condition that you could use is that has a small subcategory such that the sub(category with products) of spanned by is all of ; that is, every morphism in is a composite of product projections and tuplings of morphisms in . (So basically, we are bounding the number of generating morphisms rather than bounding the size of the generating objects.) In the doctrine of all categories, the analogue of this is is that has a small subcategory such that is all of , which is to say that itself is small, hence the theorem that Mike added to the end of functor category.
By the way, my uses of ‘is’ should all be interpreted up to isomorphism or equivalence, as appropriate.
]]>I think I understood that! And I’m actually coming to realise that keeping track of the size of everything is important. Now I just need to check whether any of the examples I have in mind satisfy the required conditions. They’re all locally small, so I need to check that is locally small. I guess that finding factorisations is the way to go.
]]>I see the converse that Mike just added to the bottom of functor category. Basically, this says that in the doctrine of all categories, a Lawvere theory, if required to be useful in the sense that both it and its category of functors to are locally small, must itself be small.
Here we are working in the doctrine of categories with products, so the Lawvere theory need not actually be small. But it still must satisfy a smallness condition, as Andrew suggested, being generated in a small way.
]]>If is the infinitary Lawvere theory for complete lattices, then the objects of are just cardinal numbers (or sets), although we write the number as (with in place of and in place of , to be completely precise) when thinking of it as an object of . From this perspective, it’s only the morphisms that are interesting; a morphism from to is a family of words, each written using variables, in the operations of complete lattices, modulo equations that follow from the axioms of a complete lattice. In other words, it’s a family of expressions built out of , , and variables, modulo an equivalence relation.
And indeed, this is not locally small; Wikipedia has a proof (which is the same as Johnstone’s and presumably goes back to Hales) that is a proper class. (This result should have been obvious to me after reading Andrew’s #12, but it was helpful to actually look at the proof again.) Nevertheless, is locally small, since it is .
Conversely, if is locally small, we don’t need that must be locally small. For a counterexample, let be the free category with products on a proper class of objects; an object of is a small family of elements of and a morphism from one family to another is a way of expressing the first as a multisubset of the second, and the number of ways to do this is bounded by their cardinalities. Now let take each generator to , so that it takes a general object, thought of as a family, to its cardinality. Then a natural transformation from to itself consists of independent endomorphisms of , and there are of these.
But if and are both locally small, then I agree with the argument in Andrew #12. So presumably this is the result that Mike quotes from the Café (due there to Sridhar) that every infinitary Lawvere theory gives a monad; you don’t count it as an infinitary Lawvere theory unless it’s locally small (because who wants to deal with categories that aren’t?) and its category of product-preserving functors to is locally small (because how can you use it in algebra if it isn’t?). I thought that I’d read that discussion earlier, but now I see that there was much more to it!
]]>One problem I have with the complete lattices example is that it’s not clear to me what and should be. For example, if we wanted to recover groups then we can take to be the opposite category of the full subcategory of groups consisting of (things isomorphic to) the free groups - much as in the example at Lawvere theory. As free lattices don’t exist, the machinery doesn’t get started!
So above you had your inclusions of 2-categories: . In this, we could insert between the second and third terms. Then would include (?) into the 2-category of algebraic categories, but this wouldn’t extend to and, moreover, wouldn’t be surjective (in any sense) as it wouldn’t hit things like complete lattices.
]]>I want to prove a theorem that if and are locally small (and these seem to be independent questions), then must be bounded. (Then this might be the result that Mike recalled in #9.) But I have to go now.
]]>there is some cardinal such that for every set of cardinality larger than , every morphism factors through
The hypothesis that is unnecessary but probably harmless. However, you need to require that the factor is one of the structure morphisms of a category with products; otherwise the condition is trivial.
nominally we can talk of arbitrarily infinite convex sums, any such will have at most countably non-zero terms
That’s a good analogy! Nominally we can talk of operations with abitrarily infinite arities, but any such will depend on at most arguments.
I don’t see where size becomes an issue in the above.
H’m, let me try this with complete lattices, setting to . (Because already the free complete lattice on elements is large, or so Johnstone says on page 31 of Stone Spaces, although I have not followed the proof in detail.) Certainly the underlying set should be . So maybe is not locally small???
]]>