41.05.02 · category-theory / monads-algebras

Beck's Monadicity Theorem and Lawvere Theories

shipped3 tiersLean: none

Anchor (Master): Mac Lane 1998 *Categories for the Working Mathematician* 2e (Springer GTM 5) Ch. VI §6-8 in full (monadicity, the precise creation-of-coequalisers conditions, the Lawvere-theory presentation of finitary algebraic theories); Adámek-Rosický-Vitale 2011 *Algebraic Theories* (Cambridge LMS 184) Ch. 1-3, 9-11 (Lawvere theories, the monad-theory equivalence, operads); Lawvere 1963 *Functorial Semantics of Algebraic Theories* (Columbia thesis); Borceux 1994 *Handbook of Categorical Algebra 2* (Cambridge) Ch. 4

Intuition Beginner

The previous unit took an adjunction apart and read off a monad — the bookkeeping of a wrapping machine, with a rule for putting an item into its simplest package and a rule for flattening a package of packages. It also built, from any monad, a category of algebras: the things that know how to unpack their own wrapping. The natural follow-up question is the reverse one. You are handed a category sitting on top of plain sets by a forgetting map — groups forgetting to their sets, say. Is that category secretly nothing but the algebras of some wrapping machine? When the answer is yes, the whole category is recovered from one monad.

A surprisingly large family of everyday categories passes this test. Groups, rings, modules over a ring, and — strikingly — compact Hausdorff spaces are each, up to renaming, the algebras of a single wrapping machine over plain sets. A handful of familiar categories fail the test, and the failures are informative: topological spaces in general, and ordered sets, do not arise this way.

The second half of this unit gives a second, more hands-on way to say the same thing. An algebraic gadget like "group" is really a list of operations (a multiplication, an inverse, a unit) together with equations they must satisfy (the laws). Packaging that list of operations-and-laws as a small bookkeeping object, and reading a group as an honest assignment of meaning to each operation, turns out to be exactly equivalent to the wrapping-machine picture.

Visual Beginner

Picture two side-by-side worlds joined by a downward forgetting arrow: a richer world of structured things on top, plain sets on the bottom. The monadicity question asks whether the top world can be rebuilt out of the bottom world plus a single wrapping rule.

The test has three checkpoints, drawn as three gates the forgetting arrow must pass through.

checkpoint what it asks of the forgetting arrow passes for groups?
has a builder there is a free-construction partner going back up yes, the free group
no fake sameness if two structured things look identical below, they were identical above yes
flattening descends a certain "collapse" computed below can always be lifted back up yes

The right-hand panel shows the second picture: a small object listing the operations and laws of "group", and an assignment that reads each operation into a chosen set. Both panels describe the same recognition; the left says it with a wrapping machine, the right with a list of operations.

Worked example Beginner

Take the forgetting arrow from groups down to sets, and walk the first checkpoint by building the free group on a one-element set .

Step 1. Start below, with the one-element set . The builder forms all the words you can spell from and its inverse, with cancellation: , , , the empty word , then , , and so on. Cancellation means collapses to the empty word.

Step 2. Read off the underlying set of this free group. The reduced words are exactly — one for each whole number, counting how many 's (negative for inverses). So the free group on one generator is the integers under addition.

Step 3. Check the no-fake-sameness checkpoint on a small case. The two-element flip group and the three-element rotation group have underlying sets of sizes and . Different sizes below force different groups above; and even two groups of the same size with different multiplication tables are told apart by their tables, which the forgetting arrow does not erase in a way that merges them.

What this tells us: the forgetting arrow from groups to sets has a genuine builder (the free group), and it does not glue together groups that were actually different. These are two of the three checkpoints that, taken together, certify groups as the algebras of one wrapping machine over sets.

Check your understanding Beginner

Formal definition Intermediate+

Throughout, is a functor with a left adjoint , unit and counit , inducing the monad with multiplication as in 41.05.01. Write for the Eilenberg-Moore category and , , for the comparison functor, the unique functor over with (the Master tier of 41.05.01).

Definition (monadic functor). The functor is monadic, and the adjunction a monadic adjunction, when the comparison functor is an equivalence of categories. Then over : the category is, up to equivalence, the algebras for [Mac Lane 1998].

