$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 7.3.8.4 (Fubini's Theorem for Relative Colimits). Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a functor of $\infty $-categories, let $K$ and $L$ be simplicial sets, and let $v$ and $w$ denote the cone points of $K^{\triangleright } = K \star \{ v\} $ and $L^{\triangleright } = L \star \{ w\} $, respectively. Let $F: K^{\triangleright } \times L^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ be a diagram having the property that, for each vertex $k \in K$, the restriction $F(k, \bullet ): L^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ is a $U$-colimit diagram. The following conditions are equivalent:
- $(1)$
The restriction $F(\bullet ,w): K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ is a $U$-colimit diagram.
- $(2)$
The composition
\[ (K \times L)^{\triangleright } = (K \times L) \star \{ (v,w)\} \subseteq (K \star \{ v\} ) \times (L \star \{ w\} ) \xrightarrow {F} \operatorname{\mathcal{D}} \]
is a $U$-colimit diagram.
Proof.
Choose inner anodyne morphisms $K \hookrightarrow \operatorname{\mathcal{K}}$ and $L \hookrightarrow \operatorname{\mathcal{L}}$, where $\operatorname{\mathcal{K}}$ and $\operatorname{\mathcal{L}}$ are $\infty $-categories (Corollary 4.1.3.3). Then the induced map $K^{\triangleright } \star L^{\triangleright } \hookrightarrow \operatorname{\mathcal{K}}^{\triangleright } \times \operatorname{\mathcal{L}}^{\triangleright }$ is also inner anodyne (Example 4.3.6.7 and Lemma 1.5.7.5), so we can extend $F$ to a functor $\overline{F}: \operatorname{\mathcal{K}}^{\triangleright } \times \operatorname{\mathcal{L}}^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ (see Proposition 1.5.6.7). Using Lemma 7.2.2.2, can replace $F$ by $\overline{F}$ and thereby reduce to proving Corollary 7.3.8.4 in the special case where $K$ and $L$ are $\infty $-categories.
Set $\operatorname{\mathcal{C}}= K \times L^{\triangleright }$, and let us identify the cone $\operatorname{\mathcal{C}}^{\triangleright }$ with the full subcategory of $K^{\triangleright } \times L^{\triangleright }$ spanned by the objects of $\operatorname{\mathcal{C}}$ together with the cone point $(v,w)$. Combining Example 4.3.7.11 and with Corollary 7.2.1.19, we see that the inclusion $K \times \{ w\} \hookrightarrow \operatorname{\mathcal{C}}$ is right cofinal. Using Lemma 7.2.2.2 again, we see that $(1)$ is equivalent to the following:
- $(1')$
The restriction $F|_{ \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ is a $U$-colimit diagram.
Set $\operatorname{\mathcal{C}}^{0} = K \times L$. Our assumption that each $F(k, \bullet )$ is a $U$-colimit diagram guarantees that $F|_{\operatorname{\mathcal{C}}}$ is $U$-left Kan extended from $F|_{ \operatorname{\mathcal{C}}^{0} }$ (see Proposition 7.3.4.3). The equivalence $(1') \Leftrightarrow (2)$ now follows from Proposition 7.3.8.1.
$\square$