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:\id_S® M and m:M²® 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 Set^S ), and start with a free algebraic theory in the sense of Section 6.1, presented as a functor T. Let \LeftAdjoint₀X be the free T-algebra on X, with inclusion h_X:X® \Monad₀X, where \Monad₀ = U·\LeftAdjoint₀. Then (\Monad₀,h,m) is a monad, for a certain natural transformation m.

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

A monad is needed to code laws. For a T-algebra \ev_A:TA® A, the map e_A:\Monad₀A® A constructed in Example  7.4.6 evaluates terms of arbitrary depth, whereas \ev_A 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, e_A must satisfy certain conditions if it is given by some \ev_A.

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 h_X and the composite of f:X® MY with g:Y® MZ is f;Mg;m_Z ( cf Exercise 3.38 for preorders). There is an adjunction, omitted diagram environment with co-unit e_X = \id_MX, 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, \LeftAdjoint_EM:X® (MX,m_X), 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 e_A: 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 lim_i\typeA_i or from \colim_iM\typeA_i shown dotted. Similarly the Eilenberg-Moore equations h;a = id and Ma;a = m;a hold because both sides are mediators to lim_i\typeA_i or from \colim_iM\typeA_i or \colim_iM²\typeA_i. []

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 h_MA 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 = \id_B 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 m_A 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 m_A 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 e_A 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 e_FX 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:\Monad₀A® 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 \Monad₀A® 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 \Monad₀A \twoheadrightarrow MA® A is an L₀-algebra satisfying the laws.

(d)

(Bob Paré) Set^op @ 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].

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

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 h_A; such monads may be recognised by the fact that m_X\dashv h_MX. 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 M^n-i-1m_MⁱX provide the boundary operations (S-morphisms) of a simplicial complex (Exercise 4.15). On the other hand the ``ordinals'' MⁿÆ just mentioned provide an abstract system of simplices (point, interval, triangle, tetrahedron, ...), so we may use maps MⁿÆ® 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.