The main theorems of category theory and their applications This question first arose as I wrote an answer for the question: Is there a nice application of category theory to functional/complex/harmonic analysis?; it can also be regarded as a (hopefully) more focused version of the question Most striking applications of category theory?.

It seems that category theory began as an organizational tool in topology and algebraic geometry, but by now it has grown into an area of research in its own right with applications all over the place in mathematics.  I realized as I was thinking about my answer to the question above that I did not know the statements of the main results in category theory, or even if there are "main results".  In a comment, Martin Brandenburg suggested several examples:


*

*The general adjoint functor theorem

*Freyd's representability criterion

*Beck's monadacity theorem

*Recognition theorems for locally presentable categories

*Brown's representability theorem


He also indicated that these results have numerous unsung applications to other areas of mathematics.  This question is essentially an invitation for Martin and anyone else add to this list and explain some of the applications of the items on it.  I would not have asked this question on mathoverflow if I believed that such a list already existed; if I am wrong then the question should probably be closed.  

Here is what I have in mind for an answer to this question.  It should include the statement of a theorem in pure category theory (ideally using language which is friendly to outsiders) and at least one application to another area of mathematics.  The community wiki rule "one theorem per answer" makes sense here, particularly so that others can conveniently add applications to your list.
When I say "theorem in pure category theory", I don't insist that the result be incredibly nontrivial, just that it is a result which is stated and proved in the language of category theory.  For example, the statement that $\pi_1$ is a functor belongs to topology, not category theory; on the other hand the Yoneda lemma counts even though it is a "lemma" instead of a "theorem".
When I say "application to another area of mathematics" I am ideally looking for statements which can be formulated without using the language of categories and functors.  I want to be clear that I am interested in applications of specific results in category theory, not just results for which categorical thinking is useful (such results are everywhere).
 A: The method of forcing in mathematical logic.
If you want to prove the consistency of axiom systems, you can just explicitly present a model of it. To prove results about set theory itself, like the independence of the continuum hypothesis or the axiom of choice, you need to find something like a "modified set theory". According to general philosophy, it is enough to present a category, similar to the category of sets. Category theory gives an abundance of such categories: elementary toposes. They are a special class of cartesian closed categories. They come equipped with a natural internal intuitionistic logic, describing the properties of morphisms. Now the problem of finding the required model transforms into the problem of finding a topos, satisfying our set of axioms, interpreted using the internal logic. It can be done categorically. An example of the construction, proving the independence of the continuum hypothesis, can be found in P.T. Johnstone's "Topos theory".
Technically one can construct a model in some category of sheaves, but topos-theoretic approach is much more simple and flexible (besides, sheaf is also a categorical notion and any topos is roughly a category of sheaves).
A: Freyd-Mitchell and Gabriel-Popescu theorems, and also the characterization of co-Grothendieck cats.
A: The small object argument. Essentially this states that if you have a collection of maps $f_\alpha$ in a presentable category (actually, you only need the domains of the $f_\alpha$ to be compact, along with cocompleteness of the category), then any map in the category can be functorially factored as the composite of two maps: 


*

*A map which is a transfinite pushout of coproducts of the $f_\alpha$. 

*A map which has the right lifting property with respect to the $f_\alpha$. 


This was first used by Grothendieck to show (in his Tohoku paper) that a Grothendieck abelian category always has enough injectives (which, as far as I know, is not directly obvious for abelian sheaves on a site, for instance). Later it became the main tool in constructing model structures on categories, because it lets you show that the factorizations needed in the definition exist. 
A: Monadicity theorems like Beck's give sufficient conditions on a functor $U \colon B \to A$ with a left adjoint F to be equivalent (in the slice category Cat/A) to the forgetful functor out of the category $A^{U F}$ of algebras for the monad $U F$.
Aside from their obvious usefulness in universal algebra, one important application is in descent theory: suppose you have a category C and a C-indexed category E (i.e. a pseudofunctor $E \colon C^{\mathrm{op}} \to \mathrm{Cat}$) such that


*

*Each $f^* = Ef$ has a right adjoint $f_!$, and

