### Context

#### Higher algebra

higher algebra

universal algebra

## 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 $C$ is a category, and write $\mathrm{Mnd}\left(C\right)$ for the category whose objects are monads on $C$ 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:

$\mathrm{Mnd}\left(C\right)\to \mathrm{PtEnd}\left(C\right)\to \mathrm{End}\left(C\right)\to \left[\mathrm{ob}\left(C\right),C\right]$Mnd(C) \to PtEnd(C) \to End(C) \to [ob(C),C]

where $\mathrm{End}\left(C\right)$ denotes the category of endofunctors of $C$, and $\mathrm{PtEnd}\left(C\right)$ denotes the category of pointed endofunctors, i.e. endofunctors $F$ equipped with a natural transformation $\mathrm{Id}\to F$. 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 $C$ 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 $C$ 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:

${\mathrm{Mnd}}_{f}\left(C\right)\to {\mathrm{PtEnd}}_{f}\left(C\right)\to {\mathrm{End}}_{f}\left(C\right)\to \left[\mathrm{ob}\left(C{\right)}_{f},C\right]$Mnd_f(C) \to PtEnd_f(C) \to End_f(C) \to [ob(C)_f,C]

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

For example, the left adjoint to ${\mathrm{Mnd}}_{f}\left(C\right)\to {\mathrm{End}}_{f}\left(C\right)$, 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 $\mathrm{Mnd}\left(C\right)$, not merely those lying in ${\mathrm{Mnd}}_{f}\left(C\right)$. It is, however, generally true that this is the case: free finitary monads are also free monads.

We say that a monad $T$ is algebraically-free on an endofunctor $F$ if the category $T{\mathrm{Alg}}_{\mathrm{mnd}}$ of $T$-algebras (in the sense of algebras for a monad) is equivalent to the category $F{\mathrm{Alg}}_{\mathrm{endo}}$ of $F$-algebras (in the sense of algebras for an endofunctor). N.B.: Any such equivalence must be an isomorphism $T{\mathrm{Alg}}_{\mathrm{mnd}}\cong F{\mathrm{Alg}}_{\mathrm{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.

###### Proof

First observe that for a (perhaps pointed) endofunctor $F$ and a monad $T$, to give a functor $T{\mathrm{Alg}}_{\mathrm{mnd}}\to F{\mathrm{Alg}}_{\mathrm{endo}}$ over $C$ is equivalent to giving a (pointed) transformation $F\to T$, and if $F$ is a monad then such a functor takes values in $F{\mathrm{Alg}}_{\mathrm{mnd}}$ iff the transformation $F\to T$ is a monad morphism. Thus, if $F{\mathrm{Alg}}_{\mathrm{endo}}\cong T{\mathrm{Alg}}_{\mathrm{mnd}}$, then for any other monad $S$, (pointed) transformations $F\to S$ correspond to maps $S{\mathrm{Alg}}_{\mathrm{mnd}}\to F{\mathrm{Alg}}_{\mathrm{endo}}\cong T{\mathrm{Alg}}_{\mathrm{mnd}}$ and hence to monad morphisms $T\to S$, i.e. $T$ is free on $F$.

###### Theorem

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

###### Proof

For any object $x\in C$, the assumptions ensure that the codensity monad of $x$ exists. This is the right Kan extension of $x:1\to C$ along itself, which we write as $⟨x,x⟩$. The universal property of Kan extensions means that for any endofunctor $F$, to give a map $Fx\to x$ (i.e. to make $x$ into an $F$-algebra) is the same as to give a natural transformation $F\to ⟨x,x⟩$. Moreover, one can check that if $F$ is a pointed endofunctor (resp. a monad), then the map $Fx\to x$ is a pointed (resp. monad) algebra iff the corresponding transformation $F\to ⟨x,x⟩$ is a morphism of pointed endofunctors (resp. of monads). Therefore, if $T$ is the free monad on $F$, then applying its universal property in $\mathrm{Mnd}\left(C\right)$ to the monad $⟨x,x⟩$, 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 $\mathrm{Mnd}\left(C\right)$, not just some subcategory of finitary or accessible monads, since $⟨x,x⟩$ 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.)

## References

Revised on February 21, 2013 21:35:22 by Todd Trimble (98.208.182.196)