Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Corollary 4.4.2.12. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a conservative functor of $\infty $-categories and let $q: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram in $\operatorname{\mathcal{C}}$. Then the induced functors

\[ F_{q/}: \operatorname{\mathcal{C}}_{q/} \rightarrow \operatorname{\mathcal{D}}_{(F \circ q)/} \quad \quad F_{/q}: \operatorname{\mathcal{C}}_{/q} \rightarrow \operatorname{\mathcal{D}}_{/(F \circ q)} \]

are also conservative.

Proof. We will show that the functor $F_{/q}$ is conservative; the conservativity of $F_{q/}$ follows by a similar argument. Let $\pi : \operatorname{\mathcal{C}}_{/q} \rightarrow \operatorname{\mathcal{C}}$ and $\pi ': \operatorname{\mathcal{D}}_{/(F \circ q)} \rightarrow \operatorname{\mathcal{D}}$ denote the projection maps. Then $\pi $ and $\pi '$ are right fibrations of $\infty $-categories (Proposition 4.3.6.1), and therefore conservative (Proposition 4.4.2.11). Since $F$ is conservative, from Remark 4.4.2.10 that the functor $F \circ \pi = \pi ' \circ F_{/q}$ is also conservative. Applying Remark 4.4.2.10 again, we conclude that $F_{/q}$ is conservative. $\square$