Item 1 (013U) — The Clowder Project

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`

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.

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.

Noticed something off, or have any comments? Feel free to reach out!

You can also use the contact form below: