nLab
Lawvere's reconstruction theorem

Lawvere’s Reconstruction Theorem

This is a famous result from William Lawvere’s thesis.

A finite products theory or Lawvere theory CC is a category with finite products where all objects are finite products of copies of a given object xx. A model is a functor F:CSetF: C \to Set preserving finite products, and a morphism of models is a natural transformation between such functors. This gives us a category Mod(C)Mod(C) of models of CC.

What is going on here? A model FF is really just a set F(x)F(x) together with a bunch of nn-ary operations coming from the morphisms in CC, satisfying equational laws coming from the equations between morphisms in CC. Any sort of algebraic gadget that’s just a set with a bunch of nn-ary operations satisfying equations can be described using a theory of this sort. For example: monoids, groups, abelian groups, rings… and so on. We can describe any of these using a suitable algebraic theory, and in each case, the category Mod(C)Mod(C) will be the category of these algebraic gadgets.

There is a functor

R:Mod(C)SetR: Mod(C) \to Set

which carries each model FF to the set F(x)F(x). We can think of this as a functor which forgets all the operations of our algebraic gadget and remembers only the underlying set. This should make you desire a left adjoint

L:SetMod(C)L: Set \to Mod(C)

sending each set to the “free” algebraic gadget on this set. Indeed, such a left adjoint exists!

Given this pair of adjoint functors we we can talk about the category of “finitely generated free models” of our theory. The objects here are objects of Mod(C)Mod(C) of the form L(S)L(S) where SS is a finite set, and the morphisms are the usual morphisms in Mod(C)Mod(C). Let us call this category fgFreeMod(C)fg Free Mod(C).

Here is a way to reconstruct CC from its category of finitely generated free models:

Theorem

If CC is a Lawvere theory, CC is equivalent to fgFreeMod(C) opfg Free Mod(C)^{op} (i.e., fgFreeMod(C)fg Free Mod(C) is equivalent to the opposite of the category CC).

Proof

See William F. Lawvere’s Ph.D. thesis, Functorial Semantics of Algebraic Theories.

In other words, you can reconstruct a Lawvere theory from its category of finitely generated free algebras in the simplest manner imaginable: just reversing the direction of all the morphisms!

The above all continues to apply in suitable form even when we replace “finite products” throughout by any other structure given by limits; e.g., “finite limits”, “arbitrary (small) products”, or “arbitrary (small) limits”. (Of course, for each case, we must also look at a correspondingly wider class of “free” models than merely those freely generated on finite sets; specifically, we recover the theory from its representable models, comprising one “freely generated” model for each object of CC). In particular, in the “arbitrary (small) products” case, we can recover the theory from its free models on arbitrary sets. Indeed, in this case LL takes the particularly nice definition L(k)(b)=Hom C(x k,b)L(k)(b) = Hom_C(x^k, b), and, in fact, the adjunction between LL and RR is monadic; that is, Mod(C)Mod(C) is equivalent to the Eilenberg–Moore category of the monad RL()=Hom C(x (),x)RL(-) = Hom_C(x^{(-)}, x), with the functors RR and LL corresponding under this equivalence to the forgetful and free functors of the Eilenberg–Moore construction. In fact, every monad can be seen to arise uniquely in this way, taking CC as the dual of its Kleisli category (automatically a category with small products generated by a single object, as SetSet is a category with small coproducts generated by the single object 11, and the Kleisli category is generated by a left adjoint applied to SetSet); thus, we have a correspondence between monads on SetSet and categories with small products generated by a single object, both equally well representing single-sorted, infinitary algebraic theories, and, in the former setting, the above recoverability result is just the immediate fact that a monad can be recovered from the forgetful functor on its Eilenberg–Moore category (as, indeed, it can of course be recovered from any adjunction giving rise to it).

(This all also works just as well for inescapably multi-sorted theories (that is, even without the restriction that CC be generated by a single object); in this case, we can’t help but recognize that there are multiple forgetful functors from Mod(C)Mod(C) to SetSet, one for each object of CC, each with a corresponding free model on 11 (by the Yoneda lemma), and, again, the theory is recovered as the dual of the category of all these models (by the Yoneda embedding lemma))

Revised on September 9, 2009 03:24:24 by Toby Bartels (71.104.230.172)