Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 7, 2017

The Category Theoretic Understanding of Universal Algebra

Posted by Emily Riehl

Guest post by Evangelia Aleiferi

We begin the second series of the Kan Extension Seminar by discussing the paper The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads by Martin Hyland and John Power, published in 2007. The subject of the above is to give a historical survey on the two main category theoretic formulations of universal algebra, the first being Lawvere theories and the second the theory of monads. Lawvere theories were introduced by William Lawvere in 1963 as part of his doctoral thesis, in order to provide an elegant categorical base for studying universal algebra, while monads were structures that had been already used in different areas of mathematics.

The article starts with the definition of a Lawvere theory and the category of its models, together with some of their properties. Later the authors proceed to relate the notion of monad to Lawvere theories and they give an explanation as to why they were dominantly used in the understanding of universal algebra, compared to Lawvere theories. Lastly they describe how monads and Lawvere theories can be used in formulating computational effects, motivated by the work of Moggi and Plotkin, and they propose future developments based on the connection between computational effects and universal algebra.

At this point, I would like to take the opportunity to thank Emily Riehl, Alexander Campbell and Brendan Fong for organizing the Kan Extension Seminar, as well as all the other participants for being such a great motivation!

Lawvere theories

Until 1963 the traditional way to conceptualize the general theory of algebraic structures was in terms of equational logic. In his doctoral thesis under the supervision of Samuel Eilenberg, Bill Lawvere attempted the unification of our understanding of universal algebra by using category theory. The advantage of this point of view over the previous one was that we can collect all the information about the operations themselves together with the axioms they are subject to, into a finite product preserving functor. In particular the definition was given as follows:

A Lawvere theory is a small category LL with finite products, together with a strict finite-product preserving identity-on-objects functor I: 0 opLI:\aleph_0^{op} \to L, where 0\aleph_0 is a skeleton of the category of finite sets.

We think of the arrows of a Lawvere theory as the collection of operations in a theory, and in particular, we think the hom-sets L(n,1)L(n,1) as the collections of the n-ary operations we can define. Lawvere theories, together with finite-product preserving commuting triangles between them, form a category Law\mathit{Law}. Moreover, Law\mathit{Law} has coproducts given by the quotient of the disjoint union of the operations of two Lawvere theories, over their equational axioms.

Examples of algebraic structures are in this case described as models of a specific Lawvere theory LL. That is, finite-product preserving functors M:LCM:L \to C, to any category CC with finite products, among which Set\mathit{Set} is of primary interest. In their turn, models together with natural transformations between them form a category Mod(L,C)\mathit{Mod}(L,C). We will talk more about the semantics of a Lawvere theory later on, when we will make the connection to monads. For the moment, we will restrict ourselves to describing a symmetric monoidal structure on LawLaw:

Let LL and LL' be two Lawvere theories. Their tensor product LLL \otimes L' will contain any operations f:nmf:n \to m and f:nmf': n' \to m' of LL and LL' respectively, subject to the following equations:

n×n n×f n×m f×n f×m m×n m×f m×m. \begin{matrix} n\times n' & \overset{n \times f'}{\longrightarrow} & n \times m' \\ {}_{f \times n'}\downarrow && \downarrow_{f \times m'} \\m \times n' & \underset{m \times f'}{\longrightarrow} & m \times m'. \\ \end{matrix}

The unit of the monoidal structure is given by the so called theory of an object, i.e. the category 0 op\aleph_0^{op} itself, considered as a Lawvere theory with the identity functor. An interesting aspect of the tensor product of two Lawvere theories is the behaviour of its models. One can prove that the models of the tensor product LLL \otimes L' in any categroy CC with finite products are equivalent, with respect to the underlying set functor given by the evaluation at 1, to the models of LL in the category Mod(L,C)\mathit{Mod}(L',C). The last can be applied to the Lawvere theory of a group, in order to show that its tensor product with itself is isomorphic to the Lawvere theory of an Abelian group.

Monads and their connection to Lawvere theories

The motivation for formulating universal algebra in terms of monads can be found in the well known “Categories for the Working Mathematician”. It was the observation of Eilenberg and Moore, back in 1965, of the fact that the category of algebras of the monad that arises from the free group functor, is exactly the category of groups. Three years after Lawvere’s thesis was submitted, Linton made the connection to monads as follows:

  • On the one hand, for any given Lawvere theory LL, the underlying set functor U L:Mod(L,Set)SetU_L:\mathit{Mod}(L,\mathit{Set}) \to \mathit{Set}, given by MM(1)M \mapsto M(1), had been proven by Lawvere to have a left adjoint. This adjunction will give rise to a monad T LT_L on SetSet. Linton showed that the category Mod(L,Set)\mathit{Mod}(L,Set) of models in SetSet is equivalent to the category of T LT_L-algebras.

  • On the other hand, if we consider any monad TT on SetSet, one can prove that the opposite of the Kleisli category Kl(T)\mathit{Kl}(T) becomes a Lawvere theory by restricting to the category 0 op\aleph_0^{op} the finite-product preserving canonical functor Set opKl(T) op\mathit{Set}^{op} \rightarrow \mathit{Kl}(T)^{op}.

Moreover, both of these mappings turn out to be functorial. We can observe that if we start with a Lawvere theory LL and consider its monad T LT_L, then the Lawvere theory Kl(T L) op\mathit{Kl}(T_L)^{op} is isomorphic to LL in Law\mathit{Law}. By that, we can consider Law\mathit{Law} as a full subcategory of the category of monads, whose inclusion functor has a right adjoint.

Which approach is better?

History showed that category theorists favored the one in terms of monads. However there are a few drawbacks to that approach. For instance, there is an equivalence of categories between the category of monads on Set\mathit{Set} and the category of large Lawvere theories, i.e. locally small categories with a strict identity-on-objects product preserving functor from the opposite of a skeleton of Set\mathit{Set}. This encompasses monads without rank, which do not preserve all κ\kappa-filtered colimits for any cardinal κ\kappa. This is due do the fact that while we are able to introduce a notion of sum between Lawvere theories (given by their coproduct), as well as a notion of a tensor product, we cannot necessarily do the same for monads without rank, which means that we are moving away from the “algebraic nature” of Lawvere theories.

Thus, why did monads gain prominence over Lawvere theories in understanding unversal algebra? Here are some possible explanations:

  1. While we can consider monads over a general category and then study Set\mathit{Set} as an example of primary interest, Lawvere theories require some notion of finiteness, which does not exist in general. One could use the notion of locally finitely presentable categories but this did not exist until some years later.
  2. It would be easier to visualize earlier a generalisation of Lawvere theories in terms of enriched categories, however this area of category theory was not yet widely developed. It was only after the early 80s that we could define Lawvere theories enriched in a locally finitely presentable monoidal closed category VV and consider its models as VV-functors.
  3. Concepts in categorical logic that appear to be closely related to Lawvere theories came to light much later.

Computational effects and universal algebra

Another significant use of monads came from computer science and specifically by Eugenio Moggi’s PhD thesis defense under the supervision of Plotkin in 1987. Moggi introduced his notions of computations and he wanted to give a general semantics of them by using mathematical theory. The actual formulation came a couple of years later, when he used monads to describe computational effects. An alternative suggestion to unify computational effects, related though to the previous one, came in 2002 by Hyland, Plotkin and Power, and it was in terms of Lawvere theories. The argument will become clearer by the use of an example:

Consider a finite set of values Val\mathit{Val} and a finite set of locations Loc\mathit{Loc}. Then the side-effects Lawvere theory L SL_S, when S=Val LocS=\mathit{Val}^{\mathit{Loc}}, is the free Lawvere theory generated by the operations lookup:ValLoc\mathit{lookup}:\mathit{Val} \to \mathit{Loc} and update:1Loc×Val\mathit{update}:1\to \mathit{Loc} \times \mathit{Val}, as it was defined in Notions of Computation Determine Monads, by Plotkin and Power. Then the underlying set functor U:Mod(L S,Set)SetU:\mathit{Mod}(L_S,Set) \to \mathit{Set}, given by evaluation at 11, will give rise to a monad, which in its turn, coincides with Moggi’s side effect monad (S×) S(S\times -)^S. An interesting result relative to the one for the tensor product of the Lawvere theory of a group is the following: The side-effects theory for S=Val LocS=\mathit{Val}^{\mathit{Loc}} is the Loc\mathit{Loc}-fold tensor product of the side-effects theory for S=ValS=\mathit{Val}.

Around this time, Hyland, Plotkin and Power, motivated by observations like the above, showed that computational effects can be regarded as instance of universal algebra. However continuations are an exception to that. This is due to the fact that the continuations monad has no rank so it doesn’t really fit into the setting of Lawvere theories, for the reasons discussed above. This indicates a fruitful area for future work.

Posted at February 7, 2017 5:45 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2935

31 Comments & 0 Trackbacks

Re: The Category Theoretic Understanding of Universal Algebra

Jon Beck was the first to point out the model/module pun, which suggests thinking of algebraic theories as generalized rings. I still think that this analogy has not yet been mined as fruitfully as it could be.

Posted by: Gavin Wraith on February 7, 2017 2:58 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

It’s interesting to hear this! That (possible) analogy was something that really caught my eye when reading this article.

If one writes as a formula what Evangelia mentions in her last paragraph under ‘Lawvere Theories’, when talking about tensors and models, we see that what she’s saying is Mod(LL,C)Mod(L,Mod(L,C))Mod(L\otimes L', C)\simeq Mod(L,Mod(L',C)) with \simeq being a coherent equivalence of categories. When written in this manner, it looks a lot like the Tensor-Hom adjunction we have when working with modules over a ring.

