$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 4.4.3.19 (Pullbacks of Isofibrations). Suppose we are given a pullback diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}' \ar [r]^-{F} \ar [d]^{q'} & \operatorname{\mathcal{C}}\ar [d]^{q} \\ \operatorname{\mathcal{D}}' \ar [r]^-{F'} & \operatorname{\mathcal{D}}, } \]
where $q$ is an isofibration of $\infty $-categories and $\operatorname{\mathcal{D}}'$ is an $\infty $-category. Then:
- $(1)$
The simplicial set $\operatorname{\mathcal{C}}'$ is an $\infty $-category.
- $(2)$
The diagram of Kan complexes
4.17
\begin{equation} \begin{gathered}\label{equation:pullback-of-core} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}'^{\simeq } \ar [r] \ar [d]^{q'^{\simeq }} & \operatorname{\mathcal{C}}^{\simeq } \ar [d]^{q^{\simeq }} \\ \operatorname{\mathcal{D}}'^{\simeq } \ar [r] & \operatorname{\mathcal{D}}^{\simeq } } \end{gathered} \end{equation}
is a pullback square and a homotopy pullback square.
- $(3)$
A morphism $u: X \rightarrow Y$ in the $\infty $-category $\operatorname{\mathcal{C}}'$ is an isomorphism if and only if $F(u)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$ and $q'(u)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}'$.
- $(4)$
The morphism $q'$ is an isofibration of $\infty $-categories.
Proof.
Since $q$ is an isofibration, it is an inner fibration. It follows that the morphism $q'$ is also an inner fibration (Remark 4.1.1.5). Since $\operatorname{\mathcal{D}}'$ is an $\infty $-category, the simplicial set $\operatorname{\mathcal{C}}'$ is also an $\infty $-category (Remark 4.1.1.9). This proves $(1)$.
Let $\operatorname{\mathcal{E}}$ denote the fiber product $\operatorname{\mathcal{C}}^{\simeq } \times _{ \operatorname{\mathcal{D}}^{\simeq } } \operatorname{\mathcal{D}}'^{\simeq }$, which we regard as a simplicial subset of $\operatorname{\mathcal{C}}' = \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}'$. It follows from Proposition 4.4.3.7 that $q$ restricts to a Kan fibration $q^{\simeq }: \operatorname{\mathcal{C}}^{\simeq } \rightarrow \operatorname{\mathcal{D}}^{\simeq }$. The projection map $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}'^{\simeq }$ is a pullback of $q^{\simeq }$, and is therefore also a Kan fibration. Since $\operatorname{\mathcal{D}}'^{\simeq }$ is a Kan complex (Corollary 4.4.3.11), it follows that $\operatorname{\mathcal{E}}$ is a Kan complex (Remark 3.1.1.11). Applying Corollary 4.4.3.18, we deduce that $\operatorname{\mathcal{E}}$ is contained in the core $\operatorname{\mathcal{C}}'^{\simeq } \subseteq \operatorname{\mathcal{C}}'$, which proves that the diagram (4.17) is a pullback square. Since $q^{\simeq }$ is a Kan fibration, it is also a homotopy pullback square (Example 3.4.1.3). This proves assertion $(2)$, and assertion $(3)$ is an immediate consequence.
To complete the proof of $(4)$, it will suffice to show that the morphism $q'$ satisfies condition $(\ast )$ of Definition 4.4.1.4. Let $Y'$ be an object of $\operatorname{\mathcal{C}}'$ and let $\overline{u}': \overline{X}' \rightarrow q'(Y')$ be an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}'$; we wish to show that $\overline{u'}$ can be written as $q'( u')$ for some isomorphism $u': X' \rightarrow Y'$ in the $\infty $-category $\operatorname{\mathcal{C}}'$. By virtue of $(3)$, this is equivalent to showing that $F'(\overline{u}')$ can be written as $q(u)$ for some isomorphism $u: X \rightarrow F(Y)$ in the $\infty $-category $\operatorname{\mathcal{C}}$, which follows from our assumption that $q$ is an isofibration.
$\square$