Practical Foundations of Mathematics

Paul Taylor

7.5  Monads

Monads are the view of adjunctions which we get by looking at them from one end, generalising closure operations from Section 3.7. They describe (single-sorted) finitary equational theories, but also characterise many apparently unalgebraic categories as categories of infinitary algebras.

Let F\dashv U be an adjunction and put M = U·F. Then the natural transformation m = e·F (the multiplication) makes the following diagrams commute, by the triangle laws (Definition  7.2.1) and naturality of e.

omitted diagram environment

DEFINITION 7.5.1 A triple consisting of a functor M:S® S and natural transformations h:\idS® M and m:M2® M that obey these laws is called a monad.

REMARK 7.5.2 Algebras for functors have arisen in informatics, and algebras for monads in categorical algebra, so the uncritical reader of abstract accounts of these separate topics is in danger of making inappropriate value-judgements. Functors and monads can both be used to code the same (free) theory, but in different ways:

(a)
The functor T is the analogue of Lemma  3.7.10, which coded a system of closure conditions. It is dynamic: we can watch the genesis of the free algebra from its well founded coalgebras (Section  6.3), and there is an associated notion of recursion.

(b)
The monad (M,h,m) generalises the closure operation and is static: the construction of the free algebra is already finished.

In particular, MX is much bigger than TX, and may be a proper class if, for example, T = P.

We shall only consider single-sorted theories (as before, for many-sorted theories we must work in SetS ), and start with a free algebraic theory in the sense of Section 6.1, presented as a functor T. Let \LeftAdjoint0X be the free T-algebra on X, with inclusion hX:X® \Monad0X, where \Monad0 = U·\LeftAdjoint0. Then (\Monad0,h,m) is a monad, for a certain natural transformation m.

For example, let T = {1} +(-)2 and X = {a,b}. Then \Monad0X contains

1    a    b    ab    ba    \arga1    1a    11    (ab)a    a(ba)    ¼,
in which we use (round) parentheses in the usual way to disambiguate non- associative operations. Then M20X consists of terms in generators from \Monad0X, which we may think of as [square] bracketed terms:
1    [1]    [a]    [ab]    [ba]    [b][a]    [a]1    [\arga1]    [ab]a    [a] æ
è
[b][ab] ö
ø
.
Then mX º e\LeftAdjoint0X removes the square brackets to give plain terms.

A monad is needed to code laws. For a T-algebra \evA:TA® A, the map eA:\Monad0A® A constructed in Example  7.4.6 evaluates terms of arbitrary depth, whereas \evA only handles those of depth 1. The more comprehensive structure is needed to test whether A satisfies the laws of an equational theory of which T is the signature, as these laws may be between terms of any depth. But even for a free theory, eA must satisfy certain conditions if it is given by some \evA.

The Kleisli and Eilenberg-Moore categories   All monads arise from adjunctions, in fact in two different ways, both found in 1965.

PROPOSITION 7.5.3 Let (M,h,m) be a monad on a category S.

(a)
The Kleisli category \Kleisli (M,h,m) has the same objects as S, but its maps X® Y are the S- maps X® MY; the Kleisli identity on X is hX and the composite of f:X® MY with g:Y® MZ is f;Mg;mZ ( cf Exercise 3.38 for preorders). There is an adjunction, omitted diagram environment with co-unit eX = \idMX, and this induces the given monad.

(b)
An algebra is an S-map a:MA® A such that omitted diagram environment cf fixed points for closure operations (Section  3.7). Although this is a more complicated notion of algebra than that in Section 6.1, the definition of homomorphism f:(A,a)® (B,b) is the same: an S-map f:A® B such that a;f = Mf; b. They constitute the Eilenberg-Moore category, Mod(M,h,m). The forgetful functor \RightAdjoint EM has a left adjoint, \LeftAdjointEM:X® (MX,mX), and e(A,a) = a is the co-unit. These also induce the given monad.

(c)
Let U:A® S with F\dashv U be any adjunction (with co-unit e and transposition l) giving rise to this monad. Then there are unique functors making the triangles commute: omitted diagram environment K takes the Kleisli morphism g:X® MY to l-1(g ):FX® FY, and, for A Î obA, E(A) is the algebra eA: UFUA® UA. []

DEFINITION 7.5.4 An adjunction F\dashv U (or just the functor U) for which the functor E is a weak equivalence is said to be monadic.

EXAMPLES 7.5.5

(a)
Vsp is the Eilenberg-Moore category for the monad on Set induced by the adjunction in Example  7.1.4(b). The Kleisli category consists of those vector spaces that have bases (which is all of them, given the axiom of choice).

(b)
Rel\hookrightarrow CSLat are (equivalent to) the Kleisli and Eilenberg-Moore categories for the covariant powerset monad (P,{-},È) on Set.

