Kerodon

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

7.5.4 Homotopy Limit Diagrams

Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Kan}$ be a diagram in the category of Kan complexes, and let

\[ \operatorname{N}_{\bullet }^{\operatorname{hc}}(\mathscr {F}): \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan}) = \operatorname{\mathcal{S}} \]

be the induced functor of $\infty $-categories. Then the homotopy limit $\varprojlim (\mathscr {F} )$ is a Kan complex, which can be regarded as a limit of the diagram $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\mathscr {F} )$ in the $\infty $-category of spaces $\operatorname{\mathcal{S}}$ (Proposition 7.5.1.5). For many applications, this assertion is insufficiently precise: we would like to have not only a Kan complex $X$ which is known abstractly to be a limit of the diagram $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\mathscr {F})$, but also a diagram $\operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } ) \rightarrow \operatorname{\mathcal{S}}$ which exhibits $X$ as a limit of $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\mathscr {F})$.

Definition 7.5.4.1. Let $\operatorname{\mathcal{C}}$ be a category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be a functor having restriction $\mathscr {F} = \overline{ \mathscr {F} }|_{\operatorname{\mathcal{C}}}$. We will say that $\overline{ \mathscr {F} }$ is a homotopy limit diagram if the composite map

\[ \overline{ \mathscr {F} }( {\bf 0} ) \rightarrow \varprojlim ( \mathscr {F} ) \hookrightarrow \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F} ) \]

is a homotopy equivalence of Kan complexes; here ${\bf 0}$ denotes the initial object of the cone $\operatorname{\mathcal{C}}^{\triangleleft } \simeq \{ {\bf 0} \} \star \operatorname{\mathcal{C}}$, and the morphism on the right is the comparison map of Remark 7.5.2.10).

Example 7.5.4.2 (Limits of Isofibrant Diagrams). Let $\operatorname{\mathcal{C}}$ be a small category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be a limit diagram in the category of simplicial sets. Suppose that the diagram $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$ is isofibrant (Definition 4.5.6.3) and that, for each object $C \in \operatorname{\mathcal{C}}$, the simplicial set $\mathscr {F}(C)$ is a Kan complex. Then $\overline{\mathscr {F}}$ is a homotopy limit diagram of Kan complexes: this follows by combining Corollary 4.5.6.18 with Proposition 7.5.3.12.

Warning 7.5.4.3. For every diagram of Kan complexes $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Kan}$, the homotopy limit $ \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ of Construction 7.5.1.1 is well-defined. However, one cannot always extend $\mathscr {F}$ to a homotopy limit diagram $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ (see Warning 3.4.1.8). This is possible only if the tautological map $\varprojlim (\mathscr {F}) \hookrightarrow \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ has a left homotopy inverse. However, we can always choose a levelwise homotopy equivalence $\alpha : \mathscr {F} \hookrightarrow \mathscr {G}$, where $\mathscr {G}$ is an isofibrant diagram of Kan complexes (Variant 7.5.3.6). We can then extend $\mathscr {G}$ can be extended to a limit diagram $\overline{ \mathscr {G} }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$, which is also a homotopy limit diagram (Example 7.5.4.2). Moreover, if take $\mathscr {G} = \mathscr {F}^{+}$ to be the isofibrant replacement of Construction 7.5.3.3, then $\overline{\mathscr {G}}$ carries the initial object of $\operatorname{\mathcal{C}}^{\triangleleft }$ to the homotopy limit $ \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F} )$ (Proposition 7.5.3.7).

