定理(Freyd)
Ab をアーベル群の圏とする。
任意の小さいアーベル圏 C に対して、
完全(過去スレ019の661)な埋め込み(過去スレ018の34) F：C → Ab が存在する。

証明
任意の X ∈ C に対して h^X ∈ Add(C, Ab) を>>423で定義した関手とする。
G = Σh^X とおく。ここで X は C の対象全体を動くものとする。
>>433より G は分離対象(過去スレ018の212)である。
>>447より Add(C, Ab) はGrothendieck圏である。
よって、>>404より G は単射包絡(>>92) E を持つ。
>>434より E は右完全(過去スレ019の660)である。
>>446より G は単関手(>>435)である。
>>441より E は単関手である。
よって、E は完全(過去スレ019の661)である。

Y ≠ 0 を C の対象とする。
0 ≠ 1_Y ∈ h^Y(Y)
よって、G(Y) = Σh^X(Y) ≠ 0 である。
G ⊂ E であるから、E(Y) ≠ 0 である。
よって、>>443より E は忠実である。
>>442より E は埋め込みと仮定してよい。
証明終