過去スレ017の819の双対

C を圏とする。
f:X → Y
g:X → Y
を C における射とする。

余積(過去スレ017の867) X＋Y が存在するとする。

(f, 1_Y)：X＋Y → Y
(g, 1_Y)：X＋Y → Y
を>>868で定義した射とする。

(f, 1_Y) と (g, 1_Y) のファイバー余積(過去スレ017の867)を P とする。

T を C の任意の対象とする。
過去スレ017の861より、
Hom(P, T) → Hom(Y, T)×Hom(Y, T) ⇒ Hom(X＋Y, T) は完全(過去スレ017の774)である。

標準同型：Hom(X＋Y, T) ⇔ Hom(X, T)×Hom(Y, T) が存在するから

Hom(P, T) → Hom(Y, T)×Hom(Y, T) ⇒ Hom(X, T)×Hom(Y, T) は完全(>>774)である。

よって、過去スレ017の818より、
Hom(P, T) → Hom(Y, T) ⇒ Hom(X, T) は完全(過去スレ017の774)である。

よって、過去スレ017の853より、
X ⇒ Y → P は完全(過去スレ017の870)である。
即ち P = Coker(f, g) である。