双積と加法の関係 -- よくわかった

半加法圏では次が成立する。

1. <f, g>;[1, 1] = f + g
2. <1, 1>;[f, g] = f + g
3. <1, 1>;(f※g);[1, 1] = f + g

f※gの定義（<π¹;f, π²;g> = [f;ι¹, g;ι²]）から、

1. <f, g>;[1, 1] = <1, 1>;f※g;[1, 1] （<f, g> = <1, 1>;f※g）
2. <1, 1>;[f, g] = <1, 1>;f※g;[1, 1] （[f, g] = f※g;[1, 1]）

がすぐ出るので、どれか1つを示せばよい。<f, g>;[1, 1] = f + g を示すことにして、次のように計算する（説明は下）。画像だけ

考えるときは上から下へと考えたが、論理の流れは下から上。

一番下の命題は、零とのペアリング、コペアリングは結合で書ける、ということ。零が相手ならペアリングしても実質的にはペアになってないこと。成分（余成分）ごとに等式を示せばよい。双積の直交性が効いている。

その他は別に問題ないだろう。線形代数の基本的な計算を使っている。

1. 縦ベクトルの足し算：<f, f'> + <g, g'> = <f + g, f' + g'>
2. 横ベクトルの足し算：[f, f']+ [g, g'] = [f + g, f' + g']
3. ベクトルの分解：<f, g> = <f, 0> + <0, g>

ここでは使ってないが、

1. <f, 0> = f;<1, 0>
2. [f, 0] = [1, 0];f

なども重宝する。

---

この程度の計算でも動悸息切れがする。ハァーー。それにしても、計算はまったく体力だな。