Kerodon

Proof. We will prove that $\theta $ is an isomorphism; the proof for $\theta '$ is similar. Fix an $n$-simplex $\sigma $ of $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})_{/f}$, which we identify with a morphism of simplicial sets $\overline{f}: \Delta ^ n \star K \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ satisfying $\overline{f}|_{K} = f$. Let $\overline{f}_0 = \overline{f}|_{ \Delta ^ n }$. Using Proposition 4.3.5.13, we can identify $\overline{f}$ with a morphism of simplicial sets $g: K \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}})_{\overline{f}_0 / }$. We wish to show that $\sigma $ can be lifted uniquely to an $n$-simplex of $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})_{ / \operatorname{N}_{\bullet }(F) }$. Equivalently, we wish to show that $g$ admits a unique factorization

for which the composite map $\operatorname{N}_{\bullet }(\operatorname{\mathcal{K}}) \xrightarrow { \overline{g} } \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})_{ \overline{f}_0 / } \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is equal to $\operatorname{N}_{\bullet }(F)$. This follows our assumption that $u$ exhibits $\operatorname{\mathcal{K}}$ as a homotopy category of $K$, since the simplicial set $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})_{ \overline{f}_0 / }$ is isomorphic to the nerve of a category (see Example 4.3.5.7). $\square$