Lemma 8.3.7.7. Suppose we are given a commutative diagram of $\infty $-categories
8.61
\begin{equation} \begin{gathered}\label{equation:covariant-transport-categorical-pullback-square} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_{00} \ar [dr]^{ U_{00} } \ar [rr] \ar [dd] & & \operatorname{\mathcal{E}}_{01} \ar [dd] \ar [dr]^{U_{01}} & \\ & \operatorname{\mathcal{D}}_{00} \ar [rr] \ar [dd] & & \operatorname{\mathcal{D}}_{01} \ar [dd] \\ \operatorname{\mathcal{E}}_{10} \ar [dr]^{U_{10} } \ar [rr] & & \operatorname{\mathcal{E}}_{11} \ar [dr]^{U_{11} } & \\ & \operatorname{\mathcal{D}}_{10} \ar [rr] & & \operatorname{\mathcal{D}}_{11} } \end{gathered} \end{equation}
satisfying the following conditions:
- $(1)$
The front face $\sigma $:
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}_{00} \ar [r] \ar [d] & \operatorname{\mathcal{D}}_{01} \ar [d] \\ \operatorname{\mathcal{D}}_{10} \ar [r] & \operatorname{\mathcal{D}}_{11} } \]
is a categorical pullback square.
- $(2)$
The back face $\tau :$
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_{00} \ar [r] \ar [d] & \operatorname{\mathcal{E}}_{01} \ar [d] \\ \operatorname{\mathcal{E}}_{10} \ar [r] & \operatorname{\mathcal{E}}_{11} } \]
is a categorical pullback square.
- $(3)$
Each of the functors $U_{ij}: \operatorname{\mathcal{E}}_{ij} \rightarrow \operatorname{\mathcal{D}}_{ij}$ is a left fibration with covariant transport representation $\mathscr {F}_{ij}: \operatorname{\mathcal{D}}_{ij} \rightarrow \operatorname{\mathcal{S}}$.
Then there exists a pullback square
\[ \xymatrix@R =50pt@C=50pt{ \mathscr {F}_{00} \ar [r] \ar [d] & \mathscr {F}_{01} |_{ \operatorname{\mathcal{D}}_{00} } \ar [d] \\ \mathscr {F}_{10} |_{ \operatorname{\mathcal{D}}_{00} } \ar [r] & \mathscr {F}_{11} |_{ \operatorname{\mathcal{D}}_{00} } } \]
in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{D}}_{00}, \operatorname{\mathcal{S}})$.
Proof.
Let us regard $\sigma $ and $\tau $ as functors from the partially ordered set $[1] \times [1]$ to the category of simplicial sets, and let $\operatorname{\mathcal{D}}= \operatorname{N}_{\bullet }^{\sigma }( [1] \times [1] )$ and $\operatorname{\mathcal{E}}= \operatorname{N}_{\bullet }^{\tau }( [1] \times [1] )$ denote the weighted nerves of Definition 5.3.3.1. The diagram (8.61) can be identified with a natural transformation from $\tau $ to $\sigma $, which induces a functor of $\infty $-categories $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$. By construction, we have a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^{ U } \ar [dr] & & \operatorname{\mathcal{D}}\ar [dl] \\ & \Delta ^1 \times \Delta ^1, & } \]
where the vertical maps are cocartesian fibrations (Corollary 5.3.3.16). In what follows, we will identify each $\operatorname{\mathcal{D}}_{ij}$ and $\operatorname{\mathcal{E}}_{ij}$ with the full subcategories of $\operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}$ given by the fiber of the vertex $(i,j) \in \Delta ^1 \times \Delta ^1$, so that $U_{ij} = U|_{ \operatorname{\mathcal{D}}_{ij} }$.
It follows from Corollary 5.3.3.18 that $U$ is a left fibration. Let $\mathscr {F}: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{S}}$ be a covariant transport representation for $U$. Without loss of generality, we may assume that each $\mathscr {F}_{ij}$ coincides with the restriction $\mathscr {F}|_{ \operatorname{\mathcal{D}}_{ij} }$. Let $\widetilde{\sigma }: [1] \times [1] \rightarrow \operatorname{Set_{\Delta }}$ be the constant functor taking the value $\operatorname{\mathcal{D}}_{00}$. There is a unique natural transformation $\widetilde{\sigma } \rightarrow \sigma $ which is the identity when evaluated at $(0,0) \in [1] \times [1]$, which induces a functor
\[ T: \operatorname{\mathcal{D}}_{00} \times \Delta ^1 \times \Delta ^1 \simeq \operatorname{N}_{\bullet }^{\widetilde{\sigma }}( [1] \times [1] ) \rightarrow \operatorname{N}_{\bullet }^{\sigma }( [1] \times [1] ) = \operatorname{\mathcal{D}}. \]
We can then identify the composition $\mathscr {F} \circ T$ with a commutative diagram
8.62
\begin{equation} \begin{gathered}\label{equation:covariant-transport-categorical-pullback-square2} \xymatrix@R =50pt@C=50pt{ \mathscr {F}_{00} \ar [r] \ar [d] & \mathscr {F}_{01} |_{ \operatorname{\mathcal{D}}_{00} } \ar [d] \\ \mathscr {F}_{10} |_{ \operatorname{\mathcal{D}}_{00} } \ar [r] & \mathscr {F}_{11} |_{ \operatorname{\mathcal{D}}_{00} } } \end{gathered} \end{equation}
in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{D}}_{00}, \operatorname{\mathcal{S}})$. We will complete the proof by showing that this diagram is a (levelwise) pullback square.
Fix an object $D_{00} \in \operatorname{\mathcal{D}}_{00}$, having image $D_{ij} \in \operatorname{\mathcal{D}}_{ij}$ for each pair $i,j \in [1]$. Evaluation at $D_{00}$ then carries (8.62) to a diagram
8.63
\begin{equation} \begin{gathered}\label{equation:covariant-transport-categorical-pullback-square3} \xymatrix@R =50pt@C=50pt{ \mathscr {F}_{00}(D_{00} ) \ar [r] \ar [d] & \mathscr {F}_{01}( D_{01} ) \ar [d] \\ \mathscr {F}_{10}( D_{10} ) \ar [r] & \mathscr {F}_{11}( D_{11} ) } \end{gathered} \end{equation}
in the $\infty $-category $\operatorname{\mathcal{S}}$, and we wish to show that (8.63) is a pullback square. Using Example 5.6.5.6, we can identify (8.63) with the homotopy coherent nerve $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \tau _0 )$, where $\tau _0: [1] \times [1] \rightarrow \operatorname{Kan}$ is the commutative diagram of Kan complexes
\[ \xymatrix@R =50pt@C=50pt{ U_{00}^{-1}( D_{00} ) \ar [r] \ar [d] & U_{01}^{-1}( D_{01} ) \ar [d] \\ U_{10}^{-1}( D_{10} ) \ar [r] & U_{11}^{-1}( D_{11} ). } \]
By construction, we have a pullback diagram
8.64
\begin{equation} \begin{gathered}\label{equation:covariant-transport-categorical-pullback-square4} \xymatrix@R =50pt@C=50pt{ \tau _0 \ar [r] \ar [d] & \tau \ar [d] \\ \underline{\Delta ^0} \ar [r] & \sigma } \end{gathered} \end{equation}
in the category $\operatorname{Fun}( [1] \times [1], \operatorname{\mathcal{QC}})$. For each pair $i,j \in [1]$, assumption $(3)$ guarantees that $U_{ij}: \operatorname{\mathcal{E}}_{ij} \rightarrow \operatorname{\mathcal{D}}_{ij}$ is an isofibration of $\infty $-categories, so that evaluation at $(i,j)$ carries (8.64) to a categorical pullback square of $\infty $-categories. Applying Example 7.6.3.4, we obtain a pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{N}_{\bullet }^{\operatorname{hc}}( \tau _0 ) \ar [r] \ar [d] & \operatorname{N}_{\bullet }^{\operatorname{hc}}( \tau ) \ar [d] \\ \underline{ \Delta ^0 } \ar [r] & \operatorname{N}_{\bullet }^{\operatorname{hc}}( \sigma ) } \]
in the $\infty $-category $\operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{QC}})$. Assumptions $(2)$ and $(3)$ guarantee that $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\sigma )$ and $\operatorname{N}_{\bullet }(\tau )$ are limit diagrams in the $\infty $-category $\operatorname{\mathcal{QC}}$ (Example 7.6.3.4). Applying Corollary 7.3.8.8, we conclude that $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \tau _0 )$ is also a limit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$, and therefore also in the full subcategory $\operatorname{\mathcal{S}}\subset \operatorname{\mathcal{QC}}$.
$\square$