= Solution
A precise <commutation of iterated categorical limits> statement is the following. For small <categories> $\mathcal I,\mathcal J$ and $F:\mathcal I\times\mathcal J\to\mathcal D$, if every column <categorical limit> and the resulting $\mathcal J$-limit exist, then
$$
\lim_j\lim_iF(i,j)\cong\lim_{(i,j)}F(i,j).
$$
If every row <categorical limit> and the resulting $\mathcal I$-limit also exist, then
$$
\boxed{\lim_j\lim_iF(i,j)\cong\lim_{(i,j)}F(i,j)\cong\lim_i\lim_jF(i,j).}
$$
Each <isomorphism> is the unique one identifying all projections to $F(i,j)$. Indeed, the preceding part proves that each iterated <categorical limit> has the <universal property> of the whole product <diagram in a category>. Its uniqueness gives the canonical <isomorphism>. Equivalently, <categorical cones> with vertex $X$ over the product <diagram in a category> are exactly compatible families, indexed by $j$, of <categorical cones> over $F(-,j)$; regrouping the same compatibility equations cannot change their representing object. In a <complete category> all the stated existence hypotheses hold for small $\mathcal I,\mathcal J$. The theorem is about <categorical limits> with <categorical limits>, and makes no unconditional claim about commuting a <categorical limit> with a <colimit>.
Back to article page
