symmetric monoidal (∞,1)-category of spectra
This general concept has many different specific incarnations, since there are potentially many different such forgetful functors. Suppose is a category, and write for the category whose objects are monads on 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:
where denotes the category of endofunctors of , and denotes the category of pointed endofunctors, i.e. endofunctors equipped with a natural transformation . A free monad can then be considered as a free object relative to any one of these forgetful functors.
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 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 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 preserved filtered colimits, to obtain:
where the subscript denotes restriction to finitary things, and is the set of compact objects of . In this case, all these forgetful functors do have left adjoints, and moreover at least the functors and are monadic. (This is shown in the papers cited below.) The construction is by a convergent transfinite composition.
For example, the left adjoint to , 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 , not merely those lying in . It is, however, generally true that this is the case: free finitary monads are also free monads.
We say that a monad is algebraically-free on an endofunctor if the category of -algebras (in the sense of algebras for a monad) is equivalent to the category of -algebras (in the sense of algebras for an endofunctor). N.B.: Any such equivalence must be an isomorphism , 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.
Any algebraically-free monad is free.
First observe that for a (perhaps pointed) endofunctor and a monad , to give a functor over is equivalent to giving a (pointed) transformation , and if is a monad then such a functor takes values in iff the transformation is a monad morphism. Thus, if , then for any other monad , (pointed) transformations correspond to maps and hence to monad morphisms , i.e. is free on .
For any object , the assumptions ensure that the codensity monad of exists. This is the right Kan extension of along itself, which we write as . The universal property of Kan extensions means that for any endofunctor , to give a map (i.e. to make into an -algebra) is the same as to give a natural transformation . Moreover, one can check that if is a pointed endofunctor (resp. a monad), then the map is a pointed (resp. monad) algebra iff the corresponding transformation is a morphism of pointed endofunctors (resp. of monads). Therefore, if is the free monad on , then applying its universal property in to the monad , 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 , not just some subcategory of finitary or accessible monads, since will not in general be finitary or accessible.
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.)
Free monads on pointed endofunctors play an important role in the construction of cofibrantly generated algebraic weak factorization systems.
Nicola Gambino, Martin Hyland, section 6 of Wellfounded trees and dependent polynomial functors. In Types for proofs and programs, volume 3085 of Lecture Notes in Comput. Sci., pages 210–225. Springer-Verlag, Berlin, 2004 (web)