There’s a nice invariance result (Proposition 3.1 in the article) that states the following:

If the categories Mod(L,Set)Mod(L, Set) and Mod(L,Set)Mod(L', Set) are coherently equivalent, then LL and LL' are isomorphic Lawvere theories.

This result, now seen while thinking about modules, led me to wonder what could happen if we were to drop the coherence and relax the condition to just an equivalence. Would it be possible to mirror a Morita-like situation, where nice properties about the Lawvere theories L and L’ must be preserved whenever the categories Mod(L,Set)Mod(L, Set) and Mod(L,Set)Mod(L', Set) are equivalent?

I was glad to hear from Alex Campbell that this is indeed the case! I look forward to delving into this in the near future.

Posted by: Maru Sarazola on February 9, 2017 4:48 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Hi. Just to be clear, this is more than a mere analogy. Every semiring RR gives rise to the Lawvere theory of its modules, in which a morphism mnm\to n is an m×nm\times n matrix over RR. These Lawvere theories have biproducts. In fact every Lawvere theory with biproducts arises in this way. A Lawvere theory with biproducts is a semiring. I first learnt this from Elgot, Matricial theories, J Algebra 1976.

A related fact, which I don’t think I’ve seen in the literature, is that tensor of theories (as in Maru’s comment) actually coincides with tensor of semirings, when the semirings are considered as Lawvere theories with biproducts.

Posted by: Sam Staton on February 11, 2017 8:55 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Maru asked:

Would it be possible to mirror a Morita-like situation, where nice properties about the Lawvere theories LL and LL' must be preserved whenever the categories Mod(L,Set)Mod(L, Set) and Mod(L,Set)Mod(L', Set) are equivalent?

If I understand the question, one answer is that it’s the same answer as found in classical Morita theory: if all idempotents split in LL and LL', then yes, LL and LL' are equivalent (you can even say isomorphic) if their model categories are equivalent.

An easy fact is this: if LL is a category with finite products, then its idempotent envelope (or Karoubi envelope or Cauchy completion, whatever you want to call it) L¯\widebar{L} also has finite products, and for any idempotent-complete category with finite products DD, restriction along the inclusion LL¯L \hookrightarrow \widebar{L}, which of course preserves finite products, induces an equivalence

Prod(L¯,D)Prod(L,D)Prod(\widebar{L}, D) \to Prod(L, D)

This is saying that for any product-preserving functor F:LDF: L \to D, there is an extension to a product-preserving functor L¯D\widebar{L} \to D that is unique up to (unique) isomorphism. So taking the case D=SetD = Set, we see that if two Lawvere theories have the same (i.e., equivalent) Cauchy completions, then they have the same models/algebras.

The other direction is harder, but is treated by Adámek, Lawvere, and Rosický in their paper On the duality between varieties and algebraic theories. I believe the theorem they give is that the Cauchy completion of an Lawvere theory LL is retrieved from the category of models as the category of functors Mod(L)=Prod(L,Set)SetMod(L) = Prod(L, Set) \to Set that preserve limits, filtered colimits, and regular epimorphisms. I have a suspicion (but without thinking about it carefully) that it could also be functors that preserve limits and sifted colimits.

There are loads of examples to consider. The usual Lawvere theory whose models are Boolean algebras is given as the opposite of the category of finite free Boolean algebras; by a baby form of Stone duality, this is equivalent to the category of finite sets of cardinality a power of 22. But we can just as well use the category of finite sets of cardinality a power of 33! Indeed, their Cauchy completions are the same (the category of finite nonempty sets).

The Lawvere theory for groups, namely the opposite of the category of finitely generated free groups, is Cauchy complete. This easily follows from the fact that subgroups of free groups are free (so that retracts of finitely generated free groups are finitely generated and free).

But as far as I know, it’s a hard and profound open question whether the usual Lawvere theory for commutative rings is Cauchy complete, or similarly for commutative kk-algebras over a commutative ring kk. I tried inquiring about this at MathOverflow here.

Posted by: Todd Trimble on February 11, 2017 1:56 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Welcome back, Kan Extension Seminar! And thank you, Evangelia!

Posted by: Tom Leinster on February 7, 2017 3:14 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

This is due to the fact that the continuations monad has no rank so it doesn’t really fit into the setting of Lawvere theories

I looked for a definition of “rank”.

Notions of Computation Determine Monads says:

the monad for continuations R (R )R^{(R^-)} does not have a rank (see [9] for a definition),

with 9 being:

G. M. Kelly, Basic Concepts of Enriched Category Theory, Cambridge: Cambridge University Press, 1982.

in which a search can’t find the word “rank”.

In the nLab the only mention seems to be in colimits in categories of algebras which says

If CC is a locally presentable category and TT is an accessible monad (aka a bounded monad, aka a monad with rank) on CC, then C TC^T is also locally presentable and in particular cocomplete. Details may be found in Locally presentable and accessible categories.

So it seems having rank is important but goes by other names but the nLab has no definition of rank.

In an answer to this MO question MO: What is known about the category of monads on Set? Steve Lack says:

Instead of finitary monads, you can take monads of rank α\alpha, for some regular cardinal α\alpha - these are the ones whose endofunctors preserve α\alpha-filtered colimits, and which can be described in terms of α\alpha-small operations and equations. The full subcategory Mnd αMnd_\alpha of MndMnd consisting of the monads of rank α\alpha is also locally finitely presentable. For example Mnd fMnd_f is just the case where α= 0\alpha=\aleph_0.

So does Kelly define rank under some different name and does discussion of rank and having rank appear in the literature with variant terminology? Could the nLab be updated to explain this?

Posted by: RodMcGuire on February 7, 2017 6:16 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

The relevant section in Kelly’s book is 4.6, where he talks about filtered categories and colimits. He does not mention ‘rank’, but does emphasize functors that preserve filtered colimits.

Posted by: Ze on February 8, 2017 2:34 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

We can fix that. I declare a race to add rank to the nLab. Ready, set, go!

Posted by: Emily Riehl on February 8, 2017 11:04 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

We can fix that. I declare a race to add rank to the nLab. Ready, set, go!

Posted by: Emily Riehl on February 8, 2017 11:05 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Thomas Holder is the winner at rank.

Anyone want to add something?

Posted by: David Corfield on February 8, 2017 1:59 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

A “monad with rank α\alpha” is the same as an “α\alpha-accessible monad”.

Posted by: Mike Shulman on February 8, 2017 12:11 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Typo: in the definition of Lawvere theory, you mean 0\aleph_0 (not 0 op\aleph_0^{op}) to be the category of finite sets.

Posted by: Tom Leinster on February 7, 2017 8:07 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

I fixed that and a few other typos. Nice article! I have some questions but I’m not awake enough to formulate them right now… I can catch typos in my sleep.

Posted by: John Baez on February 8, 2017 7:00 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Thanks John! You may be able to catch typos in your sleep, but apparently I wasn’t awake enough to notice them myself…

Posted by: Emily Riehl on February 9, 2017 3:49 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Hyland and Power’s paper also defined sums of Lawvere theories, and it was pointed out during our session that these are given by pushouts over their respective functors 0 opL,L\aleph_0^{op} \to L, L'. They remark that while sums of Lawvere theories are easy to define, the same can’t be said for monads.

Part of our discussion of this paper involved seeing what a similar sum or coproduct of monads might look like. Sums of monads don’t exist in general, and even when they do (e.g. when they are finitary, and hence correspond to Lawvere theories) taking pushouts over the respective units 1T,T1 \to T,T' of two monads doesn’t give the right notion.

I’ll let others who are more familiar with this construction say what it is, when it exists.

Posted by: Ze on February 8, 2017 2:26 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

There is a way of finding coproducts of monads via pushouts, although I’m not sure it helps that much in seeing what they look like concretely. Let TT and TT' be monads on 𝒞\mathcal{C} and write F T:𝒞𝒞 TF_T : \mathcal{C} \rightarrow \mathcal{C}_T and F T:𝒞𝒞 TF_{T'} : \mathcal{C} \rightarrow \mathcal{C}_{T'} for the free functors to the Kleisli categories of these monads. Let F:𝒞𝒟F : \mathcal{C} \rightarrow \mathcal{D} be the pushout of F TF_T and F TF_{T'}. If FF has a right adjoint, then the monad induced by that adjunction is the coproduct of TT and TT'.

