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’ve started infinitary Lawvere theory following this n-Forum discussion.
Edits and Questions:
Little bit more on the proof of the adjunction. I’m not done yet but it’s bedtime. I’m probably putting in far too much detail, but I’d rather do that to start with since this sort of thing is fairly new to me so I want to be sure that all the i’s are crossed and all the t’s dotted before pruning the proof down to something more reasonable.
Presumably the next step is to show that it is a monadic adjunction. Is that obvious due to its being a sort of functor category?
I’ve finished with the proof of the adjunction. As I said, probably a messy proof.
Next stop, monadicity. Any opinions on what’ll be the easiest to prove? I see from monadicity theorem that there’s a few choices.
It occurs to me that, while an $S$-sorted theory should be equipped with an $S$-indexed family of sorts, a general many-sorted infinitary Lawvere theory should not be equipped with a family of sorts. Compare this Café comment by Mike; Lawvere theories are at the last stage, where we have generated all additional types (objects) that must exist in our doctrine and are not remembering which are the generating ones, any more than we remember which are the generating operations or axioms.
In other words, the existence of $\mathcal{R}$ in the most general case is simply a smallness criterion. If we were working with finitary Lawvere theories, then we’d just say ‘small’ and be done with it.
On the other hand, when in doubt, one should always say ‘equipped with’. One can always define the morphisms later to ignore this equipment. So an equivalence of $S$-sorted Lawvere theories must preserve the $S$ sorts, while an equivalence of many-sorted Lawvere theories might not.
Anyway, I edited the article a bit to reflect this.
I mostly agree with you. What I hesitate about is the forgetful functor from $Prod[\mathcal{D},Set]$. Where should it land up? At the moment, I have it landing in $[S,Set]$, but that relies on a choice of $S$. Perhaps this is inevitable: if the theory were 1-sorted then you’d want to end up with a definite set which would mean evaluating the functor on a definite object.
So if we want the forgetful functor to be part of the deal of $Prod[\mathcal{D},Set]$ then we need to choose a subcategory of sorts.
Hmmm, maybe I should go and read that “What is a theory?” discussion.
@Toby #6, I think that’s an interesting question irrespective of finitarity or even many-sortedness. Is an ordinary “Lawvere theory” equipped with a generating object, or such that there exists a generating object? I think that’s the difference between the last two levels of embodiment: the “multicategory” level and the “fully embodied” level. A Lawvere theory, as a category with finite products, is fully embodied – but if we consider its generating object as structure and require morphisms to preserve that structure, we get a 2-category of Lawvere theories equivalent to that of finite-product-multicategories, at one lower level of embodiment. Just like if we consider, say, the category of free groups with specified generators and group homomorphisms that take generators to generators, we get something equivalent to Set. The conceptual relationship is clear to me, but I’m not sure whether one viewpoint or the other is implied by the terminology “Lawvere theory.” IIRC even back in Lawvere’s original work introducing the concept, he considered both types of morphisms of theories, those preserving the generator and those not.
Okay, so there’s some value in allowing for both.
But am I right that we need the sorts in order to define the forgetful functor when trying to make $Prod[\mathcal{D},Set]$ in to an algebraic category over something?
@ Andrew
I think that you’re phrasing the conjecture wrong. It should state that unsorted infinitary Lawvere theories correspond to monads on $Set$ (or monadic categories over $Set$). Then $S$-sorted infinitary Lawvere theories correspond to monads on $Set^S$, not on $Set$ at all. I’m not sure that many-sorted infinitary Lawvere theories correspond precisely to anything in this way.
@ Mike
The theorem that finitary Lawvere theories correspond to finitary monads on $Set$ requires that we preserve the generating object; that’s what I was going on. If you’re not going to preserve it, then I’m not sure why you wouldn’t at the same time generalise to all small categories with finite products. (Maybe I should see what Lawvere does with that.)
@ Andrew again
I see that you have written in the assumption that the assignment of sorts is injective. But I don’t see where you actually use this.
There are counterexamples. I think that the simplest is the theory of a subsingleton, which has one type (so unsorted), no operations, and one equation ($x = y$). Here we have $R \cong R^n$ for all $n \geq 1$. (You can even get $R \cong R^n$ for all $n$ if you add a single $0$-ary operation to get the theory of a singleton.)
Maybe to avoid even suggesting that one might want to preserve the collection of sorts, we should define a many-sorted infinitary Lawvere theory to be any category $\mathcal{D}$ with all small products such that both $\mathcal{D}$ and $Prod[\mathcal{D},Set]$ are locally small. Having eliminated the sorts as such, the term ‘many-sorted’ is a bit odd here, but this is just the red herring principle; this is the general notion of infinitary Lawvere theory, living at the fully embodied level.
Then it is a theorem that (for each small set $S$) the underlying category of each $S$-sorted infinitary Lawvere theory is a many-sorted infinitary Lawvere theory; and it is a conjecture that each many-sorted infinitary Lawvere theory is the underlying category of some $S$-sorted infinitary Lawvere theory (for some small set $S$), which hopefully we can prove in analogy with Freyd & Street.
Toby #10: I agree.
Toby #11: I thought I might need that to be the case in order that the components in the underlying graded set be somehow independent. But today I decided that that wasn’t necessary: if I take the category of, say, groups and decide that I’m going to think of it as 2-sorted, then I get a category over $Set^2$. If I take two sets, $X$ and $Y$, then I still get a free group on the pair $(X,Y)$, but because the two components have to be isomorphic[1], it’s actually the free group on $X \coprod Y$.
[1] For simplicity, I’m assuming that the 2 sorts could both generate the whole category in question.
Okay, so we have:
Is that right?
Right, with two caveats:
(I have implicitly numbered your unnumbered list above.)
Also, we should be careful using the word ‘generate’ here, since we’re not talking about a generating set. It’s OK here, where we all know what we mean, but we should avoid it on the Lab itself. I will try to say ‘span’ (the verb) instead.
@ Mike re the category of free groups
Once you say that a group is free on $3$ generators, what more is there to say about such a group? It is not only determined up to isomorphism, but up to unique isomorphism, the unique isomorphism that fixes each generator. So while one can certainly talk about arbitrary group endomorphisms (or arbitrary endo-functions, for that matter) of this group, I would not think of these as morphisms normally.
Actually, free groups are a little too trivial here; let’s consider finitely generated groups instead. Being finitely generated is a size condition, like the size condition that we wish to impose on many-sorted infinitary Lawvere theories, that makes reference to a generating family. In both cases, the question is whether the morphisms pay attention to which generating family is chosen.
Again, I would take as morphisms between groups generated by $3$ generators are the group homomorphisms that preserve the generators. (Such a morphism is again unique if it exists, but it may not exist. So really I am looking at the poset of quotient groups of the free group on $3$ generators.) Again, one can look at arbitrary group homomorphisms, or even arbitrary functions, between them, but I wouldn’t think of these as morphisms normally.
But for arbitrary finitely generated groups, I think that I would want the morphisms to really be all group homomorphisms. Even if I restrict to homomorphisms that map generators to generators, this is still more general than homomorphisms that fix generators (which doesn’t even make sense in this context).
1 to 15 of 15