In a way, this post is a continuation of my notes on functorial semantics for algebraic theories. My main sources are (still) Steve Awodey’s notes lecture notes on categorical logic, and the ncatlab article on algebraic theories. I also read parts of Filip Bár’s Notes on Adjunctions, Monads, and Lawvere Theories.
Lawvere Algebraic Theories
The discussion from last time can be continued in a more abstract setting: We went from algebraic theories to their classifying category and saw that we can essentially replace the theory with its classifying category. The classifying category itself had the property that each of its objects is a product of the basic objects corresponding to sorts. So we can just as well define a theory to be just that, and this is then a (multisorted) Lawvere algebraic theory (LAT, or algebraic Lawvere theory?). Explicitly, such a theory is a locally small category with products and a set of distinguished objects (representing the sorts) such that each object of the category is a (finite) product of these (the non-finite case of course corresponds to infinitary operations). In line with this is the definition of a model of a LAT is a (finite-)product preserving functor , and the homomorphisms of the models are just the natural transformations between the functors.
Immediate examples come from taking the full subcategory generated by an object along with all of its finite powers or any category for an algebraic theory. A more intriguing example is the given by all powers of along with the computable functions .
Given an -sorted LAT , we can consider the category of -models . There is a functor that is given by evaluating a functor at each of the sorts of . Conversely, we have a functor defined via , which is just the free model on the given sets (in the case of finitary theories, replace with the category of finite sets). Checking that requires little more than an application of the Yoneda lemma.
The monad induced by this adjunction is the monad of the Lawvere theory (you can also go the other way around and construct the Lawvere theory of a monad by taking the opposite of the monad’s Kleisli category). As a reminder, the Kleisi-category of a monad is the full subcategory of the free algebras in the monad’s Eilenberg-Moore category. It is then no surprise that : in fact, this is what we stated above, since the contravariant Yoneda-embedding is full and faithful. This last point is sometimes referred to as Lawvere duality and says that the theory is dual to its models.