What are some examples of hard theorems in category theory?

I'm currently learning some category theory, but so far I've used it only as a handy way to talk about various related concepts in algebra and topology with some nice, easy-to-prove lemmas like "left adjoint functors commute with limits" which can be applied to a wide range of problems. Even with regard to Yoneda's lemma, the hardest part is to understand the problem, the proof itself is rather straightforward.

Therefore, I was wondering which theorems of category theory involve really difficult proofs. Mitchell's embedding theorem seems to be a pretty deep result of homological algebra, but I guess there are some theorems the proofs of which are even greater achievements in category theory.

(Unsolved problems are also welcome.)

Edit: I think that I've previously misused the notion of the "depth" of a theorem. I simply wanted to say that all proofs in category theory that I have seen this far seem only to "scratch the surface" of categories (meaning that they are roughly of the form: Given an object which has this and that property, we verify that it also has another property by drawing the corresponding diagram plugging in the given universal properties at the right places in the diagram, and finally obtaining the arrow we sought). Especially, all these proofs were fairly "local", in the sense that they only involved a fixed number of arrows and morphisms of the category. I simply wanted to see some theorems requiring more ingenuous ideas than plugin in the right definition at the right time.

Solution 1:

Almost the same question has been asked at mathoverflow, MO/83437. Here is a summary:

• The general adjoint functor theorem
• Freyd's representability criterion
• Beck's monadacity theorem
• Recognition theorems for locally presentable categories
• Brown's representability theorem
• The small object argument
• Gabriel-Ulmer duality
• Tannaka duality
• Giraud's theorem
• Embedding theorems such as Freyd-Mitchell and Gabriel-Popescu

These are big and useful theorems, but of course there are also lots of other examples of nontrivial category theory (which can be found in journals such as TAC). Here is a cute example:

• Linearization reflects isomorphisms (MO/17532, proof)