Theorem: Let be a functor. is an equivalence of categories if and only if is full, faithful, and essentially surjective on objects.
Proof: Assume that is an equivalence. Then, we have a functor , and two natural isomorphisms and .
We first show that is faithful. Let be an arrow in . We have a component . The naturality condition says that . Of course and . So simplifying a bit, we have . If there were another arrow with , it would follow that . But then, we obtain by combining this with the respective naturality conditions:
Since is a natural isomorphism, is an isomorphism, thus the outer-most inequality implies .
Now we show that is full. Consider an arrow in . Take . This is well-defined since is a natural isomorphism and thus is an isomorphism. By naturality we have . Then . Equating this with the previous expression for :
and since and are both isomorphisms we can conclude that . This really means that . But, is an equivalence – we showed that equivalences are faithful in the preceding paragraph. Thus, we can conclude that .
Finally, we show that is essentially surjective on objects. Let . We claim that is the desired element so that . In fact, is an isomorphism between and .
Now assume that is full, faithful, and essentially surjective on objects. We will define the functor . For a , define as any particular object in whose image under is isomorphic to , say via a particular isomorphism (there is at least one since is essentially surjective on objects). That is, we have . We now need to define on arrows. For an arrow in , note that gives a bijection , since it is full and faithful. Then let – the inner term is a map and we take the inverse image under the bijection given by .
We now claim that we have a natural isomorphism , with components as chosen above. Note that since every is an isomorphism, will be a natural isomorphism as long as it is a natural transformation – so we need only show the latter, which amounts to checking the naturality condition, which is straightforward: For a map in , we have:
and is a natural isomorphism.
Finally, we define . For , we need to define . Note that is a map . Since is full and faithful, it gives an bijection . So, let . It is straightforward to check that since is an isomorphism, its preimage under the bijection given by will be as well. So each is an isomorphism and we need only check naturality. So, consider a in . Considering an arrow in , we know the following is true:
(since the inverse of is also a natural isomorphism ). But, both sides can be rewritten to yield:
and since is faithful, we can conclude that
which is precisely the naturality condition for . Thus, is a natural isomorphism, completing the proof.