Kerodon

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

Proposition 7.6.2.17 (Covariant Transport as a Kan Extension). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small left fibration of $\infty $-categories, let $\underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}}$ denote the constant functor $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}$ taking the value $\Delta ^0$, and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be any functor. Suppose we are given a natural transformation $\beta : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F} \circ U$. The following conditions are equivalent:

$(1)$

The natural transformation $\beta $ exhibits $\mathscr {F}$ as a left Kan extension of $\underline{ \Delta ^0}_{\operatorname{\mathcal{E}}}$ along $U$ (in the sense of Variant 7.3.1.5).

$(2)$

The commutative diagram

7.56
\begin{equation} \begin{gathered}\label{equation:covariant-transport-as-Kan-extension} \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r]^-{\beta } & \{ \Delta ^0 \} \operatorname{\vec{\times }}_{ \operatorname{\mathcal{S}}} \operatorname{\mathcal{S}}\ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ \mathscr {F} } & \operatorname{\mathcal{S}}} \end{gathered} \end{equation}

is a categorical pullback square.

Proof. Fix an object $C \in \operatorname{\mathcal{C}}$ and let $\operatorname{\mathcal{E}}_{C}$ denote the fiber $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, so that the restriction of $\beta $ to $\operatorname{\mathcal{E}}_{C}$ can be identified with a morphism of Kan complexes $e_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{S}}}( \Delta ^0, \mathscr {F}(C) )$. By virtue of Proposition 7.3.4.1 and Corollary 5.1.7.15, it will suffice to show that the following conditions are equivalent:

$(1_ C)$

The morphism $e_ C$ exhibits $\mathscr {F}(C)$ as a tensor product of $\Delta ^0$ by $\mathscr {E}_{C}$ (as an object of the $\infty $-category $\operatorname{\mathcal{S}}$).

$(2_ C)$

The morphism $e_ C$ is a homotopy equivalence.

This is a special case of Example 7.6.2.12. $\square$