(c)
The following Kleisli, co-Kleisli and Eilenberg-Moore adjunctions arise from lifting in domain theory (Remark  3.4.5, Definition  3.3.7 and Example 3.9.8(c)), where Lift(-)- homomorphisms are continuous functions that also preserve ^. omitted diagram environment Classically, every Lift(-)-algebra (or ipo) A is LiftX, for X = A\{^} , so the middle adjunction above is also Kleisli.

(d)
Any single-sorted finitary algebraic theory L gives rise to a monad on Set, for which the Eilenberg-Moore category is  Mod(L). The Kleisli category consists of the free algebras on any set of generators. Restricting to finite such sets, we obtain (Cn×L)op, cf Corollary 3.9.5.

(e)
Exercises 4.27 and 7.41 show how some cartesian closed categories of domains arise as co-Kleisli categories of monads on symmetric monoidal closed categories.

Beck's theorem   The importance of monadic adjunctions lies in the fact that universal constructions with algebras may be computed for the carriers, so long as the two structures commute. Jon Beck's theorem was presented at a conference in 1966 but he never wrote it up for publication.

PROPOSITION 7.5.6 The forgetful functor Mod(M,h,m)® Set creates all small limits (Definition  4.5.10), and whatever colimits M preserves.

omitted diagram environment

PROOF: The structure map for the (co)limit algebra is the mediator a to limi\typeAi or from \colimiM\typeAi shown dotted. Similarly the Eilenberg-Moore equations h;a = id and Ma;a = m;a hold because both sides are mediators to limi\typeAi or from \colimiM\typeAi or \colimiM2\typeAi. []

This property is characteristic, as we can see from a special case:

REMARK 7.5.7 [Bob Paré] Consider contractible coequalisers (Exercise 5.2). Such coequalisers exist in any category S where idempotents split, and they are preserved by all functors out of S, in particular by M.

An algebra for the monad (by definition) makes the two squares below commute and the rows identities (recall that Z indicates a naturality square). It is a contractible coequaliser.

omitted diagram environment

The contraction hMA is not a homomorphism: the coequaliser diagram for the algebras only becomes contractible when we apply the forgetful functor U. Such a parallel pair of homomorphisms \nearrow ,r:C\rightrightarrows B for which there is some S-map \:B®C with \;\nearrow = \idB and \nearrow ;\;r = r;\;r is called a U-contractible coequaliser.

Notice in particular that the structure map of any algebra a:FA® A is the coequaliser of Fa and mA not only in S but also in the category of algebras and homomorphisms, so it is a self- presentation.

EXAMPLE 7.5.8 For the discrete\dashv points adjunction (Theorem  7.4.1), the maps Fa and mA are both the identity on the underlying set of A equipped with the discrete topology, so the original topology on the space A is not recovered as a coequaliser.

THEOREM 7.5.9 [Jon Beck] Let F\dashv U between categories in which idempotents split (Exercise 4.16). Then the following are equivalent:

(a)
the adjunction is monadic,

(b)
U creates whatever colimits M preserves: for any diagram Á® A, if M preserves the colimit of Á ® A® C, then U creates the colimit of Á® A;

(c)
U creates U-contractible coequalisers.

The comparison functor is full and faithful (and in particular reflects invertibility) iff every eA is a self-presentation.

PROOF: To show that E is full and faithful, let g:UA® UB in S. There is a unique f with g = Uf iff the top row is a coequaliser in A:

omitted diagram environment

For essential surjectivity, let a:UFX® X be an algebra. Then Fa and eFX form a U-contractible pair in A, whose coequaliser A (created by U) gives rise to the algebra E(A) º (X,a). []

EXAMPLES 7.5.10

(a)
Reflective subcategories are always monadic, with invertible m: we call the monad idempotent. (By Corollary  7.2.10(b), e is invertible and the forgetful functor is full and faithful, so the contraction in S is already a morphism of the category A).

(b)
U:Mod(T)® Set creates whatever colimits T preserves, by the same argument as for Proposition  7.5.6, so it is monadic. Hence the functor and monad have the same algebras, and we also justified this name in terms of multiplication tables in Definition 6.1.1.

(c)
When does a:\Monad0A® A satisfy the laws of an equational theory L? As in Theorem  7.4.4, they can be stated as the equality of composites R\rightrightarrows \Monad0A® A. However, we already know the coequaliser of this pair: it is the free L-algebra FA on A. Hence a:MA® A is an M-algebra iff \Monad0A \twoheadrightarrow MA® A is an L0-algebra satisfying the laws.

