# Kerodon

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

Proposition 4.8.4.20. Let $n$ be an integer and suppose we are given a pullback diagram of $\infty$-categories

$\xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{C}}_{01} \ar [r]^-{G_0} \ar [d]^{G_1} & \operatorname{\mathcal{C}}_0 \ar [d]^{F_0} \\ \operatorname{\mathcal{C}}_1 \ar [r]^-{F_1} & \operatorname{\mathcal{C}}. }$

If $\operatorname{\mathcal{C}}$ is an $(n,1)$-category, then the diagram

$\xymatrix@C =50pt@R=50pt{ \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_{01})} \ar [r] \ar [d] & \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_0)} \ar [d] \\ \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_1)} \ar [r] & \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})} }$

is also a pullback square.

Proof. If $n \leq 0$, then we can identify $\operatorname{\mathcal{C}}_{01}$ with the full subcategory of $\operatorname{\mathcal{C}}_0 \times \operatorname{\mathcal{C}}_1$ spanned by those objects $(C_0, C_1)$ satisfying $F_0(C_0) = F_1(C_1)$. In this case, the desired result follows by combining Remarks 4.8.4.18 and 4.8.4.19. We may therefore assume without loss of generality that $n > 0$. Fix a simplicial set $A$; we wish to show that the tautological map

$\theta : \operatorname{Hom}_{\operatorname{Set_{\Delta }}}( A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_{01})} ) \rightarrow \operatorname{Hom}_{\operatorname{Set_{\Delta }}}( A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_0)} ) \times _{ \operatorname{Hom}_{\operatorname{Set_{\Delta }}}(A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})} )} \operatorname{Hom}_{\operatorname{Set_{\Delta }}}( A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_1)} ).$

is a monomorphism. We first show that $\theta$ is injective. Suppose we are given a pair of maps $u,u': A \rightarrow \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_{01})}$ satisfying $\theta (u) = \theta (u')$; we wish to show that $u = u'$. Using Remark 4.8.4.12, we can choose representatives of $u$ and $u'$ by morphisms $\widetilde{u}, \widetilde{u}': \operatorname{sk}_{n}(A) \rightarrow \operatorname{\mathcal{C}}_{01}$. Our assumption that $\theta (u) = \theta (u')$ guarantees that there are natural isomorphisms

$\alpha _0: G_0 \circ \widetilde{u} \rightarrow G_0 \circ \widetilde{u}' \quad \quad \alpha _1: G_1 \circ \widetilde{u} \rightarrow G_1 \circ \widetilde{u}'$

which are the identity when restricted to $\operatorname{sk}_{n-1}(A)$. It follows from the proof of Proposition 4.8.1.7 shows that $\alpha _0$ and $\alpha _1$ have the same image in $\operatorname{Fun}( \operatorname{sk}_{n}(A), \operatorname{\mathcal{C}})$. We can therefore identify the pair $(\alpha _0, \alpha _1)$ with an isomorphism from $\widetilde{u}$ to $\widetilde{u}'$ (which is the identity when restricted to $\operatorname{sk}_{n-1}(A)$), which proves that $u = u'$.

We now prove that $\theta$ is surjective. Choose an element $(u_0, u_1)$ of the fiber product $\operatorname{Hom}_{\operatorname{Set_{\Delta }}}( A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_0)} ) \times _{\operatorname{Hom}_{\operatorname{Set_{\Delta }}}(A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})} )} \operatorname{Hom}_{\operatorname{Set_{\Delta }}}( A, \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}_1)} )$. Using Remark 4.8.4.12, we can choose representatives of $u_0$ and $u_1$ by morphisms $\widetilde{u}_0: \operatorname{sk}_{n+1}(A) \rightarrow \operatorname{\mathcal{C}}_0$ and $\widetilde{u}_1: \operatorname{sk}_{n+1}(A) \rightarrow \operatorname{\mathcal{C}}_1$. Since $\operatorname{\mathcal{C}}$ is an $(n,1)$-category, the tautological map $\operatorname{\mathcal{C}}\rightarrow \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})}$ is an isomorphism. It follows that $F_0 \circ \widetilde{u}_0$ coincides with $F_1 \circ \widetilde{u}_1$, so that the pair $( \widetilde{u}_0, \widetilde{u}_1 )$ determines a morphism $\widetilde{u}: \operatorname{sk}_{n+1}(A) \rightarrow \operatorname{\mathcal{C}}$. This represents a morphism $u: A \rightarrow \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})}$ satisfying $\theta (u) = (u_0, u_1)$. $\square$