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 – Yemon Choi Dec 26 2011 at 13:13
Moreover: it is standard practice on MO that "big list" type questions should be made "community wiki" by checking the appropriate box (you can do this by editing your own question). – Yemon Choi Dec 26 2011 at 13:14
I disagree with this being standard practice. CW discourages people from posting well-thought and rich-in-substance answers rather than just links and minor chunks of fact (and, even worse, names). – darij grinberg Dec 26 2011 at 13:28
I would be interested if there is a real-world theorem where knowing that something is a monad facilitates finding the morally correct proof. – Lukas Dec 26 2011 at 13:28
CW is standard practice for big list questions. Whether it should be can be discussed (on meta). – Michael Greinecker Dec 26 2011 at 13:51

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.

-

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)$.

-

I would say first that monads are useful in that they offer a level of abstraction that can be used to describe lots of different algebraic phenomena. That is, categories of groups, abelian groups, rings, commutative rings,... can each be described equivalently as categories of algebras over some monad acting on sets (see Lawvere Theory for more examples). There are monads that don't arise in this way, but typically most examples are pretty close to this. So in one sense the theorems that are true in all of these situations are most naturally proven in the language of monads and their categories of algebras.

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.

I would recommend looking at Borceux's 'Handbook of Categorical Algebra' Vol. 2 Ch. 4 for more details. I'm sorry that I don't have a more geometric reference at hand.

-
 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. – Thomas Nevins Dec 28 2011 at 14:46