Why is that? Write BO(𝒞)BO(\mathcal{C}) for the full subcategory of 𝒞/Cat\mathcal{C}/\mathbf{Cat} consisting of the bijective-on-objects functors out of 𝒞\mathcal{C}. This is a coreflective subcategory since the bijective-on-objects and full-and-faithful functors form a factorisation system on Cat\mathbf{Cat}. It follows that coproducts in BO(𝒞)BO(\mathcal{C}) are the same as in 𝒞/Cat\mathcal{C}/\mathbf{Cat}, i.e. given by pushouts.

On the other hand we can define a functor from the category of monads on 𝒞\mathcal{C} to BO(𝒞)BO(\mathcal{C}) sending TF TT \mapsto F_T. This turns out to be full and faithful and identifies the monads with the bijective-on-objects left adjoints out of 𝒞\mathcal{C}. (I’m not sure if this appears in the literature anywhere; if it does I’d be grateful for a reference! In any case it’s not too difficult). In particular this inclusion reflects coproducts.

Posted by: Tom Avery on February 8, 2017 5:00 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Hi Tom! Welcome back to the Kan Extension Seminar!

I didn’t know about this construction of the coproduct of two monads, but it makes sense in retrospect: it’s the same as the construction of the coproduct of two Lawvere theories! Given identity-on-objects strict product preserving functors 0 op\aleph_0^{op} \to \mathcal{L} and 0 op\aleph_0^{op} \to \mathcal{L}', the legs of the pushout cone in Cat again are identity-on-objects and strict product preserving, an the composite functor 0 op+\aleph_0^{op} \to \mathcal{L} +\mathcal{L}' defines the coproduct of the Lawvere theories.

