# Kerodon

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

Corollary 4.4.3.18 (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{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}$$

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.17, 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$