Kerodon

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

Proposition 7.6.2.15 (Covariant Transport as a Kan Extension). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of $\infty$-categories having essentially small fibers, 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.55
$$\begin{gathered}\label{equation:covariant-transport-as-Kan-extension} \xymatrix { \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}$$

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.6.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.11. $\square$