*The Beck--Chevalley condition holds: E takes any pullback square in C to an isomorphism in Cat whose mate is again an isomorphism.
Then (this is due to Bénabou and Roubaud) for a morphism f in C, the category of descent data for f is equivalent to the category of algebras for the monad $f_!f^*$.  In particular, f is of effective descent if $f_!$ is monadic.  See the nLab page on monadic descent for details.
I believe the original application had C the category of commutative rings and $E \colon R \mapsto R\mathrm{-Mod}$.
A: I think of Gabriel-Ulmer duality as one of the early key results in categorical model theory. 
Many structures in mathematics are what are called "essentially algebraic". This includes all algebraic structures (which model theories given by a functional signature and universally quantified equations): groups, rings, Lie algebras, etc. It also includes algebra-like structures which don't quite fit in this mold, for example categories, where some of the operations may only be partially defined (but the domains of the operations are given by equations involving other operations). There are various nice ways of expressing the syntax of an essentially algebraic theory: one is via limit sketches, another is just to use finitely complete categories, in much the same way that (following Lawvere) classical algebraic theories can be expressed as certain categories with products. 
If we think of a small finitely complete category as a "theory" $T$, then a model of $T$ in this way of thinking is a finitely continuous functor $T \to Set$. The category of models would then be the category $Cont(T, Set)$ of such functors and transformations between them. 
What is amazing and very nice is that the theory $T$ can be recovered from the category of models $M$, by considering functors 
$$M \to Set$$ 
which preserve all limits (have left adjoints) and all filtered colimits. This is essentially Gabriel-Ulmer duality, giving a perfect dual correspondence between theories or syntax of finitary essentially algebraic type (small finitely complete categories) and semantic categories of models of such (which can be described in pure category terms as locally finitely presentable categories). 
This perfect duality between syntax and semantics is part of a long story in categorical model theory, culminating the theory of accessible and locally presentable categories. Spiritually, it is reminiscent of many other dualities such as the Tannaka-Krein duality mentioned by Finn Lawler earlier. 
Edit: This is in response to Martin's comment. I'll give a sample application and some nontrivial consequences (which, to be sure, can be arrived at via other avenues). The moral for me is that Gabriel-Ulmer duality is a relatively simple statement that can become, after a while, a useful part of one's daily thinking. 
My example is the category $\text{Cocomm}$ of cocommutative coalgebras over (let's say) a field $k$. What can we say about it? Well, it's easy to see it is cocomplete: one constructs colimits (coproducts, coequalizers, etc.) as one would on the underlying vector spaces, lifting the vector-space colimit to a coalgebra structure in a canonical way. Much more significantly, there is a fundamental theorem about (cocommutative) coalgebras: each is the union (in particular a filtered colimit) of its finite-dimensional subcoalgebras. Meanwhile, a finite-dimensional coalgebra $C$ has the property that $\hom(C, -): \text{Cocomm} \to Set$ preserves filtered colimits. 
People who have taken Gabriel-Ulmer duality into their hearts will immediately recognize the import of these results: $Cocomm$ is locally finitely presentable. This implies something at first unexpected: not only are coalgebras coalgebraic over vector spaces: they are models of an essentially algebraic theory! Indeed, Gabriel-Ulmer duality implies that $Cocomm$ is equivalent to the category of finitely continuous (left exact) functors 
$$\text{Cocomm}_{\text{fin.dim.}}^{op} \to Set$$ 
or if you prefer, to the category of finitely continuous functors $\text{CommAlg}_{fd} \to Set$ (so in this case, the relevant "theory" is the category of finite-dimensional commutative algebras). 
This unexpected recognition has a host of useful consequences. For example, the category $Cocomm$ is complete. Those who think this is obvious are invited to construct infinite products and equalizers explicitly with their bare hands -- it is not trivial. Also, the category is cartesian closed. Indeed $C$ and $D$ are viewed as cocommutative coalgebras, then the exponential $D^C$ is identified with the left exact functor that takes a finite-dimensional algebra $A$ to $\hom(A^\ast \otimes_k C, D)$, a very pretty and explicit formula. 
Similar considerations apply to (not necessarily cocommutative) coalgebras, and to differential graded coalgebras (cocommutative or not). 
A: There was some discussion here about special cases of Yoneda's lemma, including the usual examples of Cayley's theorem for groups and Dedekind's embedding theorem for posets.
It also seems that a good chunk of Tannaka duality can be seen as an application of the (enriched) Yoneda lemma -- see the nLab page for discussion.
A: This is that a small category may be regarded as a simplicial set with unique inner horn fillers. 
