I am a training Algebraic Geometer, and am currently trying to prepare a course on category theory. I would be really thankful if people could tell me about "real-math" applications of theorems about monads which they came across during their career.

• By "application", do you mean "example"? It seems to me often useful to notice something is a monad or an adjunction, even if I then don't quote any theorems about general monads in attacking the problem at hand Commented Dec 26, 2011 at 13:13
• I would be interested if there is a real-world theorem where knowing that something is a monad facilitates finding the morally correct proof. Commented Dec 26, 2011 at 13:28

The abstract algebra of monads is similar to the algebra of monoids, so that constructions on monoids often suggest similar constructions on monads. This applies in particular to bar constructions.

A pretty striking application in its time was the use of bar constructions on monads to construct deloopings. Around 1963, Stasheff identified the extra structures on H-spaces $X$ that need to hold in order to construct a single delooping $X \simeq \Omega Y$ compatible with the H-space structures. This was at a time before there were such things as operads and their associated monads. But by the time May's The Geometry of Iterated Loop Spaces had appeared, there was appreciation of the algebra of operads and monads to economically package the panoply of algebraic operations that obtain on iterated loop spaces. In particular, the two-sided bar constructions for monads and their algebras, similar to the Milgram bar construction for monoids, were used to give conceptually simple constructions for iterated deloopings, extending the constructions of Stasheff to much more general contexts.

• Indeed, monads and monoids are both types of categorical monoids. Because, as we know "A monad is monoid in the category of endofunctors. What's the problem?" Commented Dec 4, 2015 at 1:41

Forgetting or ignoring category theory (I hardly knew any in 1971), as Todd says I used monads concretely and constructively to manufacture spaces Y such that $\Omega ^n Y$ is equivalent to $X$, where $X$ is a space with an action by a suitable operad. Operads encode lots of operations, and their associated monads coalesce all those operations into a single operation, the product of the monad. (The portmanteau word operad combines operation and monad, inspired by this connection and by Lewis Carroll). This concrete coalescence of information is the essence of many, but by no means all, applications of monads. In iterated loop space theory, the combinatorial monads associated to operads mesh with the more abstract monads $\Omega^n\Sigma^n$ associated to the adjoint pair of functors $(\Sigma^n,\Omega^n)$.

The discussion of monads on wikipedia is very good. You can see all the terms from categorical monads popping up in that article, and facts about monads from category theory often lead to new programs in Haskell and other programming languages. Another nice overview is this pdf. An article written for computer scientists is here.

One of the other ways they show up in 'real math' is via the following: there is always a forgetful functor from the category of $T$-algebras in $\scr{C}$ to $\scr{C}$ with a left adjoint, the free $T$-algebra functor. This forgetful functor must also preserve and reflect certain coequalizer diagrams. In a precise sense (see Monadicity theorem) we can identify whether or not a functor is a forgetful functor from a category of algebras over some monad by these properties. This gives a useful criterion for seeing whether or not something is in the image of such a functor and what are the maps between such objects. This (or its dual formulation) gives descent type theorems, which is probably what algebraic geometers care most about. These theorems will generally tell you something like when is the category of sheaves of some type equivalent to a category of descent data of a very particular form.
• Just to amplify on Justin's answer slightly: the natural "geometric function theories" in algebraic geometry, i.e. categories of quasicoherent or coherent sheaves, categories of D-modules, categories of $\ell$-adic sheaves, etc. come with direct and inverse image functors of various kinds that have adjoints on one side or another. So one naturally has (co)monadic structure from that---I personally view this as a fundamental organizing principle. There are then many ways to play descent-type games in this setting; a very powerful recent tool is Lurie's Barr-Beck theorem for $\infty$-cats. Commented Dec 28, 2011 at 14:46