13
$\begingroup$

This is a reference request for the following "well-known" theorems in category theory:

  1. There is an equivalence of categories between finitary monads on $\mathbf{Set}$ and finitary Lawvere theories (i.e. single-sorted finite product theories).

  2. There is an equivalence of categories between monads on $\mathbf{Set}$ and infinitary Lawvere theories (i.e. singled-sorted product theories).

  3. The category of models of a finitary/infinitary Lawvere theory is equivalent to the category of algebras of the corresponding monad.

I am not looking for proofs (I have written them up). I am looking for references which actually give proofs, so that I can cite them in a paper (instead of writing up the proof in the paper). Ideally, they should be classical references. I have scrolled through lots of papers which mention the theorems, and most of the time one (or several) of Linton's papers (let's give them letters) are cited:

  • E. Some aspects of equational theories, Proceedings of the Conference on Categorical Algebra, Springer, 1966
  • F. An outline of functorial semantics, Seminar on triples and categorical homology theory, Springer, 1969
  • A. Applied functorial semantics, Seminar on triples and categorical homology theory, Springer, 1969

Sometimes, also the book "Toposes, Triples and Theories" by Barr & Wells is cited.

In E Linton only mentions 2) in the end of section 6, without proof. In fact, Linton proves a characterization theorem of the concrete categories of models of varietal theories (his name for infinitary Lawvere theories), via a version of the first isomorphism theorem, and he only mentions in passing that a combination with Beck's monadicity theorem yields the equivalence to monads (but this detour is actually not necessary to get the equivalence; so this is not the simplest proof anyway).

I do not understand much what is going on in F (I find it very hard to read, also because of the typesetting), but it seems to deal with a much more general situation, and therefore I don't see where 1) or 2) is proven either. This is funny because both in the introduction of the Lecture Notes and in the introduction of A it is claimed that Linton proves 2) in F. Can perhaps someone help me to "decipher" F and explain where 2) is actually proved? The only result which looks similar is Lemma 10.2, but its proof is omitted... Maybe 3) follows from Theorem 9.3, but I don't see how.

The paper A focusses on monadicity criterions, and just mentions 2) in the introduction.

I could not find a proof in the book by Barr-Wells either. They talk about the history of these theorems in section 4.5 and attribute 1) and 2) to Linton's E and F.

I have found references with proofs of more general versions of 1), for example in the enriched case (Nishizawa, Power, Lawvere theories enriched over a general base), but it is probably awkward to cite such a paper for a classical result. I haven't found a published proof of 2) so far. The only thing which comes very close to 2) and 3) is the nlab article on algebraic theories: https://ncatlab.org/nlab/show/algebraic+theory, but the proof is sketchy.

$\endgroup$
1
  • 1
    $\begingroup$ Ivan Di Liberti deleted his answer, but his recommendation "Monads of sets" by Manes is a really good one! $\endgroup$ May 12, 2021 at 18:55

3 Answers 3

10
$\begingroup$

(1, 2, 3) Though Linton's An outline of functorial semantics does contain the essence of the results and proofs of the monad–theory correspondence (see in particular Theorems 8.1 and 9.1 – 9.3), it is true that the terminology and style make it difficult to extract the results as we would expect to see them today. I think it is appropriate to cite this paper as the original reference, though citing the following papers for modern statements would be complementary.

I shall give a brief outline of Linton's development as pertains to the monad–theory correspondence. (I shall use Linton's notation for ease of comparison.) The key lies in the construction of a general semantics–structure adjunction (Theorem 3.1): given a functor $j : A_0 \to A$, there is an adjunction $m^{(j)} : (A_0°/\mathrm{Cat})° \rightleftarrows \mathrm{Cat}/A : s^{(j)}$. One may then identify the fixed points of this adjunction: on the left-hand side, we have what Linton calls clones over $A_0$. This induces an adjunction by restricting to the clones over $A_0$, called the operational semantics–operational structure adjunction (Theorem 4.1).

Recall that the codensity monad of a right adjoint functor is precisely the monad induced by the adjunction. In Theorem 8.1, Linton proves that the Kleisli category of the codensity monad of the forgetful functor from a category of models for a clone coincides with the codomain of the clone, thus establishing that clones over $A_0$ correspond to a class of condensity monads (the class itself is given explicitly, without reference to preservation of colimits as we would expect now). This is stated more explicitly in Lemma 10.2, where it is established also that morphisms of clones correspond to monad morphisms. That this relationship commutes with taking categories of models and algebras is proven in Theorem 9.3 (making use of Theorems 9.1 and 9.2).

The closest statement to the modern monad--theory correspondence is Lemma 10.2. However, due to the generality Linton is working in, the theories in this setting don't look quite the same as we might expect. I think the earliest statement that matches the modern one is given by Dubuc (below).

In the classical setting of algebraic theories, we are concerned with $j : \mathbb F \to \mathrm{Set}$, where $\mathbb F$ is the free cocartesian category on a single object. The clones over $A_0$ are then precisely finitary single-sorted algebraic theories in the modern sense, and the operational semantics–operational structure adjunction sends an algebraic theory to (the forgetful functor from) its category of models in $\mathrm{Set}$.

