Kerodon

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

Proposition 4.6.1.10. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $B$ be a simplicial set, let $A \subseteq B$ be a simplicial subset which contains every vertex of $B$, and let $f: A \rightarrow \operatorname{\mathcal{C}}$ be a diagram. Then the fiber product $\operatorname{Fun}(B,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A,\operatorname{\mathcal{C}}) } \{ f \} $ is a Kan complex.

Proof. Corollary 4.4.5.3 guarantees the restriction map $\theta : \operatorname{Fun}(B,\operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{C}})$ is an isofibration, so that the fiber $\operatorname{Fun}(B,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A,\operatorname{\mathcal{C}}) } \{ f \} $ is an $\infty $-category. To show that it is a Kan complex, it will suffice to show that every morphism $u$ in $\operatorname{Fun}(B,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A,\operatorname{\mathcal{C}}) } \{ f \} $ is an isomorphism (Proposition 4.4.2.1). By virtue of Corollary 4.4.3.19, this is equivalent to the assertion that the image of $u$ in the $\infty $-category $\operatorname{Fun}( B, \operatorname{\mathcal{C}})$ is an isomorphism. This follows from Theorem 4.4.4.4, since for every vertex $b \in B$, the evaluation functor

\[ \operatorname{ev}_ b: \operatorname{Fun}(B, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \{ b\} , \operatorname{\mathcal{C}}) \simeq \operatorname{\mathcal{C}} \]

factors through $\operatorname{Fun}(A, \operatorname{\mathcal{C}})$ and therefore carries $u$ to the identity morphism $\operatorname{id}_{ f(b)}$. $\square$