Proposition 7.5.4.4 (Homotopy Invariance). Let $\operatorname{\mathcal{C}}$ be a category and let $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$ be a natural transformation between diagrams $\overline{\mathscr {F}}, \overline{\mathscr {G}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$. Assume that, for every object $C \in \operatorname{\mathcal{C}}$, the induced map $\alpha _{C}: \overline{\mathscr {F}}(C) \rightarrow \overline{\mathscr {G}}(C)$ is a homotopy equivalence of Kan complexes. Then any two of the following conditions imply the third:

$(1)$

The functor $\overline{\mathscr {F}}$ is a homotopy limit diagram.

$(2)$

The functor $\overline{\mathscr {G}}$ is a homotopy limit diagram.

$(3)$

The natural transformation $\alpha $ induces a homotopy equivalence $\overline{\mathscr {F}}( {\bf 0} ) \rightarrow \overline{\mathscr {G}}( {\bf 0} )$, where ${\bf 0}$ denotes the cone point of $\operatorname{\mathcal{C}}^{\triangleleft }$.

Proof. Setting $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$ and $\mathscr {G} = \overline{\mathscr {G}}|_{\operatorname{\mathcal{C}}}$, we observe that $\alpha $ determines a commutative diagram of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ \overline{\mathscr {F}}( {\bf 0} ) \ar [r] \ar [d] & \overline{\mathscr {G}}( {\bf 0} ) \ar [d] \\ \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F}) \ar [r] & \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {G}), } \]

where the bottom horizontal map is a homotopy equivalence (Remark 7.5.1.3). The desired result now follows from the two-out-of-three property (Remark 3.1.6.7). $\square$

Proposition 7.5.4.5. Let $\operatorname{\mathcal{C}}$ be a small category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be a diagram of Kan complexes. Then $\overline{\mathscr {F}}$ is a homotopy limit diagram (in the sense of Definition 7.5.4.1) if and only if the induced functor of $\infty $-categories

\[ \operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}}): \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } ) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan}) = \operatorname{\mathcal{S}} \]

is a limit diagram (in the sense of Definition 7.1.2.4).

Proof. Let $\operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft })$ be the weighted nerve of the functor $\overline{\mathscr {F}}$ (Definition 5.3.3.1) and let $U: \operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft }) \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } )$ be the projection map. Then $U$ is a left fibration, and $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}} )$ is a covariant transport representation for $U$ (Example 5.7.5.6). Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$. Applying Corollary 7.4.5.10, we deduce that $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}} )$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$ if and only if the restriction map

\[ \rho : \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }), \operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft }) ) \rightarrow \simeq \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}), \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) ) \]

is a homotopy equivalence of Kan complexes. We then have a commutative diagram $\rho $ fits into a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \varprojlim ( \overline{ \mathscr {F} } ) \ar [r]^-{\rho '} \ar [d]^{\overline{\iota }} & \varprojlim (\mathscr {F}) \ar [d]^{\iota } \\ \underset {\longleftarrow }{\mathrm{holim}}( \overline{ \mathscr {F} } ) \ar [r]^-{\rho } & \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F}), } \]

where $\iota $ and $\overline{\iota }$ are the comparison maps of Remark 7.5.2.10. Since the category $\operatorname{\mathcal{C}}^{\triangleleft }$ has an initial object, the morphism $\overline{\iota }$ is a homotopy equivalence (Proposition 7.5.2.11). It follows that $\rho $ is a homotopy equivalence if and only if the composition $\rho \circ \overline{\iota } = \iota \circ \rho '$ is a homotopy equivalence. We conclude by observing that the composition $\iota \circ \rho '$ can be identified with the map $\overline{\mathscr {F}}( {\bf 0} ) \rightarrow \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ appearing in Definition 7.5.4.1. $\square$

Corollary 7.5.4.6. Let $\operatorname{\mathcal{C}}$ be a small category, let $\operatorname{\mathcal{D}}$ be a locally Kan simplicial category, and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{D}}$ be a functor. The following conditions are equivalent:

$(1)$

The functor

\[ \operatorname{N}_{\bullet }^{\operatorname{hc}}(\overline{\mathscr {F}}): \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})^{\triangleleft } \simeq \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{\mathcal{D}}) \]

is a limit diagram in the $\infty $-category $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{\mathcal{D}})$.

$(2)$

For every object $D \in \operatorname{\mathcal{D}}$, the functor

\[ \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}\quad \quad C \mapsto \operatorname{Hom}_{\operatorname{\mathcal{D}}}( D, \mathscr {F}(C) )_{\bullet } \]

is a homotopy limit diagram of Kan complexes.

Proof. By virtue of Proposition 7.4.5.13, condition $(1)$ is satisfied if and only if, for every object $D \in \operatorname{\mathcal{D}}$, the composition $(h^{D} \circ \operatorname{N}_{\bullet }^{\operatorname{hc}}(\mathscr {F})): \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$, where $h^{D}: \operatorname{N}_{\bullet }^{\operatorname{hc}}(\operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{S}}$ denotes a functor corepresented by $D$. Using Proposition 5.7.6.17, we can take $h^{D}$ to be the homotopy coherent nerve of the simplicial functor $\operatorname{Hom}_{\operatorname{\mathcal{D}}}(D, \bullet ): \operatorname{\mathcal{D}}\rightarrow \operatorname{Kan}$. In this case, $h^{D} \circ \operatorname{N}_{\bullet }^{\operatorname{hc}}(X)$ is the homotopy coherent nerve of the functor $C \mapsto \operatorname{Hom}_{\operatorname{\mathcal{D}}}(D, \mathscr {F}(C) )_{\bullet }$. The equivalence $(1) \Leftrightarrow (2)$ now follows from the criterion of Proposition 7.5.4.5. $\square$

Corollary 7.5.4.7. Let $\operatorname{\mathcal{C}}$ be a small category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Kan}$ be an isofibrant diagram of Kan complexes. Then $\mathscr {F}$ has a limit in the category $\operatorname{Kan}$, which is preserved by the inclusion functor $\operatorname{N}_{\bullet }( \operatorname{Kan}) \hookrightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan}) = \operatorname{\mathcal{S}}$.

For some applications, it is useful to extend Definition 7.5.4.1 to diagrams of simplicial sets which do not take values in the full subcategory $\operatorname{Kan}\subset \operatorname{Set_{\Delta }}$ of Kan complexes.

Definition 7.5.4.8 (Homotopy Limit Diagrams of Simplicial Sets). Let $\operatorname{\mathcal{C}}$ be a small category. We say that a functor $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ is a homotopy limit diagram if there exists a levelwise weak homotopy equivalence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$, where $\overline{\mathscr {G}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ is a homotopy limit diagram of Kan complexes (in the sense of Definition 7.5.4.1).

Remark 7.5.4.9. Let $\operatorname{\mathcal{C}}$ be a small category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be a functor. The following conditions are equivalent:

$(1)$

The functor $\overline{\mathscr {F}}$ is a homotopy limit diagram in the sense of Definition 7.5.4.1 (that is, it induces a homotopy equivalence $\overline{\mathscr {F}}( {\bf 0} ) \rightarrow \underset {\longleftarrow }{\mathrm{holim}}( \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}} )$, where ${\bf 0}$ denotes the cone point of $\operatorname{\mathcal{C}}^{\triangleleft }$).

$(2)$

