Filtered colimits commute with finite limits

Remarks

The proof uses the explicit form of a filtered colimit of sets. It is the disjoint union of the sets, where two elements are identified when they become equal at some later stage. A finite limit involves only finitely many elements and finitely many equations. Because $I$ is filtered, all of them can be moved to one common stage, which gives both injectivity and surjectivity.

Both hypotheses matter. For $J$ infinite, take $I = \N$, $J = \N$ seen as a discrete category, and $F(n, j)$ a one-point set when $j < n$ and empty otherwise. Then each $\prod_j F(n, j)$ is empty, while each $\operatorname{colim}_n F(n, j)$ is a point. So the left side is empty and the right side is a point. For $I$ not filtered, coproducts do not commute with products: $(A \sqcup B) \times (A \sqcup B)$ is larger than $(A \times A) \sqcup (B \times B)$ when $A$ and $B$ are not empty.

Going deeper

For a student

The theorem explains why filtered colimits are so well behaved in algebra. For example, a filtered colimit of groups or modules can be computed on underlying sets, because the group operations are maps out of finite products, which are finite limits. It also shows that filtered colimits of exact sequences of modules are exact. The same result holds in any locally finitely presentable category, and finitely presentable objects are defined by a closely related property of the hom functor.