双積から加法は出る

行列の圏と行列レトラクタブルな圏 - 檜山正幸のキマイラ飼育記 メモ編より：

零対象と双積を持つ圏は、自動的に（必然的に）近加法構造を持つと思うが確認してない。おそらくは、「双積を持つ近加法圏」という定義は冗長だろう。

---

A×Bを直積、A+Bを直和、A※Bを双積とする。米（※）じゃなくて、×と+を重ねた記号があると意味的にピッタリだと思うが、まー、米でもいいや。

射影をπ¹_A,B, π²_A,B、入射をι¹_A,B, ι²_A,Bと書く。零射は0_A,B。

(A, B, A※B; π¹_A,B, π²_A,B, ι¹_A,B, ι²_A,B)が双積系であるとは、

• (A, B, A※B; π¹_A,B, π²_A,B)が直積系
• (A, B, A※B; ι¹_A,B, ι²_A,B)が直和系

になっていて、さらに次の等式が成立：[追記]ウワーッ、結合の順序が逆だ！！！ 以下、π;ι を ι;π の直して読んでね。[/追記]

1. π¹;ι¹ = 1_A
2. π¹;ι² = 0_A,B
3. π²;ι¹ = 0_B,A
4. π²;ι² = 1_B

これは、δ^i,j_A,B（i,j = 1 or 2）をそれなりに定義して、

• πⁱ_A,B;ι^j_A,B = δ^i,j_A,B

とも書ける。

双積を定義するには、前もって零対象0と零射0_A,Bの存在が必須なので、双積を持つ圏（category with biproducts）は必然的に零を持つ圏（category with zero）である。

さて、双積を持つ圏では次が成立する。f:A→P, g:B→Qとして；

• <π¹;f, π²;g> = [f;ι¹, g;ι²] : A※B→P※Q

これを確認するには、<π¹;f, π²;g>;πⁱ と [f;ι¹, g;ι²];πⁱ を比較すればいい。実際にπ¹でやってみると：

• π_A,B¹;f = [f, 0_B,Q] : A※B→P

という等式が必要になるのだが、それは次の2つの等式から出る。

1. ι¹;π¹;f = ι¹;[f, 0_B,Q]
2. ι²;π¹;f = ι²;[f, 0_B,Q]

双積の定義 πⁱ;ι^j = δ^i,j からすぐにわかる。

それで、

• f※g = <π¹;f, π²;g> = [f;ι¹, g;ι²] : A※B→P※Q

と定義して、当該の圏が※に関してモノイド圏になることが示せる。このモノイド積※と、前もって持っている直積構造／直和構造から、双積を持つ圏が（等式的）双デカルト圏であることがわかる。双デカルト圏には、対角Δと余対角∇から近加法的構造（nearly additive structure）が入るから、双積を持つなら自動的・必然的に近加法的であることになる。

やっぱりね。

実はまだ、双積を持つ近加法圏の加法（事前に定義されている）が、双積から誘導された（induced）加法かどうかはわからない。双積と協調する加法がイッパイあるとは思えないが、確認してはいない。