Proposition 8.5.7.1.2 (013T): Properties of Equivalences of Categories

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

Let $F\colon \mathcal{C}\to \mathcal{D}$ be a functor.

Characterisations. If $\mathcal{C}$ and $\mathcal{D}$ are small ^[1], then the following conditions are equivalent:^[2]
1. The functor $F$ is an equivalence of categories.
2. The functor $F$ is fully faithful and essentially surjective.
3. The induced functor
  \[ \left.F\right\vert _{\mathsf{Sk}\webleft (\mathcal{C}\webright )}\colon \mathsf{Sk}\webleft (\mathcal{C}\webright )\to \mathsf{Sk}\webleft (\mathcal{D}\webright ) \]
  
  is an isomorphism of categories.
4. For each $X\in \text{Obj}\webleft (\mathsf{Cats}\webright )$, the precomposition functor
  \[ F^{*}\colon \mathsf{Fun}\webleft (\mathcal{D},\mathcal{X}\webright )\to \mathsf{Fun}\webleft (\mathcal{C},\mathcal{X}\webright ) \]
  
  is an equivalence of categories.
5. For each $X\in \text{Obj}\webleft (\mathsf{Cats}\webright )$, the postcomposition functor
  \[ F_{*}\colon \mathsf{Fun}\webleft (\mathcal{X},\mathcal{C}\webright )\to \mathsf{Fun}\webleft (\mathcal{X},\mathcal{D}\webright ) \]
  
  is an equivalence of categories.
Two-Out-of-Three. Let

be a diagram in $\mathsf{Cats}$. If two out of the three functors among $F$, $G$, and $G\circ F$ are equivalences of categories, then so is the third.
Stability Under Composition. Let

be a diagram in $\mathsf{Cats}$. If $\webleft (F,G\webright )$ and $\webleft (F',G'\webright )$ are equivalences of categories, then so is their composite $\webleft (F'\circ F,G'\circ G\webright )$.
Equivalences vs.Adjoint Equivalences. Every equivalence of categories can be promoted to an adjoint equivalence.^[3]
Interaction With Groupoids. If $\mathcal{C}$ and $\mathcal{D}$ are groupoids, then the following conditions are equivalent:
1. The functor $F$ is an equivalence of groupoids.
2. The following conditions are satisfied:
  1. The functor $F$ induces a bijection
    \[ \pi _{0}\webleft (F\webright )\colon \pi _{0}\webleft (\mathcal{C}\webright )\to \pi _{0}\webleft (\mathcal{D}\webright ) \]
    
    of sets.
  2. For each $A\in \text{Obj}\webleft (\mathcal{C}\webright )$, the induced map
    \[ F_{x,x}\colon \mathrm{Aut}_{\mathcal{C}}\webleft (A\webright )\to \mathrm{Aut}_{\mathcal{D}}\webleft (F_{A}\webright ) \]
    
    is an isomorphism of groups.

Item 1: Characterisations

We claim that Item (a), Item (b), Item (c), Item (d), and Item (e) are indeed equivalent:

Item (a)$\implies $Item (b): Clear.
Item (b)$\implies $Item (a): Since $F$ is essentially surjective and $\mathcal{C}$ and $\mathcal{D}$ are small, we can choose, using the axiom of choice, for each $B\in \text{Obj}\webleft (\mathcal{D}\webright )$, an object $j_{B}$ of $\mathcal{C}$ and an isomorphism $i_{B}\colon B\to F_{j_{B}}$ of $\mathcal{D}$.
Since $F$ is fully faithful, we can extend the assignment $B\mapsto j_{B}$ to a unique functor $j\colon \mathcal{D}\to \mathcal{C}$ such that the isomorphisms $i_{B}\colon B\to F_{j_{B}}$ assemble into a natural isomorphism $\eta \colon \text{id}_{\mathcal{D}}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}F\circ j$, with a similar natural isomorphism $\epsilon \colon \text{id}_{\mathcal{C}}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}j\circ F$. Hence $F$ is an equivalence.
Item (a)$\implies $Item (c): This follows from Item 4 of Proposition 8.1.5.1.3.
Item (c)$\implies $Item (a): Omitted.
Item (a), Item (d), and Item (e) Are Equivalent: This follows from .

This finishes the proof of Item 1.

Item 2: Two-Out-of-Three

Omitted.

Item 3: Stability Under Composition

Clear.

Item 4: Equivalences vs.Adjoint Equivalences

See Proposition 4.4.5 of [Riehl, Category Theory in Context].

Item 5: Interaction With Groupoids

See Proposition 4.4 of [nLab, Groupoid].

Footnotes

[1] Otherwise there will be size issues. One can also work with large categories and universes, or require $F$ to be constructively essentially surjective; see [MSE 1465107].

[2] In ZFC, the equivalence between Item (a) and Item (b) is equivalent to the axiom of choice; see [MO 119454].

In Univalent Foundations, this is true without requiring neither the axiom of choice nor the law of excluded middle.

[3] More precisely, we can promote an equivalence of categories $\webleft (F,G,\eta ,\epsilon \webright )$ to adjoint equivalences $\webleft (F,G,\eta ',\epsilon \webright )$ and $\webleft (F,G,\eta ,\epsilon '\webright )$.