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

証明
U：Grp → Set を忘却関手(>>72)とする。
>>48より
>>29の標準射 φ：colim[i] lim[p] UF(i, p) → lim[p] colim[i] UF(i, p) は同型である。

colim[i] lim[p] UF(i, p)
= colim[i] U(lim[p] F(i, p))　← >>72
= U(colim[i] lim[p] F(i, p))　← >>69

lim[p] colim[i] F(i, p)
= lim[p] U(colim[i] F(i, p))　← >>69
= U(lim[p] colim[i] F(i, p))　← >>72

よって、φ = U(ψ) であり、ψ は同型である。
証明終