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: Lawvere theories and 2-categories

Sergei Burkin (Oct 05 2023 at 17:40):

The category of spans of finite sets is equivalent to Lawvere theory of commutative monoids. The category of spans is not merely a category, but is also a 2-category. This, and certain intuition coming from a more involved example, suggests that Lawvere theories, or at least some class of them, should have 2-categorical nature.

Is this known? Has it been described anywhere?

Kevin Arlin (Oct 05 2023 at 18:31):

I think the category of spans is a lot of things and thus that this just seems like a coincidence to me. A Lawvere theory is just a category with finite products; surely we can't hope for any particularly substantial class of such categories to have good 2-categorical liftings.

Tom Hirschowitz (Oct 06 2023 at 07:25):

Isn't the Lawvere theory of commutative monoids the category of finite sets?

Regarding your question, a possible answer is that any rewrite system generates a 2-category, whose 1-truncation is the Lawvere theory of the corresponding equational system. A good starting point may be Relating two categorical models of term rewriting, by Corradini et al. (I've worked on this in the higher-order case, i.e., in the presence of variable binding.)

Damiano Mazza (Oct 06 2023 at 08:52):

Tom Hirschowitz said:

Isn't the Lawvere theory of commutative monoids the category of finite sets?

The category of finite sets is not generated under finite products by a single object, so it's not a Lawvere theory in the usual (one-sorted) sense, right?

John Baez (Oct 06 2023 at 09:23):

The category of finite sets is the free category with coproducts on a single object, so its opposite is the free category with products on a single object, and this is clearly a Lawvere theory. In fact it's the Lawvere theory for sets, since it has no interesting operations: no morphisms except those every Lawvere theory must have.

John Baez (Oct 06 2023 at 09:27):

This is the initial Lawvere theory.

John Baez (Oct 06 2023 at 09:28):

The terminal Lawvere theory is the theory for commutative monoids, since this has one operation of each arity, obeying all possible laws.

Tom Hirschowitz (Oct 06 2023 at 09:49):

Oh right, so now I see why @Sergei Burkin was talking about spans, thanks.

Damiano Mazza (Oct 06 2023 at 11:30):

John Baez said:

The terminal Lawvere theory is the theory for commutative monoids, since this has one operation of each arity, obeying all possible laws.

Actually, if I am not mistaken, this is the Lawvere theory of idempotent monoids. The Lawvere theory of commutative monoids may be described as the category whose set of objects is $\mathbb N$ (the natural numbers) and whose arrows $n\to m$ are $m\times n$ matrices with coefficients in $\mathbb N$. This is indeed equivalent to the category of spans of finite sets.

Maybe you were thinking of the terminal (symmetric) operad?

John Baez (Oct 06 2023 at 15:32):

Thanks for catching that! I said "all possible laws" but I left one out!

Mike Shulman (Oct 06 2023 at 16:34):

Isn't there another law you left out: $x = 1$ (the nullary analogue of binary idempotence)? So that the terminal Lawvere theory would actually be the theory of singleton sets?

Mike Stay (Oct 06 2023 at 16:47):

nlab says

The terminal Lawvere theory has exactly one morphism f:m→n for each m,n. Since there is a unique morphism between each pair of objects, each object is in fact isomorphic. Thus, this theory is a terminal category. Algebras of the terminal Lawvere theory are terminal sets, singletons.

John Baez (Oct 06 2023 at 17:04):

Wow, right! Even Damiano left out a law. I hadn't noticed that the law $x = 1$ actually parses, since I thought of $1$ as a nullary operation, i.e. a constant, and $x$ as a unary operation. (I'll let everyone individually figure out how it actually parses; for some people this might be a fun puzzle, while for others it will be dead easy.)

Aaron David Fairbanks (Oct 06 2023 at 17:08):

Tom Hirschowitz said:

Isn't the Lawvere theory of commutative monoids the category of finite sets?

The category of finite sets is the free symmetric monoidal category on a commutative monoid.

John Baez (Oct 06 2023 at 17:08):

Or if you like it's the prop for commutative monoids - another way of saying the same thing.

John Baez (Oct 06 2023 at 17:34):

Let me try to organize my thoughts a bit! Please someone let me know if any of these are wrong.

• the category of finite sets and cofunctions is the free category with products on one object. It's the Lawvere theory for sets. It's also the prop for cocommutative comonoids.

• the category of finite sets and relations is equivalent to the category $\mathsf{Mat}(2)$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of booleans, with matrix multiplication as composition. Here $2 = \{0,1\}$ is the Boolean rig. $\mathsf{Mat}(2)$ is a category with biproducts. It's the Lawvere theory for what? It's also the prop for 'special' commutative bimonoids, where 'special' means that the comultiplication followed by the multiplication is the identity.

