@ 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).

]]>Right, with two caveats:

- I would like to prove that a category $\mathcal{D}$ with small products has a small generating subcategory whenever both $\mathcal{D}$ and $Prod[\mathcal{D},Set]$ are locally small. The converse holds, so this would give another definition of (1). Right now I’m pessimistic, since Freyd & Street could not prove an analogous result about sites (and their argument, which I now understand, does not obviously generalise).
- I don’t really see the point of this item, as distinct from (4), although presumably Lawvere saw some point to it (in the finitary case). In particular, (4) is the thing that corresponds to a monad on $Set$, not (2).
- No caveat here!
- See (2).

(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.

]]>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:

- multi-sorted infinitary Lawvere theory: category with small products such that there exists a small generating subcategory
- (unsorted) infinitary Lawvere theory: category with small products such that there exists a generating object
- $S$-sorted infinitary Lawvere theory: category with small products and a functor from $S$ whose image is a generating subcategory
- $1$-sorted infinitary Lawvere theory: category with small products with an object which generates it

Is that right?

]]>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.

]]>@ 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.)

]]>@ 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.)

]]>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?

]]>@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.

]]>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.

]]>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’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.

]]>- I think definitely equipped with. Already in an unsorted Lawvere therory, you want to know which object is $R$.
- You can always make $S \to \mathcal{D}$ injective on the nose by replacing $\mathcal{D}$ with an equivalent category, but I don’t think that there’s any point in even mentioning that. Surely we do not want to make $S \to \mathcal{D}$ injective up to isomorphism, since that fails in some examples.
- I agree with your edit, I left out a clause.
- I’d say monadic category as the most precise term (and one that we expect to be correct). I haven’t read your details yet.

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?

]]>Edits and Questions:

- The definition of
**sorts**: Do we want “equipped with” or “there exists a”? Namely, should an explicit set of sorts be built in to the definition? - Relating to that, for an $S$-sorted theory, should the functor $S \to \mathcal{D}$ be injective (in whatever appropriate sense)? Perhaps not, since if not then we can regard a single sorted theory as a degenerate case of a $2$-sorted theory.
- Still on $S$-sorted theories, there seemed to be a bit missing: the image of $S$ in $\mathcal{D}$ should be the/a subcategory of sorts. I’ve put something in appropriate to the fact that we say “equipped with” at the moment.
- Started on the proof that models of the Lawvere theory form an algebraic (monadic?) category, but not gotten all the details (that I know of) down yet.

I’ve started infinitary Lawvere theory following this n-Forum discussion.

]]>