補題
F：C → D を関手とする。
任意の M ∈ D に対して (M↓F) (過去スレ017の571) から D への関手 P を
P(M → F(X)) = X により定義する。

このとき、F が差核を保存(>>257)すれば P は差核を生成(>>349)する。

証明
P は忠実(過去スレ017の403)かつ準忘却(過去スレ018の35)であり同型を反映(>>347)する。
よって、>>351より P が差核を持ち上げる(>>321)ことを証明すればよい。

u：M → F(X) と v：M → F(Y) を (M↓F) の対象とし、
f：u → v と g：u → v を (M↓F) における射とする。
ここで、f：X → Y、g：X → Y であり、F(f)u = v、F(g)u = v である。

h：K → X を f と g の差核とする。
F は差核を保存するから F(h)：F(K) → F(X) は F(f) と F(g) の差核である。
F(f)u = F(g)u であるから w：M → F(K) で F(h)w = u となるものが一意に存在する。

h：w → u が f：u → v と g：u → v の差核であることは図を描いてみれば分かる。
ここにその図を描くのは面倒なので省略する。
証明終