Lawvere Theories

In many previous posts, we have discussed connections between monads and universal algebra. So far, we have seen that given a presentation (\Sigma,E) of an algebraic theory in terms of set of operations \Sigma, and equations E, there is a corresponding monad \mathbb{T} such that:

  • The Eilenberg-Moore algebras of the monad are the algebras described by the chosen presentation.
  • The Kleisli category is the full subcategory of free algebras.

Many other aspects of monad theory can then be stood from this algebraic perspective.

Every monad arising from a presentation in terms of operations and equations is finitary. This is a technical condition saying that certain colimits are preserved by the monad endofunctor, but we will not dwell on the precise details. Intuitively, the idea is that the functor is completely defined by its action on finite objects. The key point is that there is a correspondence between algebraic presentations and finitary monads, for which the categories of algebras coincide. It is essential that the categories of models agree for this relationship to be algebraically meaningful. Note this is not a bijection, as a given finitary monad will have infinitely many potential presentations in terms of operations and equations.

In this post, we will see a third perspective on describing algebraic structures, Lawvere theories. These sit somewhere between conventional universal algebra and monads in their level of abstraction. As with any mathematical phenomenon, each new perspective deepens our understanding, and emphasises new features and intuitions.

The Idea of Lawvere Theories

To be concrete, lets consider what we need to do to describe a monoid. The general situation for different algebraic structures will follow in the same way.

Typically, we first pick out an underlying set M, and two functions:

  1. A zero argument function, or constant, for the unit element. We can identity this as a function 1 \xrightarrow{z} M.
  2. A two argument function, or binary operation, for the monoid multiplication. We can identify this with a function M \times M \xrightarrow{m} M.

Of course, once we have these functions, we can build further ones by combining them together. For example

M \times 1 \xrightarrow{m \circ (z \times \mathsf{id}_M)} M

Which informally we can think of as corresponding to a term m(z,x). Of course, by one of the monoid unit axioms, we require that this composite is equal to

M \times 1 \xrightarrow{\pi_1} M

which we can think of as corresponding to a variable x. So in this way of describing a monoid, we:

  1. Pick out some basic operations, which are maps of the form X^n \rightarrow X.
  2. Build lots of other operations by composing the basic operations together, using category composition, and the properties of products.
  3. Require that certain of the operations are equal.

We note some issues with this naive plan. Firstly, where did the basic operations come from, and why do we distinguish them from the other operations? This bias towards certain operations seems categorically unnatural, and raises the ugly question of whether any further mathematical results we derive might be dependent on our choice of presentation. Secondly, a small but annoying detail. It was a pain that M \times 1 was only isomorphic, and not equal to M when we built our composite terms. If we build up more complicated composites involving higher Cartesian powers, we will spend a lot of time bookkeeping how to bracket expressions like:

M \times ((M \times M) \times M)

for no practical benefit. So putting all this together, it would be convenient if we could describe the theory of monoids as a category with:

  1. Objects the natural numbers, corresponding to the number of arguments of our operations.
  2. (Strict) finite products are given by adding the required arities together m \times n = m + n.
  3. Intuitively, we consider an operation of arity m to be a morphism of type m \rightarrow 1. For example, a binary operation is a morphism 2 \rightarrow 1 and a constant is a morphism 0 \rightarrow 1. Notice that, unlike the common convention, in this case 0 is the terminal object.
  4. A family of n such operations is a morphism of type m \rightarrow n. This is automatic from universal property of the assumed strict finite products.
  5. A diagram commutes in our category if and only if the corresponding operations should be equal in the theory of monoids.

In fact, it is technical important to add a little bit more structure. If we consider the category of sets, and take the full subcategory with objects

\{ \},  \{ 0 \}, \{ 0, 1 \}, \ldots

this category clearly has finite coproducts, given by:

\{ 0,\ldots, m \} + \{ 0, \ldots, n \} = \{ 0, \ldots, m + n \}

If we identify the objects of this category with the natural numbers, via:

n = \{ m \in \mathbb{N} \mid m < n \}

this yields a category with finite coproducts \aleph_0, and therefore a category with finite products \aleph^{op}_0.

Moving away from the special case of monoids, we then define a Lawvere theory to be a category \mathcal{L} with strict finite products, with an identity on objects strict finite product preserving functor I : \aleph^{op}_0 \rightarrow \mathcal{L}. The category \mathcal{L} can be interpreted as encoding the operations and equations of the theory. We shall return to the interpretation of the inclusion I later. A morphism of Lawvere theories H : (\mathcal{L},I) \rightarrow (\mathcal{L}',I') is a finite product preserving functor H : \mathcal{L} \rightarrow \mathcal{L}' such that I' \circ H = I.

What we really wanted to do was describe a class of algebraic structures, using our theory. A model of a Lawvere theory in a category with finite products \mathcal{C} is a finite product preserving functor

A : \mathcal{L} \rightarrow \mathcal{C}

and a homorphism of models is a natural transformation between them. For conventional algebraic structures, we take \mathcal{C} = \mathsf{Set}. Note we don’t require that the models interact appropriately with the product structure, as in fact this is automatic. The category of models of a Lawvere theory and their homomorphisms is denoted

\mathsf{Mod}(\mathcal{L}, \mathcal{C})

This approach of identifying structures with functors from a suitably structured category is known as functorial semantics. Notice the difference with monads as a categorical tool for describing algebraic structures. The Eilenberg-Moore category of a monad captures algebraic structures on a fixed base category, whereas we can straightforwardly considering models of Lawvere theories in any category with finite products. There is a forgetful functor given by evaluation at the object 1:

