# Kerodon

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

Proposition 7.6.4.8. Suppose we are given a commutative diagram

7.60
$$\begin{gathered}\label{equation:all-squares-in-QCat} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{01} \ar [r] \ar [d] & \operatorname{\mathcal{C}}_{0} \ar [d]^-{ F_0 } \\ \operatorname{\mathcal{C}}_1 \ar [r]^-{ F_1 } & \operatorname{\mathcal{C}}} \end{gathered}$$

in the $\infty$-category $\operatorname{\mathcal{QC}}$, corresponding to a functor

$G: \operatorname{\mathcal{C}}_{01} \rightarrow \operatorname{\mathcal{C}}_{0} \times ^{\mathrm{h}}_{ \operatorname{\mathcal{C}}} ( \operatorname{\mathcal{C}}_1 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}).$

Then (7.60) is a pullback square in $\operatorname{\mathcal{QC}}$ if and only if the functor $G$ is an equivalence of $\infty$-categories.

Proof. Let us identify the diagram (7.60) with a functor of simplicial categories $\mathscr {F}: \operatorname{Path}[ [1] \times [1] ]_{\bullet } \rightarrow \operatorname{QCat}$. Using Corollary 5.3.7.5, we can factor the functor $F_0$ as a composition $\operatorname{\mathcal{C}}_0 \xrightarrow { T } \operatorname{\mathcal{C}}'_{0} \xrightarrow { F'_{0} } \operatorname{\mathcal{C}}$, where $T$ is an equivalence of $\infty$-categories and $F'_{0}$ is an isofibration. Let $\operatorname{\mathcal{C}}'_{01}$ denote the iterated homotopy fiber product $\operatorname{\mathcal{C}}'_{0} \times ^{\mathrm{h}}_{ \operatorname{\mathcal{C}}} ( \operatorname{\mathcal{C}}_1 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}})$. Then Example 7.6.4.7 supplies a commutative diagram

7.61
$$\begin{gathered}\label{equation:all-squares-in-QCat2} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}'_{01} \ar [r] \ar [d] & \operatorname{\mathcal{C}}'_{0} \ar [d]^-{F'_{0}} \\ \operatorname{\mathcal{C}}_{1} \ar [r]^-{F_1} & \operatorname{\mathcal{C}}} \end{gathered}$$

in the $\infty$-category $\operatorname{\mathcal{QC}}$, which we view as a functor of simplicial categories $\mathscr {F}': \operatorname{Path}[ [1] \times [1] ]_{\bullet } \rightarrow \operatorname{QCat}$. The morphisms $G$ and $T$ determine a natural transformation of simplicial functors $\mathscr {F} \rightarrow \mathscr {F}'$, which induces a natural transformation from the diagram (7.60) to the diagram (7.61) in the $\infty$-category $\operatorname{Fun}( \Delta ^1 \times \Delta ^1, \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 $G$ is an equivalence of $\infty$-categories. Consequently, Proposition 7.6.4.8 is equivalent to the assertion that (7.61) is a pullback square in the $\infty$-category $\operatorname{\mathcal{QC}}$ (see Proposition 7.1.2.13).

Note that we have a (strictly) commutative diagram of simplicial sets

7.62
$$\begin{gathered}\label{equation:all-squares-in-QCat3} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}'_{0} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{1} \ar [r] \ar [d] & \operatorname{\mathcal{C}}'_{0} \ar [d]^-{F'_{0}} \\ \operatorname{\mathcal{C}}_{1} \ar [r]^-{F'_1} & \operatorname{\mathcal{C}}, } \end{gathered}$$

which determines a subfunctor $\mathscr {F}'' \subseteq \mathscr {F}'$. Since $F'_0$ is an isofibration, it follows from Corollary 4.5.2.22, Proposition 5.3.7.4, and Corollary 4.5.2.23 that the inclusion maps

\begin{eqnarray*} \operatorname{\mathcal{C}}'_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 & \hookrightarrow & \operatorname{\mathcal{C}}'_{0} \times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} \operatorname{\mathcal{C}}_1 \\ & \hookrightarrow & \operatorname{\mathcal{C}}'_0 \times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} ( \operatorname{\mathcal{C}}_1 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \end{eqnarray*}

are equivalences of $\infty$-categories. Consequently, the inclusion $\mathscr {F}'' \hookrightarrow \mathscr {F}'$ is a levelwise categorical equivalence of simplicial functors and therefore induces an isomorphism from the diagram ( 7.62 ) to the diagram ( 7.61 ) in the $\infty$-category $\operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}})$. By virtue of Proposition 7.1.2.13, it will suffice to show that the diagram (7.62) is a pullback square in the $\infty$-category $\operatorname{\mathcal{QC}}$. This is a special case of Example 7.6.4.4, since (7.62) is a categorical pullback square (see Corollary 4.5.2.21). $\square$