Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Notions of algebraic theory

Mike Stay (Nov 13 2020 at 16:37):

Lawvere says a theory is a category $T$ with finite products equipped with an identity-on-objects product-preserving functor from the skeleton of FinSet [edit: should be ${\rm FinSet}^{\rm op}$] to $T$. Adámek et al. say it's just a category with finite products. Trimble's multisorted Lawvere theories generalizes FinSet to ${\rm FinSet}/ \Lambda$, giving a set of sorts; whereas the category Set (thought of as an algebraic theory) has a proper class of sorts. What theorems no longer hold in the latter case?

Dan Doel (Nov 13 2020 at 16:43):

Does it have a proper class of sorts? It seems like it has a proper class of arities.

Dan Doel (Nov 13 2020 at 16:43):

At least if it works like FinSet.

Dan Doel (Nov 13 2020 at 16:48):

E.G. you can have 'countable Lawvere theories' by generalizing from FinSet to countable sets, I think. And that gives you operations like $M^A → M$ where $A$ may be a countable set rather than a finite set.

Dan Doel (Nov 13 2020 at 16:48):

$M$ being a model, because this is still single-sorted.

Nathanael Arkor (Nov 13 2020 at 17:01):

If you view Set as an algebraic theory à la cartesian category, then it has a proper class of sorts, because you take the objects to be the sorts.

Dan Doel (Nov 13 2020 at 17:04):

Well, okay, but then FinSet isn't single sorted, is it?

Nathanael Arkor (Nov 13 2020 at 17:04):

However, taking Set to be an algebraic theory (rather than the category of models of an algebraic theory) seems like an unusual thing to want to do.

Nathanael Arkor (Nov 13 2020 at 17:05):

No, it's not either. You need to equip FinSet° (or rather its skeleton) with the generating object to see it as a one-sorted theory. Otherwise you have no chance of recovering the generators up to equality.

Nathanael Arkor (Nov 13 2020 at 17:06):

It's "essentially" one-sorted, though.

Nathanael Arkor (Nov 13 2020 at 17:07):

@Mike Stay: could you explain some of your motivation for wanting to treat Set as an algebraic theory?

Reid Barton (Nov 13 2020 at 17:10):

Isn't there an "op" missing somewhere? Are we talking about Set^op as a finite product category?

John Baez (Nov 13 2020 at 18:32):

Mike Stay said:

Lawvere says a theory is a category $T$ with finite products equipped with an identity-on-objects product-preserving functor from the skeleton of FinSet to $T$. Adámek et al. say it's just a category with finite products.

That should never be called a Lawvere theory - a better term would be "algebraic theory", and I'd use "essentially algebraic theory" for a category with finite limits, regarded as a kind of theory.

Trimble's multisorted Lawvere theories generalizes FinSet to ${\rm FinSet}/ \Lambda$, giving a set of sorts whereas the category Set (thought of as an algebraic theory) has a proper class of sorts. What theorems no longer hold in the latter case?

Note that the set of sorts is extra structure on an algebraic theory making it into a multi-sorted Lawvere theory, not merely an extra property. This extra structure is what makes multisorted Lawvere theories so different than algebraic theories: a model of a Lawvere theory (in Set) has an underlying set, and a model of a multi-sorted Lawvere theory has a set of underlying sets, and this is crucial for many theorems involving theses theories.

So it doesn't make sense to say Set has a proper class of sorts; what you should say is "there's no way to make Set into a multi-sorted Lawvere theory with a set of sorts".

This is a technical, nitpicky remark, but it's pretty important.

John Baez (Nov 13 2020 at 18:33):

Your actual question then is "what can and can't we do with a generalization of multi-sorted Lawvere theories that have a proper class of sorts?"

John Baez (Nov 13 2020 at 18:36):

And while this might be somewhat interesting, if I ever needed to deal with this I'd instantly use the axiom of universes and define $\mathsf{set}$ to be the category of small sets - sets in the first universe. Then $\mathsf{set}$ could be made into a multi-sorted Lawvere theory with every small set as a sort. So, all of Todd's theorems would apply!

