# Kerodon

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

Proposition 7.6.5.18. Let $F_0, F_1: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be functors of $\infty$-categories, which we identify with a diagram $\sigma : ( \bullet \rightrightarrows \bullet ) \rightarrow \operatorname{\mathcal{QC}}$. Suppose we are given an extension $\overline{\sigma }: ( \bullet \rightrightarrows \bullet )^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ of $\sigma$, corresponding to a functor of $\infty$-categories

$T: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}\times ^{\mathrm{h}}_{ (\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}.$

Then $\overline{\sigma }$ is an equalizer diagram in the $\infty$-category $\operatorname{\mathcal{QC}}$ if and only if $T$ is an equivalence of $\infty$-categories.

Proof. We proceed as in the proof of Proposition 7.6.4.8, with minor modifications. Let $\operatorname{\mathcal{A}}$ denote the simplicial path category of $( \bullet \rightrightarrows \bullet )^{\triangleleft }$, so that we can identify $\overline{\sigma }$ with a simplicial functor $\mathscr {F}: \operatorname{\mathcal{A}}\rightarrow \operatorname{QCat}$. Using Corollary 5.3.7.5, we can factor the functor $(F_0, F_1): \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}$ as a composition

$\operatorname{\mathcal{D}}\xrightarrow { U } \operatorname{\mathcal{D}}' \xrightarrow { (F'_0, F'_1) } \operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}},$

where $U$ is an equivalence of $\infty$-categories and $(F'_0, F'_1)$ is an isofibration. The pair $(F'_0, F'_1)$ can be identified with a morphism of simplicial sets $\sigma ': (\bullet \rightrightarrows \bullet ) \rightarrow \operatorname{\mathcal{QC}}$. Applying Remark 7.6.5.17, we can extend $\sigma '$ to a diagram $\overline{\sigma }': (\bullet \rightrightarrows \bullet )^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$, carrying the cone point to the $\infty$-category $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{D}}' \times ^{\mathrm{h}}_{ (\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}$. The diagram $\overline{\sigma }'$ corresponds to a simplicial functor $\mathscr {F}': \operatorname{\mathcal{A}}\rightarrow \operatorname{QCat}$. The morphisms $T$ and $U$ determine a natural transformation of simplicial functors $\mathscr {F} \rightarrow \mathscr {F}'$, hence also a morphism $\overline{\sigma } \rightarrow \overline{\sigma }'$ in the $\infty$-category $\operatorname{Fun}( ( \bullet \rightrightarrows \bullet )^{\triangleleft }, \operatorname{\mathcal{QC}})$. By virtue of Corollary 4.5.2.18, this natural transformation is an isomorphism of diagrams if and only if the functor $T$ is an equivalence of $\infty$-categories. Consequently, Proposition 7.6.5.18 is equivalent to the assertion that $\overline{\sigma }'$ is an equalizer diagram in $\operatorname{\mathcal{QC}}$ (Proposition 7.1.2.13).

Invoking Remark 7.6.5.17 again, we obtain another diagram $\overline{\sigma }''$ extending $\sigma '$, which carries the cone point of $(\bullet \rightrightarrows \bullet )^{\triangleleft }$ to the equalizer $\operatorname{Eq}(F'_0, F'_1) = \operatorname{\mathcal{D}}' \times _{ (\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}$ (formed in the category of simplicial sets). The diagram $\overline{\sigma }''$ corresponds to another simplicial functor $\mathscr {F}'': \operatorname{\mathcal{A}}\rightarrow \operatorname{QCat}$. Note that there is a natural inclusion map $\mathscr {F}'' \hookrightarrow \mathscr {F}'$, which carries the cone point to the inclusion

$\iota : \operatorname{\mathcal{D}}' \times _{ (\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}\subseteq \operatorname{\mathcal{D}}' \times _{ (\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) }^{\mathrm{h}} \operatorname{\mathcal{C}}.$

Since $(F'_0, F'_1)$ is an isofibration, the functor $\iota$ is an equivalence of $\infty$-categories (Corollary 4.5.2.22). It follows that the inclusion $\mathscr {F}'' \hookrightarrow \mathscr {F}'$ induces an isomorphism $\overline{\sigma }'' \rightarrow \overline{\sigma }'$ in the $\infty$-category $\operatorname{Fun}( ( \bullet \rightrightarrows \bullet )^{\triangleleft }, \operatorname{\mathcal{QC}})$. By virtue of Proposition 7.1.2.13, we are reduced to showing that $\overline{\sigma }''$ is an equalizer diagram in $\operatorname{\mathcal{QC}}$. This follows from the criterion of Proposition 7.6.5.14 (since $\iota$ is an equivalence of $\infty$-categories). $\square$