Fully faithful essentially surjective functor is an equivalence

Remarks

Suppose first that $F$ has a quasi-inverse $G$ with natural isomorphisms $\eta \colon 1 \Rightarrow GF$ and $\varepsilon \colon FG \Rightarrow 1$. Then $\varepsilon_D \colon F(G(D)) \cong D$ gives essential surjectivity, and naturality $\eta_B \circ f = G(F(f)) \circ \eta_A$ shows that $F$ is faithful, and likewise $G$. For $h \colon F(A) \to F(B)$, the morphism $f = \eta_B^{-1} \circ G(h) \circ \eta_A$ satisfies $G(F(f)) = G(h)$, so $F(f) = h$ because $G$ is faithful; this direction needs no choice. Conversely, choose for each object $D$ of $\mathcal{D}$ an object $G(D)$ of $\mathcal{C}$ and an isomorphism $\varepsilon_D \colon F(G(D)) \to D$. For $g \colon D \to D'$, full faithfulness gives a unique $G(g)$ with $F(G(g)) = \varepsilon_{D'}^{-1} \circ g \circ \varepsilon_D$, which makes $G$ a functor and $\varepsilon$ natural. The unit $\eta_A$ is the unique morphism with $F(\eta_A) = \varepsilon_{F(A)}^{-1}$, and it is an isomorphism because fully faithful functors reflect isomorphisms. Example at work: let $K$ be a field, and include the full subcategory of spaces $K^n$ into all finite-dimensional vector spaces over $K$. This inclusion is fully faithful and essentially surjective, so it is an equivalence. Without choice, the converse can fail, since a quasi-inverse requires picking one preimage up to isomorphism for every object. In fact the converse for all functors between small categories is equivalent to the axiom of choice.

Going deeper

For a student

This criterion is how most equivalences are proved in practice, for instance that every category is equivalent to its skeleton. The quasi-inverse constructed in the proof can be chosen so that $\eta$ and $\varepsilon$ satisfy the triangle identities, so every equivalence is part of an adjoint equivalence. Properties defined by universal properties, such as having products or being abelian, are invariant under equivalence, so the theorem lets one transfer them along any fully faithful essentially surjective functor.