命題 582
I を小さいフィルター圏(>>36)とする。
J を有限圏(>>43)とする。
Set を小さい集合(代数的整数論017の321)全体の圏とする。
F：I×J → Set を関手とする。
このとき>>29の標準射 ψ：colim[i] lim F(i, −) → lim[a] colim F(−, a) は同型である。

証明
J の対象全体を {a_1、．．．、a_n} とする。
F(i, a_k) の元を (i, x_k) と書く。
ここで x_k ∈ F(i, a_k) である。

lim F(i, −) は F(i, a_1)×．．．×F(i, a_n) の部分集合である。
よって、lim F(i, −) の元は ((i, x_1)、．．．、(i, x_n)) で表される。
この元の標準射 lim F(i, −) → colim[i] lim F(i, −) による像を
[(i, x_1)、．．．、(i, x_n)] と書く。

他方、(i, x_k) ∈ F(i, a_k) の標準射 F(−, a_k) → colim F(−, a) による像を
[i, x_k] と書く。
このとき、ψ([(i, x_1)、．．．、(i, x_n)]) = ([i, x_1]、．．．、[i, x_n]) である。

>>45の(1)より lim[a] colim F(−, a) の元は ([i, x_1]、．．．、[i, x_n]) と書ける。
この元に [(i, x_1)、．．．、(i, x_n)] を対応させる写像 φ が ψ の逆写像である。
φ が矛盾なく定義(well-defined)されることは以下のようにして分かる。

([i, x_1]、．．．、[i, x_n]) = ([j, y_1]、．．．、[j, y_n]) とする。
>>44より射 u：i → k、v：j → k があり
F(u, a_1)(x_1) = F(v, a_1)(y_1)、．．．、F(u, a_n)(x_n) = F(v, a_n)(y_n) となる。
よって、[(i, x_1)、．．．、(i, x_n)] = [(j, y_1)、．．．、(j, y_n)] である。
証明終