Proposition 7.4.1.16. Suppose we are given a pullback diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d]^{U} & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \ar [d] \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleleft }, } \]
where $U$ and $\overline{U}$ are essentially small left fibrations, and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ be a covariant transport representation for $\overline{U}$. The following conditions are equivalent:
- $(1)$
The morphism $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ is a limit diagram.
- $(2)$
The restriction map
\[ Q: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \]
is a homotopy equivalence of Kan complexes.
Proof of Proposition 7.4.1.16.
Using Proposition 7.4.1.9, we can choose a natural transformation $\overline{\alpha }: \underline{ \Delta ^0 }_{\overline{\operatorname{\mathcal{E}}}} \rightarrow \overline{\mathscr {F}}|_{ \overline{\operatorname{\mathcal{E}}} }$ which exhibits $\overline{\mathscr {F}}$ as a covariant transport representation for $\overline{U}$. Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$, so that we have a commutative diagram of Kan complexes
\[ \xymatrix { \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^{Q} & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \ar [d] \\ \operatorname{Hom}_{\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{S}})}( \underline{\Delta ^0}_{ \operatorname{\mathcal{C}}^{\triangleleft } }, \overline{\mathscr {F}} ) \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})}( \underline{ \Delta ^0}_{ \operatorname{\mathcal{C}}}, \mathscr {F} ) } \]
where the vertical maps are given by Construction 7.4.1.13, and are therefore homotopy equivalences (Proposition 7.4.1.14). It follows that $(2)$ is equivalent the following:
- $(2')$
The restriction map $Q': \operatorname{Hom}_{\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{S}})}( \underline{\Delta ^0}_{ \operatorname{\mathcal{C}}^{\triangleleft } }, \overline{\mathscr {F}} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})}( \underline{ \Delta ^0}_{ \operatorname{\mathcal{C}}}, \mathscr {F} )$ is a homotopy equivalence.
Choose a Kan complex $Y$ and a natural transformation $\overline{\beta }: \underline{Y}_{ \operatorname{\mathcal{C}}^{\triangleleft } } \rightarrow \overline{\mathscr {F}}$ which exhibits $Y$ as a limit of the diagram $\overline{\mathscr {F}}$ (so that $\beta $ induces a homotopy equivalence $Y \rightarrow \overline{\mathscr {F}}(v)$, where $v$ denotes the cone point of $\operatorname{\mathcal{C}}^{\triangleleft } \simeq \{ v\} \star \operatorname{\mathcal{C}}$). Then $\overline{\beta }$ restricts to a natural transformation $\beta : \underline{Y}_{\operatorname{\mathcal{C}}} \rightarrow \mathscr {F}$. We then have a commutative diagram of Kan complexes
\[ \xymatrix { & \operatorname{Hom}_{\operatorname{\mathcal{S}}}( \Delta ^0, Y) \ar [dl]^{\overline{\theta }} \ar [dr]^{\theta } & \\ \operatorname{Hom}_{\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{S}}) }( \underline{ \Delta ^0}_{\operatorname{\mathcal{C}}^{\triangleleft }}, \overline{\mathscr {F}} ) \ar [rr]^{Q'} & & \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})}( \underline{ \Delta ^0 }_{\operatorname{\mathcal{C}}}, \mathscr {F} ), } \]
where $\theta $ and $\overline{\theta }$ are induced by composition with $\beta $ and $\overline{\beta }$, respectively. It follows from Proposition 7.4.1.1 that $\overline{\theta }$ is a homotopy equivalence. Moreover, $\overline{\mathscr {F}}$ is a limit diagram if and only if $\beta $ exhibits $Y$ as a limit of $\mathscr {F}$: that is, if and only if $\theta $ is also a homotopy equivalence. Using the commutativity of the diagram, we see that this is equivalent to condition $(2')$.
$\square$