\mathsf{Mod}(\mathcal{L},\mathcal{C}) \rightarrow \mathcal{C}

In many cases, for example if \mathcal{C} is locally presentable, this functor will have a left adjoint, and will therefore induce a monad on \mathcal{C}. So a single Lawvere theory induces monads on many different base categories.

If we have two Lawvere theories such that we have equivalence:

\mathsf{Mod}(\mathcal{L}, \mathsf{Set}) \simeq \mathsf{Mod}(\mathcal{L}', \mathsf{Set})

then there is an isomorphism \mathcal{L} \cong \mathcal{L}' in the category of Lawvere theories. So there is a very tight correspondence between Lawvere theories and the category of models that they describe.

How to build a Lawvere – take one

So how do we build a Lawvere theory? One approach is to start with a presentation (\Sigma, E). We then form a category with:

  1. Object the natural numbers
  2. Morphisms n \rightarrow m are m-tuples of terms in n variables, quotiented by provable equality in equational logic, with respect to the equations of our presentation.
  3. The product projection onto the ith component of a product corresponds to the term for the ith variable.
  4. Identity morphisms are (necessarily) the tuples of projection morphisms.
  5. Composition is given by substitution of terms.
  6. The inclusion morphism I : \aleph^{op}_0 \rightarrow \mathcal{L} picks out the projection morphism in \mathcal{L}.

So we see the intuition for the inclusion I is that it picks out the trivial terms corresponding to bare variables within the broader collection of operations.

Example: We can build a Lawvere theory for monoids from the usual presentation in terms of a unit and multiplication operation, and unitality and associativity axioms. The category \mathsf{Mod}(\mathcal{L}, \mathsf{Set}) is then equivalent to the usual category of monoids.

Note is important that we do not require models of a Lawvere theory strictly preserves product structure. For the usual products in \mathsf{Set}, if we did this, the category of models for the Lawvere theory of monoids would be empty!

How to build a Lawvere Theory – take two

Instead of starting with a presentation in terms of operations and equations, what if we were given a finitary monad? Can we construct a Lawvere theory directly from this data?

The structure of a Lawvere theory in terms of equivalence classes of terms composed by substitution sounds suspiciously like the algebraic perspective on the Kleisli category of a monad. In fact, the two are very similar, up to some cosmetic details. For a finitary \mathsf{Set}-monad \mathbb{T}, we can construct a Lawvere theory (\mathcal{L},I) as follows:

  1. Form the Kleisli category \mathsf{Set}_{\mathbb{T}}.
  2. Restrict to the full subcategory of objects \{\}, \{ 0 \}, \{ 0, 1 \}, \ldots, and rename the objects to natural numbers in a similar way to the section above.
  3. Take the opposite category.

Tersely, we say the required Lawvere theory is the opposite of (the skeleton of) the full subcategory of finitely generated free algebras. As we would hope, we have an equivalence between \mathsf{Set}^{\mathbb{T}} and \mathsf{Mod}(\mathcal{L}, \mathsf{Set}), so the categories of models coincide.

Monads to Lawvere Theories

Given a Lawvere theory (\mathcal{L},I), we would like to go in the other direction, and construct a corresponding finitary monad. This can be done by taking a coend:

\mathbb{T}(X) = \int^{n \in \aleph_0} \mathcal{L}(n, 1) \times X^{n}

If this is unfamilar, the idea is that we can construct the required monad as a certain categorical colimit. Intuitively, we form the collection of equivalence classes of terms, identifying product structure where appropriate.

Again, the categories of Eilenberg-Moore algebras and models of the Lawvere theory in \mathsf{Set} agree up to equivalence.

In fact, the connection between Lawvere theories and finitary monads is about as strong as we might hope. The category of Lawvere theories is equivalent to the category of finitary monads on \mathsf{Set}. The presence of the inclusion morphism I in the definition of a Lawvere theory ensures that this equivalence goes through correctly.

Conclusion

Lawvere theories give a presentation independent formulation of algebra. They have several strengths:

  1. They are relatively close in form to concepts from conventional universal algebra. In particular, they can be seen as an abstraction of the notion of clone.
  2. Unlike monads, a single object can describe models taken in different categories. For example, we can take models of the Lawvere theory of monoids in sets, posets, topological spaces and so on.
  3. Certain operations for combining theories are more natural from the perspective of Lawvere theories, rather than that of finitary monads.
  4. They are algebraic by construction. By comparison, monads include structures such as the continuation monad, which don’t have a clear interpretation in terms of universal algebra.

There are many generalisations of Lawvere theories, for example to incorporate operations of larger aritites, or enrichments of the base category. These typically come with a correspondence to a natural class of monads, providing a different perspective to work with. The functorial semantics of Lawvere theories also suggests other structures, such as PROs and PROPs, which move us further away from convention algebra to structures potentially having multiple outputs as well as inputs.

One intriguing question is what is the equivalent of Lawvere theories for comonads. At this point there does not seem to be a satisfactory answer, as highlighted in the paper “Category Theoretic Understandings of Universal Algebra and its dual: monads and Lawvere theories, comonads and ?” This example highlight how comonad theory cannot always be seen as routinely “flipping monad theory upside down”, and sometimes a routine application of duality isn’t enough.

Further reading: An excellent source for background is the book “Algebraic Theories” by Adamek, Rosicky and Vitale. Also useful for background is Hyland and Power’s “The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads”. Power has developed much of the theory generalising Lawvere theories in various ways, and applying them in computer science.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: