命題
有限積(過去スレ018の911)と有限交わりをもつ(>>185)圏は差核をもつ(>>161)。

証明
C を有限積と有限交わりをもつ圏とする。

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

<1_X, f>:X → X×Y
<1_X, g>:X → X×Y
を過去スレ018の872で定義した射とする。

p<1_X, f> = 1_X は単射であるから <1_X, f> も単射である。
同様に <1_X, g> も単射である。

よって、<1_X, f> と <1_X, g> の交わり (P, h) が存在する。
即ち、次の図式は引き戻し四角形(過去スレ017の866)である。

P  → X
↓   ↓<1_X, f>
X  → X×Y
<1_X, g>

>>189より P → X は f と g の差核である。
証明終