nLab
free monad

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}(C)$ 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}(C)\to \mathrm{PtEnd}(C)\to \mathrm{End}(C)\to [\mathrm{ob}(C),C]$$Mnd(C) \to PtEnd(C) \to End(C) \to [ob(C),C]

where $\mathrm{End}(C)$ denotes the category of endofunctors of $C$, and $\mathrm{PtEnd}(C)$ 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.

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 $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(C)\to {\mathrm{PtEnd}}_f(C)\to {\mathrm{End}}_f(C)\to [\mathrm{ob}(C{)}_f,C]$$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}(C{)}_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(C)\to {\mathrm{End}}_f(C)$ and ${\mathrm{Mnd}}_f(C)\to [\mathrm{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 ${\mathrm{Mnd}}_f(C)\to {\mathrm{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 $\mathrm{Mnd}(C)$, not merely those lying in ${\mathrm{Mnd}}_f(C)$. It is, however, generally true that this is the case: free finitary monads are also free monads.

Algebraically-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.

Theorem

Any algebraically-free monad is free.

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}(C)$ 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}(C)$, 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.)

Examples

• The monadicity of the above adjunctions can be used to give presentation?s of monads in terms of generators and relations. This has close connections with Lawvere theories and related ideas.

• Free monads on pointed endofunctors play an important role in the construction of cofibrantly generated algebraic weak factorization systems.

Related concepts

• The algebra over a monad over a free monad on an endofunctor is an algebra over an endofunctor.

References

• Max Kelly, “A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on”

• Max Kelly and John Power, “Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads”

• Steve Lack, “On the monadicity of finitary monads”