• the category of finite sets and isomorphism classes of spans is equivalent to the category $\mathsf{Mat}(\mathbb{N})$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of natural numbers, with matrix multiplication as composition. This is the free category with biproducts on one object. It's the Lawvere theory for commutative monoids. It's also the prop for bicommutative bimonoids.

• the category $\mathsf{Mat}(\mathbb{Z})$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of integers with matrix multiplication as composition also has biproducts. It's the Lawvere theory for what? It's also the prop for bicommutative Hopf monoids.

• the category of finite sets and a unique isomorphism between each pair of finite sets is equivalent to the category $\mathsf{Mat}(1)$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of elements of the terminal ring $1$. This is a category with biproducts. It's the terminal Lawvere theory. It's the Lawvere theory for singletons. It's also the prop for what?

John Baez (Oct 06 2023 at 17:37):

The last question should be easy to answer using this paper:

• Simon Wadsley and Nick Woods, PROPs for linear systems.

But I'm getting tired!

Aaron David Fairbanks (Oct 06 2023 at 17:43):

It's interesting that there are two "degenerate" Lawvere theories: the Lawvere theory for the singleton, and the Lawvere theory for both the singleton and the empty set. The latter is missing the nullary operation $1$, but it still has the law $x = y$.

John Baez (Oct 06 2023 at 17:50):

Yeah! It turns out that for any Lawvere theory there's another theory that has all the same algebras except for possibly one more: the empty set.

John Baez (Oct 06 2023 at 17:53):

It's easy to build, but I only learned that in the comments here:

• The group with no elements.

John Baez (Oct 06 2023 at 17:54):

I had constructed such a Lawvere theory for the theory of groups, but not in a way that generalizes!

Aaron David Fairbanks (Oct 06 2023 at 18:00):

Cool. It's possible that may actually be where I learned this.

Aaron David Fairbanks (Oct 06 2023 at 18:08):

I don't think I have ever heard of a name for a model of the terminal prop.

Sergei Burkin (Oct 06 2023 at 20:02):

Aaron David Fairbanks said:

It's interesting that there are two "degenerate" Lawvere theories: the Lawvere theory for the singleton, and the Lawvere theory for both the singleton and the empty set. The latter is missing the nullary operation $1$, but it still has the law $x = y$.

Is there equation $x=y$ in the latter? There is equation $xy=xx$ and more generally $x_1\dots x_n= x'_1\dots x'_m$, $n,m>1$. I guess the category of algebras for the latter is equivalently the category obtained from the category of sets with a marked point by adding initial object (empty set).

Update: there is also equation $xy=x$, so indeed algebras are either empty or singletons.

Aaron David Fairbanks (Oct 06 2023 at 20:14):

By the equation $x = y$, I mean that the two projection maps $X \times X \to X$ are equal (where $X$ is the distinguished generating object of the Lawvere theory).

Mike Shulman (Oct 06 2023 at 20:21):

Observe that as a category, the terminal Lawvere theory is equivalent to the terminal category: any two objects are uniquely isomorphic. Similarly, the Lawvere theory for singleton-or-empty sets (i.e. [[subsingleton]] sets) is equivalent as a category to the arrow category $(0\to 1)$: all the positive powers $X^n$ are uniquely isomorphic, and there is a map $X^n \to X^0 = 1$ but not in the other direction.

Therefore:

• The Lawvere theory of sets is equivalent to the opposite of the category of finite sets.
• The Lawvere theory of subsingleton sets is equivalent to the opposite of the category of (finite) subsingleton sets.
• The Lawvere theory of singleton sets is equivalent to the opposite of the category of (finite) singleton sets.

That looks like it should be the negative-thinking version of something that extends into higher categories too.

Aaron David Fairbanks (Oct 06 2023 at 20:40):

Also, in general a Lawvere theory is the opposite of its category of free algebras on finite sets. In these cases all the algebras are free.

John Baez (Oct 06 2023 at 21:16):

Now you're reminding me of the beautiful classification of Lawvere theories all of whose algebras are free!

• Total freedom.

and Tom Leinster's comment:

The word “nontrivial” has to be uttered somewhere, otherwise your list of four has two missing:

• sets with exactly one element
• sets with at most one element

Claudio Pisani (Oct 09 2023 at 16:41):

John Baez said:

Let me try to organize my thoughts a bit! Please someone let me know if any of these are wrong.

• the category of finite sets and cofunctions is the free category with products on one object. It's the Lawvere theory for sets. It's also the prop for cocommutative comonoids.

