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.

• Whether or not a result is deep is a subjective assessment. – Igor Rivin Jan 6 '14 at 19:01
• I would say that the Yoneda lemma is one of the most important and deep theorems of category theory. Also see here :mathoverflow.net/questions/83437/… – Baby Dragon Jan 6 '14 at 19:08
• @IgorRivin Then answer subjectively? – preferred_anon Jan 6 '14 at 19:17
• The various forms of the adjoint functor theorem are one example: ncatlab.org/nlab/show/adjoint+functor+theorem Beck's monadicity theorem is another: ncatlab.org/nlab/show/monadicity+theorem – user314 Jan 6 '14 at 19:40
• In Récoltes et Semailles Grothendieck described two styles in mathematics. One: «put the cutting edge of the chisel against the shell and strike hard. If needed, begin again at many different points until the shell cracks»; and another: «The unknown thing to be known appeared to me as some stretch of earth or hard marl, resisting penetration... the sea advances insensibly in silence, nothing seems to happen, nothing moves, the water is so far off you hardly hear it… yet it ﬁnally surrounds the resistant substance» (translation by C. McLarty, AFAIK). – Grigory M Jan 6 '14 at 19:51

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

• The general adjoint functor theorem
• Freyd's representability criterion