$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 7.6.3.16. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$. The following conditions are equivalent:
- $(1)$
There exists a functor $f^{\ast }: \operatorname{\mathcal{C}}_{/Y} \rightarrow \operatorname{\mathcal{C}}_{/X}$ given by pullback along $f$ (in the sense of Definition 7.6.3.15).
- $(2)$
For every morphism $u: Y' \rightarrow Y$, there exists a pullback diagram
\[ \xymatrix { X' \ar [r] \ar [d] & Y' \ar [d]^{u} \\ X \ar [r]^{f} & Y } \]
in the $\infty $-category $\operatorname{\mathcal{C}}$.
Moreover, if these conditions are satisfied, then the pullback functor $f^{\ast }$ carries each object $Y' \in \operatorname{\mathcal{C}}_{/Y}$ to the fiber product $X \times _{Y} Y'$.
Proof.
Let $e_{0}: \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}_{/X}$ and $e_{1}: \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}_{/Y}$ denote the restriction map. Then $e_0$ is a trivial Kan fibration (Corollary 4.3.6.13), and postcomposition with $f$ is defined as the composition of $e_1$ with a section of $e_0$ (Example 4.3.6.14). We can therefore reformulate $(1)$ as follows:
- $(1')$
The restriction functor $e_1: \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}_{/Y}$ admits a right adjoint.
Let us identify the morphism $f$ with an object $\widetilde{X} \in \operatorname{\mathcal{C}}_{/Y}$. Using Proposition 7.6.3.14, we can reformulate condition $(2)$ as follows:
- $(2')$
For every object $\widetilde{Y}' \in \operatorname{\mathcal{C}}_{/Y}$, there exists a product of $\widetilde{X}$ with $\widetilde{Y}'$ in $\operatorname{\mathcal{C}}_{/Y}$.
The equivalence of $(1')$ and $(2')$ now follows from Proposition 7.6.1.12, applied to the slice $\infty $-category $\operatorname{\mathcal{C}}_{/Y}$.
$\square$