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: reading & references

Topic: Morphism of Lawvere theories on the nLab

Damiano Mazza (Jul 19 2024 at 18:12):

I just realized that the nLab page about the notion of [[Lawvere theory]] says that

A homomorphism of such theories $T\to T'$ is a product-preserving functor.

(The text is right after Definition A). We agree that this is not enough, right? It should be a product-preserving functor sending the generating object of $T$ to the generating object of $T'$. Otherwise, for example, the terminal Lawvere theory would also be initial, which contradicts the rest of the article (and general practice). Before I edit the article, would someone confirm that I'm not missing something obvious?

Evan Patterson (Jul 19 2024 at 18:20):

I would agree that a morphism of Lawvere theories should preserve the distinguished generator, just as the nLab says that a morphism of [[PROPs]] preserves the generator. The analogy here being, of course, that a Lawvere theory is to a PROP as a category with finite products is to a symmetric monoidal category.

John Baez (Jul 19 2024 at 20:18):

That sounds like an important edit to make, Damiano! Thanks!

Kevin Carlson (Jul 19 2024 at 20:43):

Another way of thinking about this is that Lawvere is part of the coslice category of finite product categories under FinSet^op.

Todd Trimble (Jul 19 2024 at 22:56):

Of course Damiano is correct. A product-preserving functor $T \to T'$ that makes the triangle involving the given product-preserving functors out of $\mathrm{FinSet}^{op}$ commute up to isomorphism.

Todd Trimble (Jul 19 2024 at 22:56):

Which is what Kevin Carlson said using different words.

Nathan Corbyn (Jul 20 2024 at 07:10):

Todd Trimble said:

Of course Damiano is correct. A product-preserving functor $T \to T'$ that makes the triangle involving the given product-preserving functors out of $\mathrm{FinSet}^{op}$ commute up to isomorphism.

I don’t think there should be an up to isomorphism here. (CC @Nathanael Arkor)

Nathanael Arkor (Jul 20 2024 at 10:32):

If one is defining an "algebraic theory" in terms of identity-on-objects functors, then the triangle should commute strictly, so as to get a correspondence with monad morphisms. A popular alternative is to define an algebraic theory simply to be a category with finite products, in which case a morphism should just be a functor preserving finite products, but then one does not get a monad–theory correspondence. I don't personally see the value in using any notion of algebraic theory between these two notions (including the one described on the nLab page), because you get the worst of both words: an awkward definition, and no good monad–theory correspondence.

Nathanael Arkor (Jul 20 2024 at 10:33):

(I think the nLab page could do with some attention, to clarify the subtleties in the definition and their motivation, but I don't have time at the moment.)

Todd Trimble (Jul 20 2024 at 10:45):

If one is defining an "algebraic theory" in terms of identity-on-objects functors, then the triangle should commute strictly

I agree with that. I'm actually fine with either convention, but would say that it is a convention.

Todd Trimble (Jul 20 2024 at 10:47):

For example, we shouldn't be saying $\mathrm{FinSet}^{op}$ under this convention, but some skeleton of that.

Nathanael Arkor (Jul 20 2024 at 11:02):

I feel "convention" suggests that we could make different choices, but we have collectively agreed on a certain choice to make communication simpler. Here, though, if the definition is relaxed, there are mathematical consequences (e.g. failure of the monad–theory correspondence) as well as as more conceptual ones (e.g. the directness of the correspondence with universal algebra). I think this is something that is often overlooked in the definition of algebraic theories (because many people have been incorrectly trained to see all definitions that involve equality as being uncategorical).

Nathanael Arkor (Jul 20 2024 at 11:03):

(Of course, it is true that we should take $\mathbb F$ instead of the opposite of the category of finite sets, but this is something the nLab page does do correctly.)

Todd Trimble (Jul 20 2024 at 11:05):

Nathanael Arkor said:

(Of course, it is true that we should take $\mathbb F$ instead of the opposite of the category of finite sets, but this is something the nLab page does do correctly.)

I hadn't looked any time recently. Good to know.

Of course I agree with the rest of what you say.