Partially Additive Categories

部分加法的圏（partially additive categories）の定義は気に入らないのだけど、とりあえず、"Types and Dynamics in Partially Additive Categories" (1995) by Gianfranco Mascari, Marco Pedicini（http://citeseer.ist.psu.edu/mascari95types.html）から引き写しておく。

---

まず、partially additive monoidの定義：

添字集合Iの族を(x_i:i∈I)という形で書くことにする。Iがたかだか可算のとき、可算族と呼ぶ。Mが集合だとして、M^★をMを値とする可算族の全体とする。今の用語法では、有限族も可算族に含まれる。また、M^★は普通の意味で集合にはならないが気にしないことにする。

部分写像Σ:M^★→Mが次の条件を満たすとき、summationと呼ぶことにする（summationは檜山が追加した用語）。Σの定義域に属する属をsummableと呼ぶ。

1. 結合性（associative）

(x_i:i∈I)が可算族で、(I_j:j∈J)がIの分割（partition）だとする。

(x_i:i∈I)がsummableである事と次の連言は同値。

1. 任意のj∈Jに対して、(x_i:i∈I_j)がsummable
2. (Σ(x_i:i∈I_j) : j∈J)がsummable

さらに、次の等式が成立する。

• Σ(x_i:i∈I) = Σ(Σ(x_i:i∈I_j) : j∈J)

2. 単元総和可能性（singleton smmability）

I = {a}のとき、Σ(x_i:i∈I) = x_a

3. 連続性

連続性は檜山の用語、もとはlimit sums。

次は同値。

1. (x_i:i∈I)がsummable
2. 任意の有限なF⊆I に対して(x_i:i∈F)がsummable

FとI＼Fという分割を使えば、有限なF⊆Iに対するsummableは出るから、同値ではなくて片方向含意でもよい。

---

次は、partially preadditive categoryの定義：

圏Cのhomsetがparitially additive monoidになっていて、圏の結合が総和Σに対して分配的なときに、その圏はpartially preadditive。詳しくは：

1. (f_i:i∈I)がa→bの射の可算族でsummableならば、任意のg:x→a, h:b→yに対して、Σ(g;f_i:i∈I) とΣ(f_i;h:i∈I) はsummabl。
2. g;(Σ(f_i:i∈I)) = Σ(g;f_i:i∈I)
3. (Σ(f_i:i∈I));h = Σ(f_i;h:i∈I)

---

やっと、partially additive categoryの定義、フーッ：

事前に零（zero）射と疑似射影の定義が要る。

• 特定された射の族 0_a,b:a→b が零射の族だとは、f;0 = 0;g = 0 が成立すること。partially preadditive categoryには零射の族がΣ(空)により定義できる。
• 零射の族を持ち、和（余積）を持つ圏において、J⊆Iのとき疑似射影（quasi-projection）π^I_Jは次のように定義される； π^I_J : (a_i:i∈I)の和→(a_i: i∈J)の和で、in_i;π^I_J = if i∈J then in_i else 0。

まず、圏Cは可算余積を持つ。そして、partially preadditive。さらに次の2つの条件を満たすときにpartially additive。

1. 互換和（Compatible Sum）公理：f_i∈Hom(a, b)であり、f:a→(bのi∈I分のコピーの和）で f;π_i = f_iとなるfがあるなら、族(f_i:i∈I)はsummable。
2. アンタイ（Untying）公理：f, g:a→bで{f, b}がsummableのとき、{f;in₁, g;in₂}:a→b+b はsummableである。