• the category of finite sets and relations is equivalent to the category $\mathsf{Mat}(2)$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of booleans, with matrix multiplication as composition. Here $2 = \{0,1\}$ is the Boolean rig. $\mathsf{Mat}(2)$ is a category with biproducts. It's the Lawvere theory for what? It's also the prop for 'special' commutative bimonoids, where 'special' means that the comultiplication followed by the multiplication is the identity.

• the category of finite sets and isomorphism classes of spans is equivalent to the category $\mathsf{Mat}(\mathbb{N})$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of natural numbers, with matrix multiplication as composition. This is the free category with biproducts on one object. It's the Lawvere theory for commutative monoids. It's also the prop for bicommutative bimonoids.

• the category $\mathsf{Mat}(\mathbb{Z})$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of integers with matrix multiplication as composition also has biproducts. It's the Lawvere theory for what? It's also the prop for bicommutative Hopf monoids.

• the category of finite sets and a unique isomorphism between each pair of finite sets is equivalent to the category $\mathsf{Mat}(1)$ with natural numbers as objects where a morphism $f : n \to m$ is an $m \times n$ matrix of elements of the terminal ring $1$. This is a category with biproducts. It's the terminal Lawvere theory. It's the Lawvere theory for singletons. It's also the prop for what?

In general, for a ri(n)g $R$, the Lawvere theory ${\bf Mat}(R)$ is the theory for modules on $R$.
So, for instance, ${\bf Mat}(Z)$ is the theory for abelian groups.

It is interesting to confront the various kinds of theories that one can use in functorial semantics.
In particular (addressing the one sorted case) one can consider (among others)
Lawvere theories, props, operads (= one-object symmetric multicategories) or cartesian operads.
Cartesian operads and Lawvere theories are essentially equivalent (they capture the same categories of algebras).

Other pairs are related by adjunction. In particular, one has the free Prop $O'$ on an operad $O$, so that $O'$ and $O$ have the same models in $\bf Set$.
For instance, if $1$ is the terminal operad, $1'$ is the Prop of finite sets and functions, so both have commutative monoids as models.
If $D$ is the one-arrow operad, $D'$ is the Prop of finite sets and bijections, so both have sets as models.
Both these instance can be generalized to any monoid $M$ in place of $1$:
if $M_1$ is the operad whose arrows are families of elements in the monoid $M$, then the free Prop $M_1'$ is (the domain of ) the family fibration on the monoid. The models of $M_1$ (and of $M_1'$) are commutative monoids with an action of $M$ on them;
on the other hand, if $M_2$ is the operad with just unary arrows (the elements of $M$; here of course it is involved the adjunction between monoids and operads), then the arrows $n\to m$ of free Prop $M_2'$
are bijections $n\to m$ with $n$ elements of $M$. The models of $M_2$ (and of $M_2'$) are $M$-sets.
(Note that the prop $O'$ is the vertical part of the double category in my approach to operads).

Claudio Pisani (Oct 09 2023 at 16:42):

One also has the free cartesian operad $O''$ on an operad $O$, so that $O''$ and $O$ have the same models in $\bf Set$.
For instance, if we start from the operad $M_1$ described above, $M_1''$ has, as arrows, the finite families in the rig freely generated by the monoid $M$, namely the rig $R_M$ of formal linear combinations of elements of $M$ with coefficient in the natural numbers.
The fact that $M_1''$ has again the same models as $M_1$, is the fact modules $L$ on $R_M$ correspond to actions of $M$ on the underlying monoid of $L$.
In particular, when $M = 1$, we get the cartesian operad for commutative monoids: its arrows are families of natural numbers
(which become matrixes of natural numbers in the corresponding Lawvere theory, where there is not just a single object, but also all its products).

Ryan Wisnesky (Oct 09 2023 at 19:40):

There's a (under appreciated, imo) line of work using 2-categories to formalize re-writing rules for algebraic theories, which are oriented equations, so you have objects as types, morphisms as terms, 2-morphisms as re-writes. Tools like CQL immediately turn Lawvere theories into re-writing systems so as to decide their word problems, which is my interest. https://www.sciencedirect.com/science/article/pii/S0304397596807134 https://www.irif.fr/~mellies/mpri/mpri-ens/articles/hilken-2-lambda-calculus.pdf

Claudio Pisani (Oct 10 2023 at 02:41):

Perhaps, I should have added that finite families of elements of any rig form a cartesian operad, which is not free in general.
Thus, modules on a rig $R$ are the algebras for a cartesian operad (or a Lawvere theory, as mentioned above) but not for an operad.
Likewise, there are of course props that are not free on an operad, such as the prop ${\bf Mat}(R)$.