Kerodon

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

Corollary 4.5.2.22. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories and let

\[ \delta : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}= \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(\{ 0\} , \operatorname{\mathcal{D}})} \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{D}}) \]

be map induced by the diagonal embedding $c: \operatorname{\mathcal{D}}\hookrightarrow \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{D}})$. Then $\delta $ is fully faithful, and its essential image is the homotopy fiber product $\operatorname{\mathcal{C}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ of Construction 4.5.2.1.

Proof. Let us identify the objects of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ with triples $(C,D,u)$, where $C$ is an object of $\operatorname{\mathcal{C}}$, $D$ is an object of $\operatorname{\mathcal{D}}$, and $u: F(C) \rightarrow D$ is a morphism in $\operatorname{\mathcal{D}}$. By definition, $\operatorname{\mathcal{C}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is the full subcategory of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ spanned by those triples $(C,D,u)$ where $u$ is an isomorphism in $\operatorname{\mathcal{D}}$. The functor $\delta $ is given on objects by the formula $\delta (C) = ( C, F(C), \operatorname{id}_{ F(C) } )$, and therefore factors through $\operatorname{\mathcal{C}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$. To complete the proof, it will suffice to show that the functor $\delta : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is an equivalence of $\infty $-categories. Equivalently, we wish to show that the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^{\operatorname{id}} \ar [d]^{F} & \operatorname{\mathcal{C}}\ar [d]^{F} \\ \operatorname{\mathcal{D}}\ar [r]^{\operatorname{id}} & \operatorname{\mathcal{D}}} \]

is a categorical pullback square, which is a special case of Proposition 4.5.2.21. $\square$