Kerodon

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

Corollary 7.3.5.9. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a coreflective full subcategory and let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be an isofibration of $\infty $-categories. Suppose we are given a lifting problem

7.27
\begin{equation} \begin{gathered}\label{equation:relative-Kan-extension-coreflective} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}^{0} \ar [r]^-{F_0} \ar [d] & \operatorname{\mathcal{D}}\ar [d]^{U} \\ \operatorname{\mathcal{C}}\ar [r]^-{G} \ar@ {-->}[ur]^{F} & \operatorname{\mathcal{E}}. } \end{gathered} \end{equation}

The following conditions are equivalent:

$(1)$

The lifting problem (7.27) admits a solution $F$ which is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$.

$(2)$

For every morphism $u: C' \rightarrow C$ of $\operatorname{\mathcal{C}}$ which exhibits $C'$ as a $\operatorname{\mathcal{C}}^{0}$-coreflection of $\operatorname{\mathcal{C}}$, the image $G(u)$ can be lifted to a $U$-cocartesian morphism $F_0( C' ) \rightarrow D$ of $\operatorname{\mathcal{D}}$.

Proof. Fix an object $C \in \operatorname{\mathcal{C}}$, and choose a morphism $u: C' \rightarrow C$ which exhibits $C'$ as a $\operatorname{\mathcal{C}}^{0}$-coreflection of $\operatorname{\mathcal{C}}$. By virtue of Proposition 7.3.5.5, it will suffice to show that the lifting problem

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}^{0}_{/C} \ar [rr] \ar [d] & & \operatorname{\mathcal{D}}\ar [d]^{U} \\ ( \operatorname{\mathcal{C}}^0_{/C})^{\triangleright } \ar [r] \ar@ {-->}[urr]^{ F_ C } & \operatorname{\mathcal{C}}\ar [r]^-{G} & \operatorname{\mathcal{E}}} \]

admits a solution which is a $U$-colimit diagram if and only if $G(u)$ can be lifted to a $U$-cocartesian morphism $F_0(C') \rightarrow D$. This follows from Corollary 7.2.2.14, since $u$ is final when viewed as an object of the $\infty $-category $\operatorname{\mathcal{C}}^{0}_{/C}$. $\square$