Definition (split coequaliser). A split coequaliser of a parallel pair is a map together with sections and satisfying $$ e f = e g,\qquad e s = \mathrm{id}_E,\qquad f t = \mathrm{id}_B,\qquad g t = s e. $$ These equations force to be a coequaliser of , and the configuration is preserved by every functor, since it is a finite list of composite-equations: a split coequaliser is an absolute coequaliser. A pair in is -split if its image in admits a split coequaliser; equivalently the pair is sent by to a pair carrying a coequaliser preserved by all functors out of .

Definition (creation of coequalisers). A functor creates coequalisers of -split pairs if, whenever in is -split with chosen split coequaliser in , there is a unique pair in with , , and is a coequaliser of in . A functor reflects isomorphisms if invertible forces invertible.

Definition (reflexive pair). A parallel pair is reflexive if it has a common section with . Reflexive coequalisers occur throughout algebra: the presentation of an algebra by generators and relations is the coequaliser of a reflexive pair of free algebras.

The free-forgetful adjunctions assemble the standard gallery of monadic functors. The forgetful functors , , , , and are all monadic; so is from compact Hausdorff spaces, whose monad is the ultrafilter monad , an arresting fact since compactness is a topological notion with no operations in sight. The forgetful is not monadic — it has a left adjoint (the discrete topology) but is not a category of algebras; nor is . Notation introduced here ( for the comparison functor, for the ultrafilter monad, for the theory below) is recorded in _meta/NOTATION.md.

Counterexamples to common slips Intermediate+

  • Reflecting isomorphisms is not the same as being faithful. The forgetful is faithful and even reflects identities on underlying maps, yet it does not reflect isomorphisms: a continuous bijection (a finer topology mapping to a coarser one) is sent to an invertible set map but is itself not invertible. This single failure already shows is not monadic over .

  • -split is strictly weaker than split in . Beck's theorem requires creation of coequalisers only for pairs whose image splits below, in — not for pairs split in . This is what makes the criterion usable: the splitting need not lift, only the coequaliser.

  • A left adjoint and faithfulness do not suffice. (underlying graph of a category) has a left adjoint and reflects isomorphisms, but is not monadic, because it fails to create the relevant coequalisers; conversely the inclusion of a reflective subcategory is always monadic (its monad is idempotent), so monadicity is genuinely the conjunction of all three Beck conditions, not any one of them.

Key theorem with proof Intermediate+

The signature result is Beck's monadicity theorem: a finite checklist on decides whether the comparison functor is an equivalence, so whether is a category of algebras.

