---
tag: WA60RW9E04
kind: statement
role: theorem
name: Fully faithful essentially surjective functor is an equivalence
msc: [18A22]
uses: [K7A04ZBD92, GRG8WEBSH5, 6ERBSBVF14, 28NQ0KRHD3, KYCPCC57FT]
about: [K7A04ZBD92]
sources:
  - url: https://en.wikipedia.org/wiki/Equivalence_of_categories
---

## Statement

Assume the axiom of choice, applied to the classes of objects involved.
Let $F \colon \mathcal{C} \to \mathcal{D}$ be a [[functor|28NQ0KRHD3]].
Then $F$ is an [[equivalence of categories|K7A04ZBD92]] if and only if $F$ is [[fully faithful|GRG8WEBSH5]] and [[essentially surjective|6ERBSBVF14]].

## Remarks

Suppose first that $F$ has a quasi-inverse $G$ with [[natural isomorphisms|KYCPCC57FT]] $\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.

## Explanations

### L1 human

To check that two categories are "the same up to isomorphism", one does not need to build a functor going back.
It is enough that the functor matches the arrows exactly and reaches every object up to isomorphism.
The return functor can then be built by picking, for each target object, one source object that lands near it.

### L2 human

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.