Kerodon

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

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$

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.6.5.6). Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$. Applying Corollary 7.4.5.13, 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

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

where $\iota $ and $\overline{\iota }$ are the comparison maps of Remark 7.5.2.12. Since the category $\operatorname{\mathcal{C}}^{\triangleleft }$ has an initial object, the morphism $\overline{\iota }$ is a homotopy equivalence (Proposition 7.5.2.13). 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$

Proof. By virtue of Proposition 7.4.5.16, 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.6.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$

Proof. Combine Example 7.5.4.2 with Proposition 7.5.4.5. $\square$

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

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

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

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$

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

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$

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.2.3.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 equivalence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$ (Theorem 3.6.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.4.2.5). $\square$

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.51) is a diagram of Kan complexes. By virtue of Corollary 3.4.1.6, the diagram (7.51) 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

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