Theorem (Beck's monadicity theorem). A functor is monadic if and only if (i) has a left adjoint, (ii) reflects isomorphisms, and (iii) creates coequalisers of -split pairs [Beck 1967].

Proof. For necessity, suppose is monadic, so up to equivalence . It has the left adjoint . It reflects isomorphisms: an algebra morphism with invertible in has inverse which is automatically an algebra morphism, since . And creates coequalisers of -split pairs: given a -split pair of algebra maps with split coequaliser in , the splitting data is absolute, so preserves the coequaliser; the structure map on then descends along to a unique structure map on making an algebra map, and this is the unique lift, a coequaliser in .

For sufficiency, assume (i)-(iii). The comparison satisfies and . Each algebra presents itself as a -split coequaliser of free algebras: the pair has -split coequaliser in , with splitting and — the standard bar presentation. Applying on the underlying -split pair in : the pair is -split (its image is the split coequaliser above), so by (iii) it has a coequaliser in with . Sending defines a functor , and the created-coequaliser uniqueness gives natural isomorphisms and ; here (ii) is used to upgrade the comparison maps to isomorphisms in . Hence is an equivalence and is monadic.

Bridge. This theorem builds toward the recognition of entire mathematical categories as algebraic, and appears again in the Master tier as the engine identifying , , and with Eilenberg-Moore categories. The foundational reason the three conditions suffice is that every algebra is canonically a -split coequaliser of free algebras — the bar resolution — so creating exactly those coequalisers reconstructs every algebra from free ones, which the comparison functor already handles. This is exactly the converse direction to the monad-of-an-adjunction theorem of 41.05.01: there an adjunction produced a monad, here a checklist decides when the adjunction is recovered from that monad. The criterion generalises the reflective case of 41.03.02, where the inclusion of a reflective subcategory is always monadic because its monad is idempotent and the descent is automatic; and it is dual to a comonadicity criterion recognising categories of coalgebras. Putting these together, the central insight is that "is monadic", "creates -split coequalisers and reflects isomorphisms", and "every object is a canonical colimit of free objects" name one condition from three sides, and the bridge is that this same colimit-of-free-objects idea, made syntactic, becomes the Lawvere-theory presentation co-developed with the Kan and codensity material of 41.06.02.

Exercises Intermediate+

Advanced results Master

Theorem (Beck, precise form). is monadic if and only if has a left adjoint, reflects isomorphisms, and for every parallel pair in whose -image has a split coequaliser, that pair has a coequaliser preserved by and reflected as a colimit by [Beck 1967]. The reflexive variant weakens "-split" to "reflexive", at the cost of requiring to have and to preserve reflexive coequalisers; the crude variant drops the absoluteness and asks to preserve and reflect those coequalisers outright. Each variant proves monadicity by reconstructing every algebra as the coequaliser of the bar presentation , the canonical -split (and reflexive) pair whose coequaliser is the algebra.

Theorem (the algebraic gallery is monadic). The forgetful functors from , , , , , , , and every variety of finitary algebras to are monadic, because each has free objects (so a left adjoint), reflects isomorphisms (a bijective homomorphism is an isomorphism of algebras), and creates reflexive coequalisers, which exist in any variety as quotients by a congruence. The forgetful is monadic with monad the ultrafilter (codensity) monad : a -algebra is a set with an ultrafilter-convergence map satisfying the unit and associativity laws, and Manes's theorem identifies these algebras with compact Hausdorff spaces, recovering . The non-examples are equally structural: and fail to reflect isomorphisms, and fails the creation condition.

Theorem (Lawvere theories present finitary monads). A Lawvere theory is a small category with finite products in which every object is a finite power of a distinguished object , equipped with the chosen product structure; a model of is a finite-product-preserving functor , and the models form the category with the forgetful functor . The maps in are the -ary operations of the theory and the commuting diagrams are the equational laws. There is an equivalence of categories $$ {\text{Lawvere theories}}\ \simeq\ {\text{finitary monads on }\mathbf{Set}}, $$ under which and the forgetful functors agree [Lawvere 1963]. A finitary monad is one whose endofunctor preserves filtered colimits; equivalently it is determined by its values on finite sets, which are the free models on finitely many generators. Thus "model of an equational theory" and "algebra for a finitary monad" name the same objects, and Beck's theorem certifies that the syntactic category really is the algebras of its monad.

Theorem (the category of monads and monad maps). Monads on a fixed form a category : a monad morphism is a natural transformation with and , and each such induces a functor over — contravariantly on algebras. Restricting to finitary monads on , is equivalent to the category of Lawvere theories and finite-product-preserving functors between them; a theory map is a translation of one equational theory into another, and the induced algebra functor is the resulting forgetful-along-translation. Symmetric operads and PROPs sit inside this picture as theories with restricted variable usage: an operad is a Lawvere theory in which operations may not duplicate or discard inputs, presenting the strongly regular equational theories.

Synthesis. Putting these together, monadicity is the precise sense in which a category "is algebra over a base", and Beck's three conditions are the bridge that turns the monad-of-an-adjunction construction of 41.05.01 into a recognition theorem: a left adjoint and a reflection property and the creation of exactly the -split coequalisers that present every algebra as a colimit of free ones. This is exactly the colimit-of-free-objects principle made into a criterion, and it generalises the reflective case of 41.03.02, where idempotency makes the descent automatic, while shows the criterion reaching past visibly algebraic categories to the ultrafilter monad, where compactness is revealed as an algebraic structure. The Lawvere-theory equivalence is dual to the monad presentation in the precise sense that a theory is the syntax — operations and laws assembled into a category with finite products — and the monad is the semantics — the endofunctor whose algebras are the models; the foundational reason the two agree is that the finitary monad is the left Kan extension along of the theory's action on finite sets, the codensity-and-Kan thread of 41.06.02. The central insight is that "monadic functor", "variety of algebras", "models of a Lawvere theory", and "algebras for a finitary monad" are one notion seen as recognition criterion, as classical universal algebra, as functorial syntax, and as categorical semantics, with Birkhoff's variety theorem the classical shadow of the monad-theory equivalence.

Full proof set Master

Proposition 1 (split coequalisers are absolute and are coequalisers). A split coequaliser of is a coequaliser, and is preserved by every functor.

Proof. Given with , set . Then , using , then , then . If then by , so the mediating map is unique and . For absoluteness, a functor sends the four defining equations to the same equations for , so is a split coequaliser of , hence a coequaliser.

Proposition 2 (every algebra is the absolute coequaliser of its bar presentation). For , the pair has the split coequaliser with sections .

Proof. Put , , . The algebra associativity law is . The algebra unit law is . The monad right-unit law is . Naturality of at gives , that is . By Proposition 1 this is an absolute coequaliser.

Proposition 3 (sufficiency of Beck's conditions). If has left adjoint , reflects isomorphisms, and creates coequalisers of -split pairs, then the comparison is an equivalence.

Proof. For , the pair in has -image — using and — whose split coequaliser is by Proposition 2. By the creation hypothesis there is a unique object and coequaliser with and . Functoriality of follows from uniqueness of created coequalisers applied to algebra morphisms. Now where is forced equal to because presents the structure map; so . Conversely for , the counit exhibits as the coequaliser of the -split pair , whose image splits via ; creation gives with a comparison map over an isomorphism in , which reflects to an isomorphism in . Hence and is an equivalence.

Proposition 4 (necessity of Beck's conditions). If is monadic then it has a left adjoint, reflects isomorphisms, and creates coequalisers of -split pairs.

Proof. Transport along the equivalence ; it suffices to treat . The left adjoint is . If has invertible in , then is an algebra morphism since , so is an isomorphism in : reflects isomorphisms. For creation, let a pair of algebra maps have -split coequaliser in with splitting data. Absoluteness (Proposition 1) makes and preserve , so the structure map coequalises and factors uniquely through as a map making an algebra and an algebra coequaliser; uniqueness of the factorisation is exactly the unique lift. So creates these coequalisers.

Proposition 5 (models of a Lawvere theory are the algebras of its monad). For a Lawvere theory there is a finitary monad on with over , and the forgetful functor is monadic.

Proof. The forgetful functor , , has a left adjoint sending a set to the free model evaluated on , i.e. the model of -terms in variables from ; this is because a model map out of the free model is determined by the images of the generators. So is a monad, finitary because a -term uses finitely many variables, so preserves filtered colimits. Now reflects isomorphisms (a model map that is a bijection on underlying sets has inverse a model map, as products are computed in and preserved), and has reflexive coequalisers computed underlying-set-wise and preserved by (a quotient of a model by a model congruence is a model, since finite products commute with reflexive coequalisers in ). By the reflexive monadicity variant (Proposition 3 applied to reflexive pairs) is monadic, so over . The assignment is full and faithful onto finitary monads, with inverse sending to the theory whose -ary operations are the elements of — the equivalence of categories.

Connections Master

  • Monads, Eilenberg-Moore, and Kleisli 41.05.01. This unit answers the recognition question left open in 41.05.01: there an adjunction produced a monad and the comparison functor into was defined; here Beck's theorem says exactly when that comparison is an equivalence, so when the adjunction is — up to equivalence — the free-forgetful adjunction of its own monad. The bar presentation that drives the proof is the canonical -split coequaliser built from the unit and multiplication introduced there.

  • RAPL, reflective subcategories, and the adjoint functor theorems 41.03.02. Reflective inclusions are precisely the monadic functors whose monad is idempotent, so the reflective-localisation theory of 41.03.02 is the degenerate case of monadicity where every object carries at most one algebra structure and descent is automatic; the adjoint functor theorems supply the left adjoints whose monadicity this unit then tests, and — produced by the Special Adjoint Functor Theorem there — is monadic here via the ultrafilter monad.

  • Kan extensions and the codensity monad 41.06.02. A finitary monad on is the left Kan extension along of a Lawvere theory's action on finite sets, so the monad-theory equivalence is a Kan-extension statement; the ultrafilter monad presenting is the codensity monad of the inclusion of finite sets, the construction developed in the co-produced 41.06.02, where the comparison functors of this unit reappear as universal arrows into a Kan extension.

  • Natural transformations and the endofunctor category 41.01.02. A monad morphism is a natural transformation between endofunctors compatible with the monoid structures of 41.01.02, so the category of monads lives inside the endofunctor category there, and a Lawvere-theory translation is exactly such a monad morphism between the finitary monads, inducing the forgetful-along-translation functor on algebras.

  • Limits, colimits, and their construction 41.02.01. Monadicity is detected by the creation of a specific class of coequalisers, tying the recognition of algebraic categories to the colimit theory of 41.02.01; the reflexive coequalisers that compute quotients in a variety, and the absolute coequalisers of the bar resolution, are the precise colimits whose creation Beck's criterion demands, while the algebra category inherits all limits from along the monadic forgetful functor.

Historical & philosophical context Master

The monadicity question crystallised in Jonathan Beck's 1967 Columbia thesis Triples, Algebras and Cohomology [Beck 1967], which isolated the creation-of-split-coequalisers condition now bearing his name and proved the precise characterisation of categories of algebras. The theorem was circulated in the Eilenberg-school "triples" idiom of the period and reached its standard textbook form in Mac Lane's Categories for the Working Mathematician (1971; 2nd ed. 1998) [Mac Lane 1998], Chapter VI, alongside the comparison functor and the Eilenberg-Moore resolution. The recognition that compact Hausdorff spaces are the algebras of the ultrafilter monad was established by Ernest Manes in 1969 and independently informed by Eduard Čech's and Marshall Stone's earlier compactification work, supplying the most striking example of a non-syntactically-algebraic category that is nonetheless monadic.

The theory side descends from William Lawvere's 1963 Columbia thesis Functorial Semantics of Algebraic Theories [Lawvere 1963], which reconceived an equational theory as a category with finite products and a model as a product-preserving functor, replacing the symbol-pushing of universal algebra with a coordinate-free categorical object. The equivalence between Lawvere theories and finitary monads on was developed by Fred Linton in 1966 and connects to Garrett Birkhoff's 1935 variety theorem — the HSP characterisation of equationally definable classes — which becomes the classical shadow of the monad-theory correspondence. The operad and PROP refinements, isolating theories with restricted variable usage, were introduced by J. Peter May and Saunders Mac Lane in the early 1970s and systematised in the algebraic-theories literature of Adámek, Rosický, and Vitale.

Bibliography Master

@phdthesis{Beck1967mon,
  author = {Beck, Jonathan M.},
  title  = {Triples, Algebras and Cohomology},
  school = {Columbia University},
  year   = {1967}
}

@book{MacLane1998mon,
  author    = {Mac Lane, Saunders},
  title     = {Categories for the Working Mathematician},
  edition   = {2},
  publisher = {Springer},
  series    = {Graduate Texts in Mathematics 5},
  year      = {1998}
}

@phdthesis{Lawvere1963,
  author = {Lawvere, F. William},
  title  = {Functorial Semantics of Algebraic Theories},
  school = {Columbia University},
  year   = {1963},
  note   = {Summary in Proc. Nat. Acad. Sci. USA 50 (1963) 869--872}
}

@article{Manes1969,
  author  = {Manes, Ernest G.},
  title   = {A triple theoretic construction of compact algebras},
  journal = {Lecture Notes in Mathematics},
  volume  = {80},
  year    = {1969},
  pages   = {91--118}
}

@article{Linton1966,
  author  = {Linton, F. E. J.},
  title   = {Some aspects of equational categories},
  journal = {Proceedings of the Conference on Categorical Algebra (La Jolla 1965)},
  year    = {1966},
  pages   = {84--94},
  publisher = {Springer}
}

@article{Birkhoff1935,
  author  = {Birkhoff, Garrett},
  title   = {On the structure of abstract algebras},
  journal = {Proceedings of the Cambridge Philosophical Society},
  volume  = {31},
  number  = {4},
  year    = {1935},
  pages   = {433--454}
}

@book{AdamekRosickyVitale2011,
  author    = {Ad\'amek, Ji\v{r}\'i and Rosick\'y, Ji\v{r}\'i and Vitale, Enrico M.},
  title     = {Algebraic Theories: A Categorical Introduction to General Algebra},
  publisher = {Cambridge University Press},
  series    = {Cambridge Tracts in Mathematics 184},
  year      = {2011}
}