# Kerodon

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

Proposition 7.3.1.15. 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.6.15, 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$ 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.6.5) and therefore left cofinal (Corollary 7.2.1.12). 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.11, we see that $\alpha '$ exhibits $H \circ G \circ \delta ^0 = H \circ \delta$ as a right Kan extension of $F_0$ along $F \circ G$. 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.12, we conclude that $\alpha$ exhibits $F$ as a right Kan extension of $F_0$ along $\delta$, as desired. $\square$