命題
Grp を群の圏とする。
I を小さいフィルター圏(>>97)とする。
F：I → Grp を関手とする。

このとき L = colim F (過去スレ018の847) が存在し、
次の条件を満たす。

(1) L = ∪f_i(F(i))
　　ここで f_i：F(i) → L は標準射である。

(2) Ker(f_i) = ∪Ker(u)
　　ここで u は i を定義域とする全ての射を動く。

証明
>>111で定義した L が colim F であることは>>110から明らかである。
L の作り方から (1) と (2) も明らかである。
証明終