The connection with Kleisli categories of the associated monads is explained in Evangelia’s post above, and I suppose this gives another verification of Tom’s construction in the case of finitary monads on Set (in which case the right adjoint he mentions will always exist).

Posted by: Emily Riehl on February 9, 2017 3:41 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Nice argument, Tom! A related observation came up in our class discussions, namely that bijective on objects functors out of a category 𝒞\mathcal{C} are equivalent to monads on 𝒞\mathcal{C} in the bicategory of profunctors (also known as cateads). From this perspective it’s again not too difficult to see that the bijective on objects left adjoints out of 𝒞\mathcal{C} correspond to the “representable” cateads (i.e. ordinary monads) on 𝒞\mathcal{C}.

Another perspective on colimits of monads is that one can always define what the category of algebras for a colimit ought to be. So, given two monads TT and TT' on a category 𝒞\mathcal{C}, an algebra for the coproduct T+TT + T' should be an object of 𝒞\mathcal{C} with both a TT-algebra structure and a TT'-algebra structure, and the (T+T)(T+T')-algebra morphisms should be those morphisms in 𝒞\mathcal{C} which are both TT-algebra morphisms and TT'-algebra morphisms. This defines a category with an underlying functor down to 𝒞\mathcal{C}, but it won’t have a left adjoint in general. Indeed, the coproduct monad T+TT+T' exists if and only if this underlying functor has a left adjoint, in which case it is the monad induced by this adjunction.

Posted by: Alexander Campbell on February 9, 2017 11:23 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Since LawLaw is a symmetric monoidal category, it seems to natural to ask:

Is it closed? What do duals look like, if they exist? And what are monoids in this category?

Posted by: Ze on February 8, 2017 2:42 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

The tensor product in Law of two theories Th(Gizmo) and Th(Gadget) is a Gizmo in the category of Gadgets or, equivalently, a Gadget in the category of Gizmos.

The monoidal unit for the tensor product is the “Lawvere theory of a Set”, i.e. the theory generated by no function symbols or equations, i.e. 0 op\aleph_0^{op}. It is also the initial and terminal object, so there’s a canonical unit for any monoid object in Law.

