双積と加法の関係 -- だいたいわかった

加法から双積は出るのか？ - 檜山正幸のキマイラ飼育記 メモ編と双積と加法の関係 -- まだわかってない - 檜山正幸のキマイラ飼育記 メモ編の話。

発端は：

• 半加法圏 ： 零対象と双積を持つAbMon圏（by 檜山）

この定義が冗長だろう、ということ。双積を持てば加法は一意的に定義されるだろう、ということ。

双積から加法の定義は、f + g := Δ;(f※g);∇ となる。だから、半加法圏のなかで成立する等式として f + g = Δ;(f※g);∇ が示せればOK。

f + g = Δ;(f※g);∇ は普通の線形代数でも示せるのだから、半加法圏で線形代数をやって、この等式を示せばいいことになる。例えば、準備として次のような等式を示したい。

• <f, f'> + <g, g'> = <f + f', g + g'>
• <f, 0> + <0, g> = <f, g>
• <f, g>;[1, 1] = f + g