# Kerodon

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

Proposition 7.3.1.17. Suppose we are given a diagram

$\xymatrix@R =50pt@C=50pt{ & \operatorname{\mathcal{C}}\ar [dr]^{F} \ar@ {=>}[]+<0pt,-25pt>;+<0pt,-50pt>^-{\alpha } & \\ K \ar [ur]^{\delta } \ar [rr]_{F_0} & & \operatorname{\mathcal{D}}}$

as in Definition 7.3.1.2. Assume that $\delta$ exhibits $\operatorname{\mathcal{C}}$ as a localization of $K$ (with respect to some collection of edges of $K$) and that $\alpha$ is an isomorphism in the $\infty$-category $\operatorname{Fun}(K, \operatorname{\mathcal{D}})$. Then $\alpha$ exhibits $F$ as a right Kan extension of $F_0$ along $\delta$.

Proof. Fix an object $C \in \operatorname{\mathcal{C}}$. Since $\alpha$ is an isomorphism, it will suffice to show that the tautological map $\underline{F(C)} \rightarrow (F \circ \delta )|_{ K_{C/} }$ exhibits $F(C)$ as a limit of the diagram $(F \circ \delta )|_{ K_{C/} }$. Since the projection map $\operatorname{\mathcal{C}}_{C/} \rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Proposition 4.3.6.1), the map $\delta _{C/}: K_{C/} \rightarrow \operatorname{\mathcal{C}}_{C/}$ exhibits the $\infty$-category $\operatorname{\mathcal{C}}_{C/}$ as a localization of the simplicial set $K_{C/}$ (Corollary 6.3.5.5). In particular, $\delta _{C/}$ is left cofinal (Proposition 7.2.1.9). We can therefore replace $K$ by $\operatorname{\mathcal{C}}$ (Corollary 7.2.2.7), in which case the desired result follows from the criterion of Corollary 7.2.2.5. $\square$