前加法圏

定義 3.1（「加法圏とアーベル圏」§3）

圏 $\mathcal C$ が前加法圏であるとは、各 $\operatorname{Hom}(X, Y)$ にアーベル群の構造が与えられ、合成

\operatorname{Hom}(Y, Z) \times \operatorname{Hom}(X, Y) \to \operatorname{Hom}(X, Z),\quad (g, f) \mapsto gf

が双線形であることをいう。すなわち $g(f_1 + f_2) = gf_1 + gf_2$ 、 $(g_1 + g_2)f = g_1f + g_2f$ が成り立つ。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明で明示的に参照している定理は、まだありません。