# Kerodon

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

Lemma 7.1.3.15. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a conservative functor of $\infty$-categories and let $u: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram. Suppose that $u$ can be extended to a limit diagram $\overline{u}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ for which the composition $(F \circ \overline{u}): K^{\triangleleft } \rightarrow \operatorname{\mathcal{D}}$ is also a limit diagram. Let $\overline{u}': K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ be an arbitrary extension of $u$. Then $\overline{u}'$ is a limit diagram in $\operatorname{\mathcal{C}}$ if and only if $F \circ \overline{u}'$ is a limit diagram in $\operatorname{\mathcal{D}}$.

Proof. Let us identify $\overline{u}$ and $\overline{u}'$ with objects $C$ and $C'$ of the slice $\infty$-category $\operatorname{\mathcal{C}}_{/u}$. Our assumption that $\overline{u}$ is a limit diagram guarantees that $C$ is a final object of $\operatorname{\mathcal{C}}_{/u}$, so there exists a morphism $f: C' \rightarrow C$ in $\operatorname{\mathcal{C}}_{/u}$. Note that $\overline{u}'$ is a limit diagram if and only if the object $C'$ is also final: that is, if and only if the morphism $f$ is an isomorphism.

Let $g: D' \rightarrow D$ be the image of $f$ under the functor $F_{/u}: \operatorname{\mathcal{C}}_{/u} \rightarrow \operatorname{\mathcal{D}}_{ / (F \circ u)}$. Our assumption that $F \circ \overline{u}$ is a limit diagram guarantees that $D$ is a final object of $\operatorname{\mathcal{D}}_{ / (F \circ u)}$. Consequently, $g$ is an isomorphism if and only if the object $D'$ is also final: that is, if and only if $(F \circ \overline{u}')$ is a limit diagram in $\operatorname{\mathcal{D}}$.

To complete the proof, it will suffice to show that $f$ is an isomorphism in $\operatorname{\mathcal{C}}_{/u}$ if and only if $g = F_{/u}(f)$ is an isomorphism in $\operatorname{\mathcal{D}}_{ / (F \circ q)}$. In fact, the functor $F_{/q}$ is conservative: this follows from our assumption that $F$ is conservative, by virtue of Corollary 4.4.2.12. $\square$