Since a model of any theory in the category of models of that theory is already equipped with all the required structure, I think that that ThTh=ThTh \otimes Th = Th, so the multiplication in the monoid would just be an endomorphism of the theory.

Posted by: Mike Stay on February 8, 2017 2:46 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

It just occurred to me that I was using the PROP for monoids with models in (Law, \otimes) rather than the Lawvere theory of monoids with models in (Law, ×\times). In either case, it will be equivalent to the notion of a monoid in the category of finitary monads with the corresponding tensor product and categorical product.

The product of two theories has a single sort, and its function symbols are pairs of function symbols with the same arity. The equations get modified to apply to the projected components.

For example, the product of the theory Th(AbGrp) of abelian groups and the theory Th(Mon) of monoids with sorts A and M, respectively, would have

  • one sort A×MA\times M

  • two function symbols

    • (+,*):A×M×A×MA×M(+, *)\colon A\times M \times A\times M \to A\times M

    • (0,1):1A×M(0, 1)\colon 1 \to A\times M

  • equations

    • (+,*)(+, *) is associative and unital in both components and commutative in the first, i.e.
(1)π 1((a,m)(+,*)(a,m))=π 1((a,m)(+,*)(a,m))\pi_1((a, m) (+, *) (a', m')) = \pi_1 ((a', m') (+, *) (a, m))

The product of a theory Th with itself may not be Th, but if Th only has one function symbol of each arity, it is. In those cases, a monoid in (Law, ×\times) is also just an endomorphism of the theory.

Posted by: Mike Stay on February 8, 2017 3:12 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Hmm, I must have something wrong. The terminal object ought to be the monoidal unit for the cartesian product of theories, but that’s clearly not true of the construction I gave, which I got from this mathoverflow post. Where did I go wrong?

Posted by: Mike Stay on February 8, 2017 3:28 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Ah! 0 op\aleph_0^{op} is not the terminal theory; in fact, I’m not sure how I ever thought that, since any theory with function symbols has no morphisms into 0 op\aleph_0^{op}.

It’s not clear to me that there even is a terminal Lawvere theory. It would have to have morphisms of every arity satisfying all possible equations.

Posted by: Mike Stay on February 8, 2017 5:24 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Actually there is one, as noted by Hyland and Power in this paper: it is the category on the object set of 0 op\aleph_0^{op} that is equivalent to the terminal category 1 (i.e., with exactly one morphism in each hom-set).

As a Lawvere theory, this category is a bit counter-intuitive: all of its objects are isomorphic to the terminal object, and thus each object is the nn-fold product of any other object for any nn. The labeling of the distinct objects however chooses distinct nn-fold products for each nn.

We had some fun in our video chat working out what the models for this Lawvere theory are. I’ll leave this for someone else to comment on.

Posted by: Emily Riehl on February 9, 2017 3:47 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Responses to Mike.

ThTh=ThTh \otimes Th = Th

For ThTh the theory of groups, ThThTh \otimes Th is the theory of abelian groups, for the same reason that a group object in the category of groups is an abelian group.

It’s not clear to me that there even is a terminal Lawvere theory.

There is, and it’s just the indiscrete category on the natural numbers.

Posted by: Todd Trimble on February 8, 2017 6:01 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Suppose we have two Lawvere theories Th(Gadget) and Th(Gizmo), with corresponding finitary monads M(Gadget) and M(Gizmo). In order to compose two monads and get a new monad, we have to choose a distributive law natural transformation. The resulting monad corresponds to the Lawvere theory (Th(Gadget) + Th(Gizmo))/~, where ~ is the equation expressing the distributive law.

Posted by: Mike Stay on February 8, 2017 1:50 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

This comment is a great segue into the next post which will on Beck’s paper Distributive Laws.

Posted by: daniel cicala on February 8, 2017 6:44 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

Thinking of Cat as a mere 1-category, there is a 1-monad Λ\Lambda for the free cartesian closed category on a category. To every category X it assigns the category Λ(X)\Lambda(X) whose objects are generated by ×,,1,\times, \multimap, 1, and the objects of X.X. (I’m using \multimap instead of the usual \to to avoid collisions with the arrows for morphisms and 2-morphisms.) Its morphisms are generated similarly, but given f:xyf\colon x\to y and f:xyf'\colon x' \to y', we get the morphism ff:(yx)(xy).f\multimap f'\colon (y \multimap x') \to (x \multimap y').

