Kerodon

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

Proposition 7.4.5.11. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. Then a morphism of simplicial sets $F: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ is a limit diagram if and only if, for every object $X \in \operatorname{\mathcal{C}}$, the composition

\[ K^{\triangleleft } \xrightarrow { F } \operatorname{\mathcal{C}}\xrightarrow {h^{X} } \operatorname{\mathcal{S}} \]

is a limit diagram in the $\infty $-category of spaces; here $h^{X}$ denotes the functor corepresented by $X$ (Notation 5.6.6.15).

Proof. Applying Proposition 7.1.5.12, we see that $F$ is a limit diagram if and only if, for every object $X \in \operatorname{\mathcal{C}}$, the restriction map

\[ \theta _{X}: \operatorname{Hom}_{ \operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}}) }( \underline{X}, F) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( K, \operatorname{\mathcal{C}}) }( \underline{X}|_{K}, F|_{K} ) \]

is a homotopy equivalence of Kan complexes. Let $\operatorname{\mathcal{E}}$ denote the oriented fiber product $\{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$ and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be given by projection onto the second factor. Note that $U$ is a left fibration (Proposition 4.6.4.10) and that $\theta _{X}$ can be identified with the restriction map

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( K^{\triangleleft }, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( K, \operatorname{\mathcal{E}}). \]

The identity morphism $\operatorname{id}_{X}$ can be viewed as an initial object of $\operatorname{\mathcal{E}}$ satisfying $U( \operatorname{id}_{X} ) = X$ (Proposition 4.6.6.23), so the corepresentable functor $h^{X}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ is a covariant transport representation for $U$ (Proposition 5.6.6.22). Applying Corollary 7.4.5.8, we see that $\theta _{X}$ is a homotopy equivalence if and only if $h^{X} \circ F$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$. $\square$