Kerodon

Proof. We will prove $(1)$; the proof of $(2)$ is similar. Fix an object $C \in \operatorname{\mathcal{C}}$. Since $\epsilon $ is a categorical equivalence and the projection map $\operatorname{\mathcal{C}}_{C/} \rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Proposition 4.3.6.1), it follows that the induced map $\epsilon _{C/}: K' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{C/} \rightarrow K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{C/}$ is also a categorical equivalence of simplicial sets (Corollary 5.6.7.6). In particular, $\epsilon _{C/}$ is left cofinal (Corollary 7.2.1.13). Applying Corollary 7.2.2.3, we see that the natural transformation $\alpha $ satisfies condition $(\ast _ C)$ of Definition 7.3.1.2 if and only if $\alpha '$ satisfies condition $(\ast _ C)$. The desired result now follows by allowing the object $C \in \operatorname{\mathcal{C}}$ to vary. $\square$

Proof. Using Corollary 3.1.8.2, we can choose a monomorphism $\iota : \Delta ^1 \rightarrow Q$, where $Q$ is a contractible Kan complex. Let us identify $\iota $ with an edge $e: q_0 \rightarrow q_1$ of $Q$. Since $\iota $ is a weak homotopy equivalence, there is a morphism of simplicial sets $f: Q \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})^{\simeq }$ satisfying $t(e) = \alpha $. Let us identify $f$ with a diagram $F: Q \times K \rightarrow \operatorname{\mathcal{C}}$. Let $\widetilde{H}$ denote the composite map $Q \times K \rightarrow K \xrightarrow {H} \operatorname{\mathcal{D}}$. Since the inclusion $\{ q_1 \} \times K \hookrightarrow Q \times K$ is a categorical equivalence, we can extend $\alpha $ to a natural transformation $\widetilde{\alpha }: G \circ F \rightarrow \widetilde{H}$. Unwinding the definitions, we see that the composite natural transformation $G \circ F_0 \xrightarrow { \alpha } G \circ F_1 \xrightarrow {\beta } H$ can be identified with the restriction of $\widetilde{\alpha }$ to $\{ q_0 \} \times K$. Applying Proposition 7.3.1.14 twice, conclude that $(a)$ and $(b)$ are both equivalent to the requirement that $\widetilde{\alpha }$ exhibits $G$ as a right Kan extension of $\widetilde{H}$ along $F$. $\square$

Proof. Suppose that $F$ is fully faithful. Then, for every pair of objects $X,Y \in \operatorname{\mathcal{C}}$, the functor $F$ induces a homotopy equivalence of left-pinched morphism spaces

Allowing $Y$ to vary and applying Corollary 5.1.7.16, we see that the natural map $\operatorname{\mathcal{C}}_{X/} \rightarrow \operatorname{\mathcal{D}}_{ F(X)/ } \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}$ is an equivalence of left fibrations over $\operatorname{\mathcal{C}}$. It follows that the induced map $\operatorname{\mathcal{C}}_{X/} \times _{ \operatorname{\mathcal{C}}} K \rightarrow \operatorname{\mathcal{D}}_{ F(X) / } \times _{ \operatorname{\mathcal{D}}} K$ is an equivalence of left fibrations over $K$. In particular it is a categorical equivalence of simplicial sets (Proposition 5.1.7.5) and therefore left cofinal (Corollary 7.2.1.13). Applying Corollary 7.2.2.3, we see if $\alpha $ satisfies condition $( \ast _{F(X) })$ of Definition 7.3.1.2, then it also satisfies condition $(\ast _ X)$. Assertion $(1)$ now follows by allowing the object $X$ to vary.

We now prove $(2)$. Assume that $F$ is an equivalence of $\infty $-categories and that $\alpha $ exhibits $G \circ F$ as a right Kan extension of $G_0$ along $\gamma $. Let $E: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a homotopy inverse of $F$. Then $E$ is left adjoint to $F$, so we can choose natural transformations

which are compatible up to homotopy in the sense of Definition 6.2.1.1. Note that $\eta $ and $\epsilon $ are isomorphisms (Proposition 6.1.4.1). Let $\alpha '$ denote a composition of the natural transformations

Using Corollary 7.3.1.15, we see that $\alpha '$ exhibits $G \circ F$ as a right Kan extension of $G_0$ along $E \circ F \circ \gamma = E \circ \delta $. Applying assertion $(1)$ to the fully faithful functor $E: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$, we deduce that $\alpha '$ also exhibits $\delta $ as a right Kan extension of $G_0$ along $G \circ F \circ E$. The compatibility of $\eta $ and $\epsilon $ guarantees that $\alpha $ is a composition of the natural transformations

Applying Remark 7.3.1.12, we conclude that $\alpha $ also exhibits $G$ as a right Kan extension of $G_0$ along $\delta $, as desired. $\square$

Proof. Let $\alpha : F \circ G \rightarrow F_0$ be a natural transformation which exhibits $F$ as a right Kan extension of $F_0$ along $G$. Applying Proposition (in the special case where $K = \operatorname{\mathcal{C}}^0$), we deduce that $\alpha $ also exhibits $F \circ G$ as a right Kan extension of $F_0$ along the identity functor $\operatorname{id}_{ \operatorname{\mathcal{C}}^{0} }: \operatorname{\mathcal{C}}^{0} \rightarrow \operatorname{\mathcal{C}}^{0}$. Invoking Example 7.3.1.8, we see that $\alpha $ is an isomorphism. This proves the first assertion; the second follows by a similar argument. $\square$

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.4.5). In particular, $\delta _{C/}$ is left cofinal (Proposition 7.2.1.10). 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.6. $\square$