命題
C を小さい前加法圏(過去スレ019の504)とし、Ab をアーベル群の圏とする。
このとき Add(C, Ab)(>>413) はGrothendieck圏(>>236)である。

証明
>>414より Add(C, Ab)(>>413) はアーベル圏である。
Ab はAB5(>>121)を満たすから>>417より Add(C, Ab) もAB5を満たす。
>>433より Add(C, Ab) は分離対象を持つ。
よって、Add(C, Ab) はGrothendieck圏(>>236)である。
証明終