nLab
monadic adjunction

Context

Higher algebra

2-Category theory

Monadic adjunctions

Idea

One can turn monads into adjunctions and adjunctions into monads, but one doesn't always return where one started. Every monad comes from an adjunction, but only a monadic adjunction comes from a monad via a monadic functor. (To be fair, there are two ways to turn a monad into an adjunction, given by the Kleisli category and the Eilenberg–Moore category; we are talking about the latter here.)

Definition

We give the definitions in Cat and leave it to future readers and writers to generalise. See for instance (Riehl-Verity 13).

Let (C,D,,r,ι,ϵ)(C,D,\ell,r,\iota,\epsilon) be an adjunction in CatCat; that is, :CD\ell: C \to D and r:DCr: D \to C are adjoint functors with r\ell \dashv r, where ι\iota and ϵ\epsilon are the unit and counit. Let TT be rr \circ \ell; TT has the structure of a monad on CC, so consider the Eilenberg–Moore category C TC^T of modules (algebras) for TT. Then rϵ:Trrr \circ \epsilon: T \circ r \to r endows r:DCr: D \to C with a TT-algebra structure, hence defines a functor k:DC Tk: D \to C^T.

The adjunction r\ell \dashv r is monadic if this functor kk is an equivalence of categories.

Beck’s monadicity theorem

Beck’s Monadicity Theorem gives a necessary and sufficient condition for an adjunction to be monadic. Namely, the adjunction (C,D,,r,ι,ϵ)(C,D,\ell,r,\iota,\epsilon) is monadic iff:

  • rr reflects isomorphisms; and

  • DD has coequalizers of rr-split coequalizer pairs, and rr preserves those coequalizers.

See monadicity theorem for more details and variants.

Algebraic categories

The typical categories studied in algebra, such as Grp, Ring, etc, all come equipped with monadic adjunctions from Set. Specifically, the right adjoint is the forgetful functor from algebras to sets, and the left adjoint maps each set to the free algebra on that set. Their composite (a monad on SetSet) may be thought of as mapping a set AA to the set of words with alphabet taken from AA and the connections between letters taken from the appropriate algebraic operations, with two words identified if they can be proved equal by the appropriate algebraic axioms.

Abstractly, one may define an algebraic category to be a category equipped with a monadic adjunction from SetSet. However, there are now more examples than the ones from algebra; the best known of these is the category of compact Hausdorff spaces, which corresponds to the ultrafilter monad. (This result relies on the ultrafilter principle, regardless of whether one interprets ‘space’ here as referring to topological spaces or locales.)

References

Discussion

John Baez: We read above: “One can turn monads into adjunctions and adjunctions into monads, but one doesn't always return where one started.” This suggests that there is something like an adjunction between monads and adjunctions! What’s the precise story?

I imagine something like this: there’s a functor (or 2-functor)

[adjunctions][monads] [adjunctions] \to [monads]

and this has left and right adjoints (or 2-adjoints)

Kleisli:[monads][adjunctions] Kleisli : [monads] \to [adjunctions]
EilenbergMoore:[monads][adjunctions] Eilenberg Moore: [monads] \to [adjunctions]

As evidence, note that the Kleisli category gives the initial object among adjunctions that give rise to a specified monad, while the Eilenberg-Moore category gives the terminal one. See the Wikipedia article.

Zoran Škoda: the best-well-known article on monads, R. Street, Formal theory of monads, JPAA 2, 149–168, 1972, has the basic fact that Eilenberg-Moore construction as a correspondence from monads to categories, extends to a 2-functor which is right 2-adjoint to the trivial monad 2-functor and the left adjoint is the underlying 2-functor (forgetting actions). Now you are trying to view EM construction as an adjoint to adjunctions to monads correspondence. First of all, I could imagine several different 2-categories of adjunctions, hence several different questions in the game (and monads make 2-category in more than one way, but with lessvariety than adjunctions). But there are better people to ask about this…

Mike Shulman: This adjunction does exist (although you sometimes have to be careful about size issues) and is called the semantics-structure adjunction. The EM-category functor Mnd(C)RAdj/CMnd(C) \to RAdj/C is called the “semantics” functor (here RAdj/CRAdj/C is the subcategory of Cat/CCat/C consisting of the right adjoints) and its left adjoint (the monad underlying an adjunction) is called the “structure” functor. In fact, the structure functor is defined on a larger subcategory of Cat/CCat/C, namely those functors g:ACg:A\to C such that Ran ggRan_g g exists (if gg has a left adjoint ff then Ran ggRan_g g always exists and is equal to gfg f). In this case Ran ggRan_g g is the image of gg under “structure”, also called its codensity monad. Presumably by duality, “structure” also has a left adjoint “cosemantics” given by the Kleisli construction. The semantics-structure adjunction can be found in Chapter II of Dubuc’s “Kan Extensions in Enriched Category Theory” and also in section 2 of “The Formal Theory of Monads”.

Emily Riehl: I’m interrupting Mike to comment on duality. The Kleisli construction is really a functor Mnd(C) opC/LAdjMnd(C)^{op} \to C/LAdj. A monad map (C,S)(C,T)(C,S) \to (C,T) consists of a 2-cell TST \Rightarrow S satisfying conditions. This defines a map of Kleisli categories C TC SC_T \to C_S that commutes with the left adjoints but not with the right adjoints (that apply the monads to objects to get back to CC).

I didn’t check all the details but it does seem to be the case that “structure” and “cosemantics” are mutual left adjoints, with adjunct maps defined in exactly the way you’d expect.

Mike Shulman: If anyone can give a nice conceptual explanation of the terms “semantics” and “structure” in this context, Daniel Schaeppi is currently writing a paper which could benefit from such an explanation. I’ve never found anyone who really explains the words (nor is it entirely clear who pioneered their use in this context—Dubuc perhaps?) It makes sense to me that the E-M category can be called the “semantics” of a monad, but my intuition for “structure” is fuzzier, except that of course any monad can be regarded as a notion of structure with which one can equip objects. But why is that “the” structure associated to an adjunction?

Mike Shulman: In case anyone is following this, Daniel has come up with what seems to be the right answer to this question; I’m hoping that eventually he will write about it here.

References

Discussion for quasi-categories is around definition 6.1.15 and definition 7.1.6 in

Revised on March 24, 2014 12:24:45 by Anodyne Howard (92.192.97.65)