Equivalence of over categories induced by equivalence

Question

Suppose $F:C \to D$ is a equivalence of categories and that $X$ is an object of $C$.

Then there exists a equivalence of over categories $F/X:C/X \to D/F(X)$?

I see a related theorem stated in Prop. 3.1 https://ncatlab.org/nlab/show/over+category although I wish to relax the existence of pullbacks.

Answer 1

Yes, if $F$ is an equivalence, then $F/X$ is also an equivalence.

Let $C$ and $D$ be categories, $F\colon C\to D$ and $G\colon D\to C$ be functors, $u\colon I_C\to G\circ F$ and $\varepsilon\colon F\circ G\to I_D$ be natural transformations, such that $(F,G,u,\varepsilon)$ is an adjoint equivalence, $X\in\text{Obj}(C)$. Then define the functor $F/X\colon C/X\to D/F(X)$ in the following way: $(F/X)_{\text{Obj}}(X',f)=(F(X'),F(f))$, $(F/X)_{\text{Mor}}(g)=F(g)$. Also define the functor $\overline{G/X}\colon D/F(X)\to C/X$ in the following way: $(\overline{G/X})_{\text{Obj}}(Y,f)=(G(Y),u^{-1}(X)\circ G(f))$, $(\overline{G/X})_{\text{Mor}}(g)=G(g)$. Define also natural transformations $\overline{u}\colon I_{C/X}\to\overline{G/X}\circ F/X$ and $\overline{\varepsilon}\colon F/X\circ\overline{G/X}\to I_{D/F(X)}$ in the following way: $\overline{u}(X',f)=u(X')$, $\overline{\varepsilon}(Y,f)=\varepsilon(Y)$. Then $(F/X,\overline{G/X},\overline{u},\overline{\varepsilon})$ is an equivalence.