Nathanael Arkor (Nov 13 2020 at 19:30):

So it doesn't make sense to say Set has a proper class of sorts

There is a canonical class of sorts associated to any cartesian category: namely, the class of objects. This way, every small cartesian category is canonically a (multisorted) Lawvere theory.

Todd Trimble (Nov 13 2020 at 20:41):

Taking a syntactic point of view, I was thinking of "sorts" as primitives from which one freely generates product types (the construct $(\textsf{FinSet}/\Lambda)^{op}$ is the free category with finite products generated from $\Lambda$), and then one can define a $\Lambda$-sorted algebraic theory to be a category $C$ with finite products equipped with a product-preserving functor $(\textsf{FinSet}/\Lambda)^{op} \to C$ that is variously essentially surjective, or bijective on objects, or the identity on objects, according to taste. For example, there is a 2-sorted theory of vector spaces, where one of the sorts carries the ground field structure, and the other carries a vector space structure over that field. A virtue of the "evil" bijective-on-objects choice is that it assigns a definite $\Lambda$-sorted arity to morphisms in $C$ considered as operations; for example, the Lawvere theory of Jonsson-Tarski algebras is equivalent to a one-object category (a monoid), since all powers of the generating object are isomorphic, but the monoid wouldn't remember anything about arities.

Mike Stay (Nov 13 2020 at 20:41):

Isn't there an "op" missing somewhere?

Oops, yes, sorry. Should be from FinSet^op to the cartesian category.

Todd Trimble (Nov 13 2020 at 20:50):

If one takes the Adamek et al. point of view of (let's say small) categories $C$ with products, which is completely fine, one can follow Nathanael's suggestion and call the objects of $C$ "sorts", and then one would still have an essentially surjective product-preserving functor $(\textsf{FinSet}/Ob(C))^{op} \to C$ induced by the inclusion of $Ob(C)$ (as discrete category) into $C$. Roughly speaking, one can then "pull back" the morphism structure $(d_0, d_1): C_1 \to C_0 \times C_0$ along this functor to get a more "traditional" multi-sorted Lawvere theory from a theory in the sense of Adamek et al. that is equivalent to $C$ in the doctrine of categories with products. So in the end there's not a tremendous amount of difference between these approaches.

Mike Stay (Nov 13 2020 at 20:52):

Lawvere says a theory is a category $T$ with finite products equipped with an identity-on-objects product-preserving functor from the skeleton of FinSet to $T$. Adámek et al. say it's just a category with finite products.

That should never be called a Lawvere theory - a better term would be "algebraic theory", and I'd use "essentially algebraic theory" for a category with finite limits, regarded as a kind of theory.

So I guess my question is, what theorems hold for (single- or multisorted) Lawvere theories that don't hold for algebraic theories? Are there algebraic theories that don't correspond to a finitary monad on Set?

Todd Trimble (Nov 13 2020 at 20:53):

Well, one should speak rather of finitary monads on $\textsf{Set}/\Lambda$ in the multisorted case.

Nathanael Arkor (Nov 13 2020 at 20:55):

Mike Stay said:

Lawvere says a theory is a category $T$ with finite products equipped with an identity-on-objects product-preserving functor from the skeleton of FinSet to $T$. Adámek et al. say it's just a category with finite products.

That should never be called a Lawvere theory - a better term would be "algebraic theory", and I'd use "essentially algebraic theory" for a category with finite limits, regarded as a kind of theory.

So I guess my question is, what theorems hold for (single- or multisorted) Lawvere theories that don't hold for algebraic theories? Are there algebraic theories that don't correspond to a finitary monad on Set?

If you restrict yourself to essentially small cartesian categories, there should be no real difference.

John Baez (Nov 13 2020 at 21:33):

Nathanael Arkor said:

So it doesn't make sense to say Set has a proper class of sorts

There is a canonical class of sorts associated to any cartesian category: namely, the class of objects. This way, every small cartesian category is canonically a (multisorted) Lawvere theory.

Yes, but if you apply this trick to an ordinary Lawvere theory you'll get a multi-sorted Lawvere theory with infinitely many sorts. Which is fine if that's what you want!

John Baez (Nov 13 2020 at 21:42):

Mike Stay said:

Lawvere says a theory is a category $T$ with finite products equipped with an identity-on-objects product-preserving functor from the skeleton of FinSet to $T$. Adámek et al. say it's just a category with finite products.

That should never be called a Lawvere theory - a better term would be "algebraic theory", and I'd use "essentially algebraic theory" for a category with finite limits, regarded as a kind of theory.

So I guess my question is, what theorems hold for (single- or multisorted) Lawvere theories that don't hold for algebraic theories?

Well, as I mentioned, the main thing about Lawvere theory $T$ that you don't have with an algebraic theory is this: every model (in $\mathsf{Set}$) has an underlying set. So you get a god-given functor $\mathsf{Mod}(T) \to \mathsf{Set}$, and this is monadic: it has a left adjoint which creates a monad on on $\mathsf{Set}$. And the category of algebras of this monad is equipped with an equivalence to $\mathsf{Mod}(T)$.

The same story works with slight changes if you have a multi-sorted Lawvere theory: just replace $\mathsf{Set}$ with $\mathsf{Set}^S$, where $S$ is the set of sorts.

If you start with an arbitrary algebraic theory you don't get this stuff until you pick a set of sorts.

Of course as @Nathanael Arkor mentioned you are always free to choose all objects as sorts. So the whole discussion is about technical convenience rather than anything deeply thrilling.

But when I"m talking about the theory of groups I would prefer to let $G$, the group, be my only sort, rather than have infinitely many sorts. Why? Because I would prefer to say a group has an underlying set, rather than an infinite sequences of underlying sets $X_n$ equipped with isomorphisms $\alpha_{n,m} : X_n \times X_m \cong X_{n+m}$ that make an infinite collection of diagrams commute.

Choosing sorts is a way of focusing on what you're really interested in.

Are there algebraic theories that don't correspond to a finitary monad on Set?

I believe so: for example, the algebraic theory for a pair of groups.

John Baez (Nov 13 2020 at 21:57):

I suppose you could pack the information about a pair of groups into a single-sorted Lawvere theory, but I don't see how it would work.

Someone should settle this: is $\mathsf{Gp}^2$ monadic over $\mathsf{Set}$ or not?

John Baez (Nov 13 2020 at 22:00):

As you mentioned recently, sometimes there are surprises: reflexive graphs seem naturally to involve two sorts, and they're clearly monadic over $\mathsf{Set}^2$ - but they're also monadic over $\mathsf{Set}$!

John Baez (Nov 13 2020 at 22:00):

But I'm convinced that these surprises are the exception rather the rule.

Nathanael Arkor (Nov 14 2020 at 01:31):

If you restrict to "pure" algebras (in which every sort is either empty or every sort is nonempty), then every multisorted variety is equivalent to a one-sorted variety. (E.g. see Theorem 5 of Barr's "The point of the empty set".) That's not quite the same question, though.

Todd Trimble (Nov 14 2020 at 03:51):

John Baez said:

I suppose you could pack the information about a pair of groups into a single-sorted Lawvere theory, but I don't see how it would work.

Someone should settle this: is $\mathsf{Gp}^2$ monadic over $\mathsf{Set}$ or not?

It seems to me that $\mathsf{Gp}^2$ is monadic over $\mathsf{Set}$, straightforwardly, via the composite

$\mathsf{Gp}^2 \stackrel{\times}{\to} \mathsf{Gp} \stackrel{U}{\to} \mathsf{Set}.$

This follows from the crude monadicity theorem: both these functors are right adjoints and reflect isomorphisms, and the composite preserves reflexive coequalizers because it is isomorphic to the composite

$\mathsf{Gp}^2 \stackrel{U^2}{\to} \mathsf{Set}^2 \stackrel{\times}{\to} \mathsf{Set}$

where both functors preserve reflexive coequalizers. (But someone please feel free to check up on this.)

However, $\mathsf{Set}^2$ cannot be monadic over $\mathsf{Set}$. Any monadic functor $\mathsf{Set}^2 \to \mathsf{Set}$, being a right adjoint, is representable, say by a pair of sets $(A, B)$ where $\mathsf{Set}^2((A, B), (C, D)) = \mathsf{Set}(A, C) \times \mathsf{Set}(B, D)$. Such a representable cannot be faithful: for example, if both $A$ and $B$ are empty then the functor takes on only terminal values, whereas if say $A$ is nonempty, then the values on pairs $(\emptyset, D)$ are all empty and this is fatal as well.

John Baez (Nov 14 2020 at 07:40):

Darn! First I picked the example of $\mathsf{Set}^2$ but then I thought @Mike Stay would consider that too boring so I switched to $\mathsf{Gp}^2$.

John Baez (Nov 14 2020 at 07:45):

I'm too crude to really understand even the crude monadicity theorem, so if $\mathrm{Gp}^2$ is monadic over $\mathsf{Set}$ I hope it gives a finitary monad - it's be crazy otherwise, huh? - and I hope I can find the Lawvere theory for pairs of groups explicitly.

John Baez (Nov 14 2020 at 07:51):

Oh, maybe the operations that make it possible correspond to these operations that any pair of groups $G,H$ has: the operation that sends any element $(g,h)$ to $(g,1)$, and the operation that sends $(g,h)$ to $(1,h)$.

John Baez (Nov 14 2020 at 07:56):

In other words, what operations on a set $X$, obeying what laws, do we need to be sure it's of the form $G \times H$ for groups $G$ and $H$?

John Baez (Nov 14 2020 at 07:56):

We figure them out by figuring out what operations $G \times H$ has when $G$ and $H$ are groups.

John Baez (Nov 14 2020 at 07:58):

We have all the obvious "pairwise" operations, coming from the usual group operations - for example multiplication gives a binary operation

$m ((g,h), (g',h')) = (gg', hh')$

and so on, and these obey all the usual group axioms. This is just a longwinded way of saying that $G \times H$ is a group.

John Baez (Nov 14 2020 at 07:58):

But then there are operations

$q_1(g,h) = (g,1)$

and

$q_2(g,h) = (1,h)$

and these obey a bunch of further laws (for example, each one is a group endomorphism of $G \times H$), and from these we can tell that any model of our Lawvere theory is not just a group but a product of two groups.

John Baez (Nov 14 2020 at 08:05):

So I think it's really crucial here that a group has an underlying pointed set - that's what allows us to define these operations $q_1$ and $q_2$.

John Baez (Nov 14 2020 at 08:06):

So:

Conjecture. If $\mathsf{Set}_\ast$ is the category of pointed sets, then $\mathsf{Set}_\ast^2$ is monadic over $\mathsf{Set}$.

Nathanael Arkor (Nov 14 2020 at 12:36):

Presumably this follows as a corollary of my comment above regarding pure algebras: for pointed algebraic structures, every sort is inhabited, thus pure. Consequently every multisorted algebraic theory with a constant for each sort is (Morita) equivalent to a one-sorted algebraic theory. This includes the square of pointed sets and of groups.

Todd Trimble (Nov 14 2020 at 16:12):

Interesting comment, Nathanael. I don't know Barr's paper -- I should have a look.

Alternatively, the proof I gave that $\mathsf{Gp}^2$ is monadic over $\mathsf{Set}$ applies equally well to $\mathsf{Set}_\ast^2$.

John Baez (Nov 14 2020 at 21:52):

Thanks, Nathanael. I didn't quite understand your comment at first. Now I do.