(d)
(Bob Paré) Setop @ Mod(M, h,m), where this monad arises from the symmetric self-adjunction of Example 7.1.9(b) with S = W, ie the contravariant powerset. Monadicity in this case is a consequence of the Beck-Chevalley condition for the quantifiers (Remarks 9.3.7 and 9.4.3). From the definition of an elementary topos as having finite limits and powersets, it follows immediately that it has finite colimits, though the resulting constructions are more complicated than those in Section 2.1. Indeed toposes have products and sums of the same shapes, Proposition 9.6.13 and [BW85, Section 5.1].

Applications   We came to monads from finitary algebraic theories. The types analogue of Theorem 3.9.4 and Exercise  3.37 is

PROPOSITION 7.5.11 Every finitary monad on Set, ie for which M preserves filtered colimits, is isomorphic to that given by the free algebras for some single-sorted finitary algebraic theory L, and then Mod(L) is externally locally finitely presentable (Definition 6.6.14(c)).

PROOF: We shall describe the Lawvere theory (Exercise  4.29). The set of k-ary operation-symbols is Cn×L(k,1) = Mk. The composition

(Mn)kx(Mk) = Cn× L(n,k) xCn×L( k,1) ® Cn×L(n ,1) = Mn,
which determines how to apply a k-ary operation-symbol to arguments, is the effect of the adjoint transposition f® p:

omitted diagram environment

The multiplication m thereby captures the laws of L ( cf saturation for closure conditions). For a finite set n, the value at n of the monad derived from the theory L is the carrier of the free algebra on n generators, which is Cn×L(n,1) = Mn as required, and similarly for functions between finite sets. Since every set is a filtered colimit of finite(ly presented) sets (Exercise 7.21) and M preserves filtered colimits, M is determined up to unique isomorphism by its values Mn, so it agrees with the monad arising from L. Again since M preserves filtered colimits, U creates them; F preserves finite presentability, and Mod(L) is LFP. []

As we have repeatedly pointed out, infinitary algebraic theories with arbitrary laws present problems when we reject the Axiom of Choice. Fred Linton developed monads as a useful alternative, showing that the symbolic and diagrammatic notions are equivalent in the presence of Choice [Lin69 ]. Monads can give an unexpected algebraic perspective on topology: for example the category of compact Hausdorff spaces is monadic over  Set, the left adjoint being the space of ultrafilters. See [ Man76] for this and a monadic treatment of algebra.

REMARK 7.5.12 The infinitary operations of most interest are meets, joins, limits and colimits. Proposition 3.2.7(b) and Theorem 3.9.7 showed in particular how to add joins to a poset, retaining certain specified joins. If a poset A is able to carry an algebra for a join-adding monad, then this structure a is unique, and a\dashv hA; such monads may be recognised by the fact that mX\dashv hMX. They were investigated by Anders Kock [Koc95] and V. Zöbelein. For meet- or limit- adding monads, the adjunctions are reversed. Alan Day found such a monad over Sp (or Dcpo) whose algebras are continuous lattices and whose homomorphisms preserve Ù and Ú­ [GHK+80]. This was generalised (to smaller classes of meets) in [Tay90] and [ Sch93].

REMARK 7.5.13 The Transfinite Recursion Theorem 6.7.4 relates the algebras for the covariant powerset monad (complete join- semilattices) equipped with an endofunction, to the well founded coalgebras for the functor alone, which we discussed in Example 6.3.3 and Remark 6.7.14 . In fact the coalgebras for any functor which happens to be part of a monad carry partial ``successor'' and ``union'' operations (Exercise  7.45) [CP92, JM95,Tay96b].

REMARK 7.5.14 Eugenio Moggi has argued that certain monads should be regarded as notions of computation [Mog91]. To each type X we associate the type MX of computations (whose ultimate results would be) of type X. For example, with the lift monad (Definition  3.3.7), morphisms G® LiftX are partial (possibly non-terminating) programs. Additional structure, known as a strength, is needed for this, as for parametric recursion in Remark 6.1.6 and Exercise  6.23. Moggi gave a symbolic form (the `` let'' calculus) for this piece of category theory.

REMARK 7.5.15 Jon Beck himself studied monads to unify homological algebra [ BB69]. Applying the functor M repeatedly to an object X, the natural transformations Mn-i-1mMiX provide the boundary operations (S-morphisms) of a simplicial complex (Exercise 4.15). On the other hand the ``ordinals'' MnÆ just mentioned provide an abstract system of simplices (point, interval, triangle, tetrahedron, ...), so we may use maps MnÆ® X to investigate the homotopy of any object X.

Echoing what we said about the utility of adjoints at the end of Section 7.3, whenever you have a construction which yields an object of the same category as its data, it is well worth looking for natural transformations making it a monad. The opportunities for mathematical investigation from such a simple thing are quite striking: the algebras for the monad often turn out to form important categories in their own right, and the iterates of its functor provide detailed information about the abstract topology and recursion theory of the category.