In the setting of large algebraic theories, we instead take $j : \mathrm{Set} \to \mathrm{Set}$. The clones over $\mathrm{Set}$ are large single-sorted algebraic theories.

(2, 3) As far as I can tell, the earliest reference in which the monad–theory correspondence appears in the modern form is Theorem III of Dubuc's Enriched semantics–structure (meta) adjointness. Dubuc establishes an equivalence between (large) $\mathcal V$-theories and $\mathcal V$-monads on $\mathcal V$, which in particular implies the classical result. The correspondence with all monads, rather than just finitary or $\kappa$-ary, seems to have fallen out of favour, and many modern treatments elide this case.

(1, 3) For the finitary version, the result (again in the enriched setting) appears as Theorems 4.3, 3.4, and 4.2 of Power's Enriched Lawvere theories. I haven't found an earlier reference with proofs.

(1, 2, 3) As far as I am aware, the only paper in which both results follow directly is Lucyshyn-Wright's Enriched algebraic theories and monads for a system of arities: in particular both the finitary and the large monad–theory correspondences follow from Theorems 11.8 and 11.14. Again, this all takes place in the $\mathcal V$-enriched setting.

$\endgroup$
15
  • 1
    $\begingroup$ Sorry, you're right: I swapped 1 and 2 by mistake. Dubuc proves 2 and 3 in Theorem III: the equations (1) and (2) state that the equivalence commutes with taking categories of algebras. I believe that the monads are equivalent follows because taking the codensity monad of a functor means the monad structure is uniquely determined, so it suffices just to check that the left adjoint is correct. (I think there are more elegant proofs of this correspondence, but there's often a trade-off between a classical proof and an elegant one!) $\endgroup$
    – varkor
    May 12, 2021 at 14:00
  • 1
    $\begingroup$ I've added an outline of the relevant steps in Linton's result. It may be appropriate to attribute the modern form of the correspondence to Dubuc. $\endgroup$
    – varkor
    May 12, 2021 at 14:36
  • 1
    $\begingroup$ I may email around to see whether anyone can shed light on the provenance of the precise modern statement. $\endgroup$
    – varkor
    May 12, 2021 at 14:44
  • 1
    $\begingroup$ @MartinBrandenburg: I was looking at the paper again today, and I realised I had overlooked Lemma 10.2, which does establish a relationship between the categories of monads and "theories" (for a suitable notion of theory), and in particular monad morphisms and morphisms of "theories". In this light, I think it is appropriate to attribute the full equivalence to Linton; however, Dubuc's paper is certainly the first that contains the modern monad–theory correspondence (with the modern definition of "theory"). I've updated my answer accordingly. Apologies for the confusion. $\endgroup$
    – varkor
    May 18, 2021 at 19:14
  • 1
    $\begingroup$ Indeed I also mention that Lemma 10.2 in my question, but also that the proof is omitted. And as you say, it is unclear if "theories" there coincide with infinitary Lawvere theories. (With all that being said, I am really confused by F, often also E are cited as a reference for the equivalence. Perhaps it is the right thing to do, but for someone who wants to actually read a proof such a citation is not useful at all.) $\endgroup$ May 18, 2021 at 19:23
8
$\begingroup$

1 and 3 are proved in Appendix A of the book “Algebraic theories” by Jiří Adámek, Jiří Rosický, Enrico M. Vitale.

1 is Theorem A.37 (and A.41 for the multisorted version).

3 is Theorem A.21 (and A.40 for the multisorted version).

$\endgroup$
8
  • $\begingroup$ In my copy of the book, 1 is Theorem A.38 (Theorem A.42 for multisorted); and 3 is Theorem A.21 (Theorem A.41 for multisorted). (Perhaps there are different editions.) $\endgroup$
    – varkor
    May 11, 2021 at 10:51
  • 3
    $\begingroup$ @varkor: The numeration in the published book has changed compared to the preliminary draft people.math.rochester.edu/faculty/doug/otherpapers/… $\endgroup$ May 11, 2021 at 15:05
  • $\begingroup$ Thank you! Theorem A.21 uses Birkhoff's variety theorem. Since this detour is not necessary, I wonder if it would still have some value to keep the proof in the paper. $\endgroup$ May 12, 2021 at 8:06
  • 2
    $\begingroup$ @MartinBrandenburg: Since the proofs are already written up, I think it is fine to keep them in an appendix or something. A self-contained reference (including part 2) would be useful. $\endgroup$ May 12, 2021 at 15:32
  • 1
    $\begingroup$ @MartinBrandenburg: Thanks for doing this, it is surprising that an elementary proof has not been written up before. The proof of Theorem A.6 is 3 pages long, it may be beneficial to split it. $\endgroup$ Jun 22, 2021 at 18:51
2
$\begingroup$

A detailed, self-contained and beginner-friendly proof of both theorems can now be found in my new paper on limit sketches in the appendix.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.