The functor $\overline{\mathscr {F}}$ is a homotopy limit diagram in the sense of Definition 7.5.4.8: that is, there exists a homotopy limit diagram of Kan complexes $\overline{\mathscr {G}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a levelwise weak homotopy equivalence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$.

The implication $(1) \Rightarrow (2)$ is immediate, and the reverse implication follows from Proposition 7.5.4.4.

Proposition 7.5.4.10. Let $\operatorname{\mathcal{C}}$ be a small category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be a functor. The following conditions are equivalent:

$(1)$

The functor $\overline{\mathscr {F}}$ is a homotopy limit diagram. That is, there exists a homotopy limit diagram $\overline{\mathscr {F}}': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a levelwise weak homotopy equivalence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {F}}'$.

$(2)$

Let $\overline{\mathscr {F}}': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be any functor. If there exists a levelwise weak homotopy equivalence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {F}}'$, then $\overline{\mathscr {F}}'$ is a homotopy limit diagram.

Proof. Using Proposition 3.1.7.1, we can choose a functor $\overline{ \mathscr {G} }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a natural transformation $\beta : \overline{ \mathscr {F}} \rightarrow \overline{\mathscr {G} }$ which carries each object $C \in \operatorname{\mathcal{C}}^{\triangleleft }$ to an anodyne morphism of simplicial sets $\beta _{C}: \overline{ \mathscr {F} }(C) \rightarrow \overline{ \mathscr {G} }(C)$. We will show that $(1)$ and $(2)$ are equivalent to the following:

$(3)$

The functor $\overline{ \mathscr {G} }$ is a homotopy limit diagram.

The implications $(2) \Rightarrow (3) \Rightarrow (1)$ are immediate. To prove the reverse implications, suppose we are given another functor $\overline{\mathscr {F} }': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a levelwise weak homotopy equivalence $\alpha : \overline{ \mathscr {F} } \rightarrow \overline{ \mathscr {F} }'$. We will show that $\overline{ \mathscr {F} }'$ is a homotopy limit diagram if and only if $\overline{ \mathscr {G} }$ is a homotopy limit diagram.

Applying Proposition 3.1.7.1 again, we can choose a functor $\overline{ \mathscr {G} }': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \overline{ \mathscr {F} } \ar [r]^-{\alpha } \ar [d]^{\beta } & \overline{ \mathscr {F} }' \ar [d]^{\beta '} \\ \overline{ \mathscr {G} } \ar [r]^-{\alpha '} & \overline{ \mathscr {G} }' } \]

with the property that, for every object $C \in \operatorname{\mathcal{C}}^{\triangleleft }$, the induced map

\[ \overline{\mathscr {F} }'(C) \coprod _{ \overline{\mathscr {F} }(C)} \overline{ \mathscr {G} }(C) \rightarrow \overline{ \mathscr {G} }'(C) \]

is anodyne (and, in particular, a weak homotopy equivalence). Applying Proposition 3.4.2.11, we see that the diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \overline{ \mathscr {F} }(C) \ar [r]^-{ \alpha _ C } \ar [d]^{ \beta _{C} } & \overline{ \mathscr {F} }'(C) \ar [d]^{ \beta '_{C} } \\ \overline{ \mathscr {G} }(C) \ar [r]^-{ \alpha '_{C} } & \overline{ \mathscr {G} }'(C) } \]

is a homotopy pushout square. Since $\alpha _ C$ and $\beta _ C$ are weak homotopy equivalences, it follows that $\alpha '_ C$ and $\beta '_{C}$ are also weak homotopy equivalences (Proposition 3.4.2.10). Applying Proposition 7.5.4.4, we see that $\overline{ \mathscr {F} }'$ and $\overline{ \mathscr {G} }$ are homotopy limit diagrams if and only if $\overline{ \mathscr {G} }'$ is a homotopy limit diagram. $\square$

Corollary 7.5.4.11 (Homotopy Invariance). Let $\operatorname{\mathcal{C}}$ be a category, let $\overline{\mathscr {F}}, \overline{ \mathscr {G} }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be functors, and let $\alpha : \overline{ \mathscr {F} } \rightarrow \overline{ \mathscr {G} }$ be a natural transformation. Suppose that, for every object $C \in \operatorname{\mathcal{C}}$, the induced map $\alpha _{C}: \overline{ \mathscr {F} }(C) \rightarrow \overline{ \mathscr {G} }(C)$ is a weak homotopy equivalence. Then any two of the following conditions imply the third:

$(1)$

The functor $\overline{ \mathscr {F} }$ is a homotopy limit diagram.

$(2)$

The functor $\overline{ \mathscr {G} }$ is a homotopy limit diagram.

$(3)$

The natural transformation $\alpha $ induces a weak homotopy equivalence $\overline{ \mathscr {F} }( {\bf 0} ) \rightarrow \overline{ \mathscr {G} }( {\bf 0} )$, where ${\bf 0}$ denotes the cone point of $\operatorname{\mathcal{C}}^{\triangleleft }$.

Proof. Using Proposition 3.1.7.1, we can choose functors $\overline{ \mathscr {F}}', \overline{ \mathscr {G}}': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \overline{\mathscr {F}} \ar [r]^-{\alpha } \ar [d] & \overline{ \mathscr {G}} \ar [d] \\ \overline{ \mathscr {F} }' \ar [r]^-{\alpha '} & \overline{ \mathscr {G} }', } \]

