nLab free monad

Free monads

Free monads

Definition

A free monad is a free object relative to a forgetful functor whose domain is a category of monads.

This general concept has many different specific incarnations, since there are potentially many different such forgetful functors. Suppose CC is a category, and write Mnd(C)Mnd(C) for the category whose objects are monads on CC and whose morphisms are natural transformations commuting with the monad structure maps; i.e. it is the category of monoids in the monoidal category of endofunctors with composition. Then we have a string of forgetful functors:

Mnd(C)PtEnd(C)End(C)[ob(C),C] Mnd(C) \to PtEnd(C) \to End(C) \to [ob(C),C]

where End(C)End(C) denotes the category of endofunctors of CC, and PtEnd(C)PtEnd(C) denotes the category of pointed endofunctors, i.e. endofunctors FF equipped with a natural transformation IdFId\to F. A free monad can then be considered as a free object relative to any one of these forgetful functors.

Free finitary monads

In general, these forgetful functors cannot be expected to have left adjoints, i.e. there will not be a "free monad functor", but individual objects can often be shown to generate free monads. One general case in which this is true is when CC is locally presentable and we consider monads and endofunctors which are accessible, i.e. preserve sufficiently highly filtered colimits. Suppose for the sake of argument that CC is locally finitely presentable (the higher-ary case is analogous). Then we can restrict the above string of forgetful functors to the finitary monads, i.e. those preserving filtered colimits, to obtain:

Mnd f(C)PtEnd f(C)End f(C)[ob(C) f,C] Mnd_f(C) \to PtEnd_f(C) \to End_f(C) \to [ob(C)_f,C]

where the subscript ff denotes restriction to finitary things, and ob(C) fob(C)_f is the set of compact objects of CC. In this case, all these forgetful functors do have left adjoints, and moreover at least the functors Mnd f(C)End f(C)Mnd_f(C) \to End_f(C) and Mnd f(C)[ob(C) f,C]Mnd_f(C) \to [ob(C)_f,C] are monadic. (This is shown in the papers cited below.) The construction is by a convergent transfinite composition.

For example, the left adjoint to Mnd f(C)End f(C)Mnd_f(C) \to End_f(C), shows that there exists a “free finitary monad” on any finitary endofunctor. Note, though, that this does not automatically imply that the “free finitary monad” on a finitary endofunctor is also a “free monad” on that endofunctor, i.e. that as a free object it satisfies the requisite universal property relative to all objects of Mnd(C)Mnd(C), not merely those lying in Mnd f(C)Mnd_f(C). It is, however, true: free finitary monads are also free monads.

Algebraically-free monads

We say that a monad TT is algebraically-free on an endofunctor FF if the category TAlg mndT Alg_{mnd} of TT-algebras (in the sense of algebras for a monad) is equivalent to the category FAlg endoF Alg_{endo} of FF-algebras (in the sense of algebras for an endofunctor). N.B.: Any such equivalence must be an isomorphism TAlg mndFAlg endoT Alg_{mnd} \cong F Alg_{endo}, because the underlying functors from the categories of algebras in each case are amnestic isofibrations. See remarks at the article monadicity theorem on monadicity vis-à-vis strict monadicity.

A priori, being algebraically free is different from being free. However, one can show the following.

Theorem

Any algebraically-free monad is free.

Proof

First observe that for a (perhaps pointed) endofunctor FF and a monad TT, to give a functor TAlg mndFAlg endoT Alg_{mnd} \to F Alg_{endo} over CC is equivalent to giving a (pointed) transformation FTF\to T, and if FF is a monad then such a functor takes values in FAlg mndF Alg_{mnd} iff the transformation FTF\to T is a monad morphism. Thus, if FAlg endoTAlg mndF Alg_{endo} \cong T Alg_{mnd}, then for any other monad SS, (pointed) transformations FSF\to S correspond to maps SAlg mndFAlg endoTAlg mndS Alg_{mnd} \to F Alg_{endo} \cong T Alg_{mnd} and hence to monad morphisms TST\to S, i.e. TT is free on FF.

Theorem

If CC is locally small and complete, then any free monad is algebraically-free.

Proof

For any object xCx\in C, the assumptions ensure that the codensity monad of xx exists. This is the right Kan extension of x:1Cx\colon 1\to C along itself, which we write as x,x\langle x,x\rangle. The universal property of Kan extensions means that for any endofunctor FF, to give a map FxxF x \to x (i.e. to make xx into an FF-algebra) is the same as to give a natural transformation Fx,xF\to \langle x,x\rangle. Moreover, one can check that if FF is a pointed endofunctor (resp. a monad), then the map FxxF x \to x is a pointed (resp. monad) algebra iff the corresponding transformation Fx,xF\to \langle x,x\rangle is a morphism of pointed endofunctors (resp. of monads). Therefore, if TT is the free monad on FF, then applying its universal property in Mnd(C)Mnd(C) to the monad x,x\langle x,x\rangle, we see that it is also algebraically-free.

Notice that this second proof relies crucially on the fact that free monads have a universal property relative to a forgetful functor whose domain is all of Mnd(C)Mnd(C), not just some subcategory of finitary or accessible monads, since x,x\langle x,x\rangle will not in general be finitary or accessible.

Constructions

Perhaps the most general set-theoretically based construction of (algebraically) free monads is the transfinite construction of free algebras. (In type theory, it is natural to use instead higher inductive types.)

Examples

References

Last revised on February 13, 2024 at 15:45:47. See the history of this page for a list of all contributions to it.