$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 7.7.6.2. Suppose we are given a commutative diagram of simplicial sets
7.89
\begin{equation} \begin{gathered}\label{equation:anchor-easy} \xymatrix { \operatorname{\mathcal{E}}' \ar [r]^{\iota '} \ar [d]^{U} & \overline{\operatorname{\mathcal{E}}}' \ar [d]^{\overline{U}} \\ \operatorname{\mathcal{E}}\ar [r]^{\iota } \ar [d] & \overline{\operatorname{\mathcal{E}}} \ar [d] \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright } } \end{gathered} \end{equation}
satisfying the following conditions:
- $(a)$
Both squares in the diagram (7.89) are pullback squares, and the vertical maps are left fibrations.
- $(b)$
The morphism $U$ is a Kan fibration.
- $(c)$
The morphism $\iota $ is a weak homotopy equivalence.
Then $\iota '$ is a weak homotopy equivalence if and only if $\overline{U}$ is a Kan fibration.
Proof.
Assume that $\iota '$ is a weak homotopy equivalence; we will show that $\overline{U}$ is a Kan fibration (the converse is a special case of Corollary 3.3.7.4). Using Proposition 3.1.7.1, we can factor $\iota \circ U$ as a composition $\operatorname{\mathcal{E}}' \xrightarrow {\iota ''} \overline{\operatorname{\mathcal{E}}}'' \xrightarrow {\overline{V}} \overline{\operatorname{\mathcal{E}}}$, where $\iota ''$ is inner anodyne and $V$ is a Kan fibration. Our assumption that $\iota '$ is a weak homotopy equivalence guarantees that the lifting problem
\[ \xymatrix { \operatorname{\mathcal{E}}' \ar [d]^{ \iota ' } \ar [r] & \overline{\operatorname{\mathcal{E}}}'' \ar [d]^{V} \\ \overline{\operatorname{\mathcal{E}}}' \ar@ {-->}[ur]^{ F } \ar [r]^{\overline{U}} & \overline{\operatorname{\mathcal{E}}} } \]
admits a solution. To show that $\overline{U}$ is a Kan fibration, it will suffice to show that $F$ is an equivalence of left fibrations over $\overline{\operatorname{\mathcal{E}}}$ (Proposition 5.1.7.14). Using the criterion of Corollary 5.1.7.16, we are reduced to proving that for every vertex $X \in \overline{\operatorname{\mathcal{E}}}$, the induced map
\[ F_{X}: \{ X \} \times _{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}' \rightarrow \{ X\} \times _{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}'' \]
is a homotopy equivalence. We consider two cases:
Suppose that $X$ belongs to the image of $\iota $. In this case, the desired result follows by applying Proposition 3.2.8.1 to the diagram
\[ \xymatrix { \operatorname{\mathcal{E}}' \ar [d]^{U} \ar [r]^{ \iota '' } & \overline{\operatorname{\mathcal{E}}}'' \ar [d]^{V} \\ \operatorname{\mathcal{E}}\ar [r]^{\iota } & \overline{\operatorname{\mathcal{E}}}, } \]
since the vertical maps are Kan fibrations and the horizontal maps are weak homotopy equivalences.
Suppose that $X$ does not belong to the image of $\iota $: that is, it lies over the cone point $C \in \operatorname{\mathcal{C}}^{\triangleright }$. Set $\overline{\operatorname{\mathcal{E}}}_{C} = \{ C\} \times _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ and define $\overline{\operatorname{\mathcal{E}}}'_{C}$ and $\overline{\operatorname{\mathcal{E}}}''_{C}$ similarly, so that we have a commutative diagram
\[ \xymatrix { \overline{\operatorname{\mathcal{E}}}'_{C} \ar [r]^{ F_{C} } \ar [d]^{U_{C}} & \overline{\operatorname{\mathcal{E}}}''_{C} \ar [d]^{V_{C}} \\ \overline{\operatorname{\mathcal{E}}}_{C} \ar@ {=}[r] & \overline{\operatorname{\mathcal{E}}}_{C} } \]
The morphisms $U_{C}$ and $V_{C}$ are pullbacks of $U$ and $V$ respectively, and are therefore left fibrations. Assumption $(a)$ guarantees that the simplicial set $\overline{\operatorname{\mathcal{E}}}_{C}$ is a Kan complex (Proposition 4.4.2.1), so that $U$ and $V$ are Kan fibrations (Corollary 4.4.3.8). Consequently, to show that $F_{X}$ is a homotopy equivalence, it will suffice to show that $F_{C}$ is a homotopy equivalence (Proposition 3.2.8.1). By construction, we have a pullback diagram of simplicial sets
\[ \xymatrix { \overline{\operatorname{\mathcal{E}}}'_{C} \ar [r]^{F_ C} \ar [d] & \overline{\operatorname{\mathcal{E}}}''_{C} \ar [d] \\ \overline{\operatorname{\mathcal{E}}}' \ar [r]^{ F } & \overline{\operatorname{\mathcal{E}}}'', } \]
where $F$ is a weak homotopy equivalence by construction. We are therefore reduced to showing that the vertical maps in this diagram are weak homotopy equivalences. In fact, the vertical maps are right anodyne, since they arise as the pullback of the right anodyne inclusion $\{ C\} \hookrightarrow \operatorname{\mathcal{C}}^{\triangleright }$ along left fibrations (Corollary 7.2.3.13).
$\square$