Proposition 7.3.1.16. 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, where $\delta $ factors as a composition
\[ K \xrightarrow { \delta ^{0} } \operatorname{\mathcal{C}}^{0} \xrightarrow {G} \operatorname{\mathcal{C}} \]
for some $\infty $-category $\operatorname{\mathcal{C}}^{0}$. Then:
- $(1)$
If $G$ is fully faithful and $\alpha $ exhibits $F$ as a right Kan extension of $F_0$ along $\delta $, then it also exhibits $F \circ G$ as a right Kan extension of $F_0$ along $\delta ^{0}$.
- $(2)$
If $G$ is an equivalence of $\infty $-categories and $\alpha $ exhibits $F \circ G$ as a right Kan extension of $F_0$ along $\delta ^0$, then it exhibits $F$ as a right Kan extension of $F_0$ along $\delta $.
Proof.
Assume that $G$ is fully faithful. Then, for every pair of objects $X,Y \in \operatorname{\mathcal{C}}^{0}$, the induced map of left-pinched morphism spaces
\[ \operatorname{\mathcal{C}}^{0}_{X/} \times _{\operatorname{\mathcal{C}}} \{ Y\} = \operatorname{Hom}^{\mathrm{L}}_{\operatorname{\mathcal{C}}^{0}}( X,Y) \rightarrow \operatorname{Hom}^{\mathrm{L}}_{\operatorname{\mathcal{C}}}( G(X), G(Y) ) = \operatorname{\mathcal{C}}_{ G(X) / } \times _{\operatorname{\mathcal{C}}} \{ G(Y) \} \]
is a homotopy equivalence. Allowing $Y$ to vary and applying Corollary 5.1.7.16, we see that the natural map $\operatorname{\mathcal{C}}^{0}_{X/} \rightarrow \operatorname{\mathcal{C}}_{ G(X)/ } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}^0$ is an equivalence of left fibrations over $\operatorname{\mathcal{C}}^{0}$. It follows that the induced map
\[ \operatorname{\mathcal{C}}^{0}_{X/} \times _{ \operatorname{\mathcal{C}}^{0} } K \rightarrow \operatorname{\mathcal{C}}_{ G(X) / } \times _{ \operatorname{\mathcal{C}}} 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 that the natural transformation $\alpha $ satisfies condition $(\ast _ X)$ of Definition 7.3.1.2 if and only if it satisfies condition $(\ast _{ G(X) })$. Assertion $(1)$ now follows by allowing the object $X \in \operatorname{\mathcal{C}}^{0}$ to vary.
We now prove $(2)$. Assume that $G$ is an equivalence of $\infty $-categories and that $\alpha $ exhibits $F \circ G$ as a right Kan extension of $F_0$ along $\delta ^0$; we wish to show that $\alpha $ exhibits $F$ as a right Kan extension of $F_0$ along $\delta $. Let $H: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{0}$ be a homotopy inverse of $G$. Then $H$ is left adjoint to $G$, so we can choose natural transformations
\[ \eta : \operatorname{id}_{ \operatorname{\mathcal{C}}} \rightarrow G \circ H \quad \quad \epsilon : H \circ G \rightarrow \operatorname{id}_{\operatorname{\mathcal{C}}^{0}} \]
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
\[ F \circ G \circ H \circ G \circ \delta ^0 \xrightarrow {\epsilon } F \circ G \circ \delta ^0 \xrightarrow {\alpha } F_0. \]
Using Remark 7.3.1.12, we see that $\alpha '$ exhibits $F \circ G$ as a right Kan extension of $F_0$ along $H \circ G \circ \delta ^0 = H \circ \delta $. Applying assertion $(1)$ to the fully faithful functor $H: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{0}$, we deduce that $\alpha '$ also exhibits $\delta $ as a right Kan extension of $F_0$ along $F \circ G \circ H$. The compatibility of $\eta $ and $\epsilon $ guarantees that $\alpha $ is a composition of the natural transformations
\[ F \circ \delta \xrightarrow { \eta } F \circ G \circ H \circ \delta \xrightarrow { \alpha ' } F_0. \]
Applying Remark 7.3.1.13, we conclude that $\alpha $ exhibits $F$ as a right Kan extension of $F_0$ along $\delta $, as desired.
$\square$