Kerodon

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

Remark 7.7.0.2 (Distributivity). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $K$ be a simplicial set. Assume that $\operatorname{\mathcal{C}}$ admits pullbacks and $K$-indexed colimits. Let $\mathscr {F}: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram equipped with a natural transformation $\beta : \mathscr {F} \rightarrow \underline{C}$. Then $\beta $ determines a map $u: \varinjlim (\mathscr {F}) \rightarrow C$, which is characterized (up to homotopy) by the existence of a $2$-simplex $\sigma :$

\[ \xymatrix { & \underline{ \varinjlim (\mathscr {F}) } \ar [dr]^{ \underline{u} } & \\ \mathscr {F} \ar [ur]^{\alpha } \ar [rr]^{ \beta } & & \underline{C} } \]

where $\alpha $ denotes a fixed natural transformation exhibiting $\varinjlim ( \mathscr {F} )$ as a colimit of $\mathscr {F}$. Suppose we are given morphism $f: C' \rightarrow C$ of $\operatorname{\mathcal{C}}$. Since $\operatorname{\mathcal{C}}$ admits pullbacks, we can form a pullback square $\tau :$

\[ \xymatrix { C' \times _{C} \varinjlim (\mathscr {F}) \ar [r] \ar [d]^{f'} & C' \ar [d]^{f} \\ \varinjlim (\mathscr {F}) \ar [r]^{f} & C. } \]

In the $\infty $-category $\operatorname{Fun}(K, \operatorname{\mathcal{C}})$, we can then choose a (levelwise) limit diagram

\[ \xymatrix { \mathscr {F}' \ar [r]^{\alpha '} \ar [d] & \underline{ C' \times _{C} \varinjlim (\mathscr {F}) } \ar [r] \ar [d] & \underline{C}' \ar [d]^{ \underline{f} } \\ \mathscr {F} \ar [r]^{\alpha } & \underline{\varinjlim (\mathscr {F})} \ar [r]^{ \underline{u} } & \underline{C}, } \]

where restriction to the bottom half of the diagram is given by $\sigma $ and the right side is the image of $\tau $ under the diagonal map $\operatorname{\mathcal{C}}\rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Since the outer rectangle is a fiberwise pullback square (Proposition 7.6.2.28), we can identify $\alpha '$ with a comparison map

\[ \theta : \varinjlim (\mathscr {F}') = \varinjlim _{k \in K}(C' \times _ C \mathscr {F}(k)) \rightarrow C' \times _{C} (\varinjlim _{k \in K} \mathscr {F}(k) ). \]

If the colimit of $\mathscr {F}$ is universal, then $\theta $ is an isomorphism.