where the vertical maps are levelwise weak homotopy equivalences. Using Proposition 7.5.4.10, we can replace $\alpha $ by the natural transformation $\alpha ': \overline{ \mathscr {F} }' \rightarrow \overline{ \mathscr {G} }'$, in which case the desired result follows from Proposition 7.5.4.4. $\square$

Corollary 7.5.4.12. Let $\operatorname{\mathcal{C}}$ be a category and let $\overline{ \mathscr {F} }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be a functor. Let $\overline{ \mathscr {F} }^{\operatorname{op}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ be the functor given on objects by $\overline{ \mathscr {F} }^{\operatorname{op}}(C) = \overline{\mathscr {F}}(C)^{\operatorname{op}}$. Then $\overline{\mathscr {F}}$ is a homotopy limit diagram if and only if $\overline{\mathscr {F}}^{\operatorname{op}}$ is a homotopy limit diagram.

Proof. For each object $C \in \operatorname{\mathcal{C}}^{\triangleleft }$, let $| \overline{\mathscr {F}}(C) |$ denote the geometric realization of the simplicial set $\overline{\mathscr {F}}(C)$ (Definition 1.1.8.1). Then the construction $C \mapsto \operatorname{Sing}_{\bullet }( | \overline{ \mathscr {F} }(C) | )$ determines a functor $\overline{\mathscr {G}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$, and the unit maps $\overline{ \mathscr {F} }(C) \rightarrow \operatorname{Sing}_{\bullet }( | \overline{ \mathscr {F}}(C) |)$ determine a levelwise weak homotopy equivlaence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$ (Theorem 3.5.4.1). By virtue of Corollary 7.5.4.11, it will suffice to show that the functor $\overline{\mathscr {G}}$ is a homotopy limit diagram if and only if $\overline{ \mathscr {G} }^{\operatorname{op}}$ is a homotopy limit diagram. This is clear, since the functors $\overline{ \mathscr {G} }$ and $\overline{ \mathscr {G} }^{\operatorname{op}}$ are isomorphic (see Example 1.3.2.5). $\square$

The notion of homotopy pullback square (see ยง3.4.1) can be regarded as a special case of the notion of homotopy limit diagram:

Proposition 7.5.4.13. Suppose we are given a commutative diagram of simplicial sets

7.50
\begin{equation} \begin{gathered}\label{equation:homotopy-pullback-as-homotopy-limit} \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_{0} \ar [d] \\ X_{1} \ar [r] & X, } \end{gathered} \end{equation}

which we identify with a functor $\mathscr {F}: [1] \times [1] \rightarrow \operatorname{Set_{\Delta }}$. Then (7.50) is a homotopy pullback square (in the sense of Definition 3.4.1.1) if and only if $\mathscr {F}$ is a homotopy limit diagram (in the sense of Definition 7.5.4.8).

Proof. Using Proposition 3.1.7.1, we can choose a levelwise weak homotopy equivalence $\alpha : \mathscr {F} \rightarrow \mathscr {F}'$, where $\mathscr {F}'$ is a diagram of Kan complexes. Using Corollaries 3.4.1.12 and 7.5.4.11, we can replace $\mathscr {F}$ by $\mathscr {F}'$ and thereby reduce to the case where (7.50) is a diagram of Kan complexes. By virtue of Corollary 3.4.1.6, the diagram (7.50) is a homotopy pullback square if and only if it induces a homotopy equivalence $f: X_{01} \rightarrow X_{0} \times _{X}^{\mathrm{h}} X_1$, where $X_0 \times _{X}^{\mathrm{h}} X_{1}$ is the homotopy fiber product of Construction 3.4.0.3. On the other hand, $\mathscr {F}$ is a homotopy limit diagram if and only if the composition $\iota \circ f$ is a homotopy equivalence, where

\[ \iota : X_{0} \times _{X}^{\mathrm{h}} X_{1} \hookrightarrow X_0 \times ^{\mathrm{h}}_{X} ( X_{1} \times ^{\mathrm{h}}_{X} X) \simeq \underset {\longleftarrow }{\mathrm{holim}}(F) \]

is the comparison map described in Example 7.5.2.15. The desired result now follows from the observation that $\iota $ is a homotopy equivalence (see Example 7.5.2.15). $\square$