I would like a reference for the following fact, which I believe to be true.
Consider the simplicial model category of Kan complexes with the Quillen model structure, and suppose given a commutative 3×3 square as below:
$\require{AMScd}$
\begin{CD}
X_1 @>>> X_{12} @<<< X_2\\
@VVV @VVV @VVV\\
Y_1 @>>> Y_{12} @<<< Y_2\\
@AAA @AAA @AAA\\
Z_1 @>>> Z_{12} @<<< Z_2
\end{CD}
Denote by $\operatorname{holim}(X)$, $\operatorname{holim}(Y)$, and $\operatorname{holim}(Z)$ the homotopy limits of the three rows, and by $\operatorname{holim}(C_1)$, $\operatorname{holim}(C_{12})$, and $\operatorname{holim}(C_2)$ the homotopy limits of the three columns. Then the claim is that
$$\operatorname{holim}(\operatorname{holim}(X)\to \operatorname{holim}(Y)\leftarrow \operatorname{holim}(Z))$$
is weakly equivalent to
$$\operatorname{holim}(\operatorname{holim}(C_1)\to \operatorname{holim}(C_{12})\leftarrow \operatorname{holim}(C_2)).$$
In the category of topological spaces this is Theorem 3.3.15 in the book ‘Cubical Homotopy Theory’ by Munson & Volic. It’s a general case of the idea ‘homotopy limits commute with homotopy limits.’ Others refer to it as a ‘Fubini theorem.’ I’ve been able to find surprisingly little documentation of this sort of thing, and I would like to know of a treatment of this kind of thing in any simplicial model category. Thanks.
Iterated homotopy pullbacks
homotopy-theorymodel-categoriessimplicial-stuff
Best Answer
It seems to me you have found an acceptable concrete argument for yourself, so let me discuss the general principle of "homotopy limits commute with homotopy limits". Your question can be considered to be a special case of the following question:
The answer is that there are natural weak equivalences: $$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{i : \mathcal{I}} \mathop{\textrm{ho}{\varprojlim}}_{j : \mathcal{J}} X (i, j) \longrightarrow \mathop{\textrm{ho}{\varprojlim}}_{(i, j) : \mathcal{I} \times \mathcal{J}} X (i, j)$$ $$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{j : \mathcal{J}} \mathop{\textrm{ho}{\varprojlim}}_{i : \mathcal{I}} X (i, j) \longrightarrow \mathop{\textrm{ho}{\varprojlim}}_{(i, j) : \mathcal{I} \times \mathcal{J}} X (i, j)$$
(The reason why this is sometimes referred to as a "Fubini theorem" is that there is an even more general result concerning homotopy ends, and the corresponding result about ordinary ends is (for better or worse) called a "Fubini theorem" because ends are written with an $\int$ sign.)
In fact, when $\mathcal{M}$ is a simplicial model category and each $X (i, j)$ is a fibrant object in $\mathcal{M}$, there is a very satisfactory theory of homotopy limits in which the comparison morphisms mentioned above are isomorphisms. Specifically, if $\mathcal{M}$ is the category of simplicial sets with the Kan–Quillen model structure, then the Bousfield–Kan theory of homotopy limits has this property, and it is straightforward to generalise the Bousfield–Kan theory to other simplicial model categories.
Since there is not yet a consensus regarding terminology in this subject, let me make some definitions.
Definition. Given a category $\mathcal{I}$ and functors $G : \mathcal{I}^\textrm{op} \to \textbf{sSet}$ and $F : \mathcal{I} \to \textbf{sSet}$, the bar construction $\mathrm{B} (G, \mathcal{I}, F)$ is the simplicial set where $$\mathrm{B} (G, \mathcal{I}, F)_n = \coprod_{(i_0, \ldots, i_n)} G (i_n)_n \times \mathcal{I} (i_{n-1}, i_n) \times \cdots \times \mathcal{I} (i_0, i_1) \times F (i_0)_n$$ with face operators defined by composition in $\mathcal{I}$ and the actions of $G$ and $F$, and degeneracy operators defined by inserting identity morphisms in $\mathcal{I}$.
For brevity, we write $\mathrm{B} (G, \mathcal{I}, \mathcal{I})$ for the functor $\mathcal{I}^\textrm{op} \to \textbf{sSet}$ defined by $i' \mapsto \mathrm{B} (G, \mathcal{I}, \mathcal{I}^{i'})$, where $\mathcal{I}^{i'} = \mathcal{I} (i', -)$.
Definition. Given a category $\mathcal{I}$, a functor $G : \mathcal{I} \to \textbf{sSet}$, and a functor $F : \mathcal{I} \to \mathcal{M}$, the cobar construction $\mathrm{C} (G, \mathcal{I}, F)$ is an object in $\mathcal{M}$ equipped with isomorphisms $$\mathcal{M} (T, \mathrm{C} (G, \mathcal{I}, F)) \cong [\mathcal{I}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}), \mathcal{M} (T, F))$$ simplicially natural in $T$, where $[\mathcal{I}, \textbf{sSet}]$ is the simplicially enriched category of functors $\mathcal{I} \to \textbf{sSet}$.
Proposition / Definition. Let $F : \mathcal{I} \to \mathcal{M}$ be a functor where each $F (i)$ is fibrant and let $G : \mathcal{I} \to \textbf{sSet}$ be any functor. Then the cobar construction $\mathrm{C} (G, \mathcal{I}, F)$ computes the homotopy limit of $F$ weighted by $G$. In particular, if $G (i)$ is (weakly) contractible for all $i$, then $\mathrm{C} (G, \mathcal{I}, F)$ computes $\mathop{\textrm{ho}{\varprojlim}}_\mathcal{I} F$.
To be very concrete, let us define $\mathop{\textrm{ho}{\varprojlim}}_\mathcal{I} F$ to mean the cobar construction $\mathrm{C} (G, \mathcal{I}, F)$ where $G (i) = \Delta^0$ for all $i$, bearing in mind that every $F (i)$ must be fibrant for this definition to work well. Then the claim that "homotopy limits commute with homotopy limits" comes down to the following straightforward calculation:
Lemma. Let $F : \mathcal{I} \times \mathcal{J} \to \mathcal{M}$, $G : \mathcal{I} \to \textbf{sSet}$, and $H : \mathcal{J} \to \textbf{sSet}$ be functors. Then we have a natural isomorphism: $$\mathrm{C} (G, \mathcal{I}, \mathrm{C} (H, \mathcal{J}, F)) \cong \mathrm{C} (G \boxtimes H, \mathcal{I} \times \mathcal{J}, F)$$ Here, $G \boxtimes H : \mathcal{I} \times \mathcal{J} \to \textbf{sSet}$ is defined by $(G \boxtimes H) (i, j) = G (i) \times H (j)$.
Proof. By definition, $$\mathcal{M} (T, \mathrm{C} (G, \mathcal{I}, \mathrm{C} (H, \mathcal{J}, F))) \cong [\mathcal{I}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}), [\mathcal{J}, \textbf{sSet}] (\mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}), \mathcal{M} (T, F)))$$ and it can be shown (using the so-called Fubini theorem, but from ordinary category theory) that \begin{multline} [\mathcal{I}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}), [\mathcal{J}, \textbf{sSet}] (\mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}), \mathcal{M} (T, F))) \\ \cong [\mathcal{I} \times \mathcal{J}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}) \times \mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}), \mathcal{M} (T, F)) \end{multline} but it is clear that $$\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}) \times \mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}) \cong \mathrm{B} (G \boxtimes H, (\mathcal{I} \times \mathcal{J})^\textrm{op}, (\mathcal{I} \times \mathcal{J})^\textrm{op})$$ so we are done. ◼