命題 592
I を小さいフィルター圏(>>36)とする。
J を有限圏(>>43)とする。
Ab を小さいアーベル群(過去スレpart2の893)の圏とする。
F：I×J → Grp をAbとする。
このとき>>29の標準射 ψ：colim[i] lim F(i, −) → lim[a] colim F(−, a) は同型である。

証明
>>73と同様である。