The monad Λ\Lambda does not extend to a 2-monad on Cat because of the contravariance of the first slot of \multimap: suppose we have functors x,y:1Xx, y\colon 1 \to X that pick out objects x,yx, y from the category XX, and a natural transformation f:xyf\colon x \Rightarrow y between them. Then Λ(1)\Lambda(1) is the free cartesian category on one object \bullet; Λ(x)\Lambda(x) is the functor that replaces each copy of \bullet in a formula like \bullet \multimap \bullet with the object xx, and similarly for Λ(y)\Lambda(y); and Λ(f)\Lambda(f) should be a natural transformation between them that assigns to each object like \bullet \multimap \bullet in Λ(1)\Lambda(1) a morphism

ff:xxyyf\multimap f\colon x \multimap x \to y \multimap y

in Λ(X).\Lambda(X). Such a morphism doesn’t exist, in general, but does if ff is an isomorphism; so Λ\Lambda is 2-monadic over Cat g,Cat_g, the category of small categories, functors, and natural isomorphisms.

Finitary monads over Set correspond to Lawvere theories. Power showed that when a symmetric monoidal biclosed category VV has finite cotensors, finitary VV-monads correspond to VV-enriched Lawvere theories. Let’s set V=Cat gV = Cat_g.

Λ\Lambda is finitary in the sense that any formula is finite, but it looks to me like a Cat gCat_g-enriched Lawvere theory doesn’t have the ability to talk about opposites of objects. Is there some other notion of generalized Lawvere theory that does?

Posted by: Michael Stay on February 13, 2017 11:45 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

To what extent can all study of Groups/Monoids really be reduced to Universal algebra? When I use them I feel like there are 2 “modes”, universal algebra mode, which tells me what monoid homomorphisms and congruences look like, and category mode, which tells me what a monoid action is.

Specifically, is there a definition of “action” of a model of an arbitrary Lawvere theory m:LCm : L \to C on an object in CC? Or is “action” a concept that only really makes sense for enriched Monoid/Group/Category-like things?

Posted by: Max New on February 13, 2017 11:46 PM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

The question about actions is intriguing.

The short answer is that I don’t really know, but there is a notion of module over an algebra over an operad, and Lawvere theories are pretty much the same thing as cartesian operads, in the sense explained for example here (I’m sure there are better references, but then again I am usually not too good giving references). It might be possible putting these two things together, but having just consumed a healthy slug of whisky, I’m not feeling prepared to investigate this at the moment. :-)

Posted by: Todd Trimble on February 14, 2017 3:24 AM | Permalink | Reply to this

Re: The Category Theoretic Understanding of Universal Algebra

A monoid action on a set can be captured with a multisorted Lawvere theory, with

  • objects MM and SS,

  • morphisms

    • m:M×MMm\colon M\times M \to M,

    • e:1Me\colon 1 \to M,

    • a:M×SSa\colon M \times S \to S, and

  • equations

    • mm is associative and unital,

    • a(e,s)=sa(e, s) = s, and

    • a(x,a(y,s))=a(m(x,y),s)a(x, a(y, s)) = a(m(x, y), s).

The last two equations are effectively giving a monoid homomorphism between the model and the endomorphisms on S taking the monoidal product to composition. A category is the structure that captures the notion of what we mean by composition, so that explains to some extent why category-like structures seem to be the things with actions on sets.

A category is a monad in the bicategory of spans in Set, and the action of a category on a set is an algebra for the monad. Generalizing, we can take an arbitrary monad in a bicategory and consider its algebras the actions. The usual finitary monads on Set arising from Lawvere theories live in the bicategory Cat, so we get actions of the theories on categories, not actions of models of the theories on sets.

In particular, given a monad T:SetSetT\colon Set \to Set, an algebra of TT is a functor λ:CSet\lambda\colon C \to Set and a natural transformation ρ:Tλλ\rho\colon T\lambda \Rightarrow \lambda such that

(1)ρTρ=ρμ Tλ. \rho \circ T\rho = \rho \circ \mu^T\lambda.

We think of λ\lambda as picking out the objects of CC sitting over each set and ρ\rho as the action of TT on CC.

Posted by: Michael Stay on February 14, 2017 4:53 PM | Permalink | Reply to this

Post a New Comment