Kerodon

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

Variant 7.6.2.23. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$. By virtue of Example 5.3.7.5, the evaluation functor $\operatorname{ev}_1: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of $\infty $-categories, and therefore determines a covariant transport functor

\[ f_{!}: \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ X\} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ Y\} . \]

We say that a functor

\[ f^{\ast }: \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ Y\} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ X\} \]

is given by pullback along $f$ if it is right adjoint to the functor $f_{!}$. By virtue of Proposition 5.3.7.6, this is equivalent to the existence of a homotopy commutative diagram

\[ \xymatrix { \operatorname{\mathcal{C}}_{/Y} \ar@ {-->}[r] \ar [d]^{ \delta _{/Y} }_{\sim } & \operatorname{\mathcal{C}}_{ / X} \ar [d]^{ \delta _{/X} }_{\sim } \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y\} \ar [r]^{ f^{\ast } } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ X\} , } \]

where the vertical maps are the pinch inclusion equivalences of Corollary 4.6.4.18 and the upper horizontal map is given by pullback along $f$ (in the sense of Definition 7.6.2.22).