分裂する短完全列

補題 2.1（「Ext と拡大」§2）・ ✓公理まで証明済み

$0 \to A \xrightarrow{i} E \xrightarrow{p} C \to 0$ を $\mathcal A$ の短完全列とする。

次は同値である。(a) $ri = 1_A$ を満たす $r\colon E \to A$ がある。(b) $ps = 1_C$ を満たす $s\colon C \to E$ がある。(c) 射 $r, s$ があって $(E, i, s, r, p)$ は $A, C$ の双積である（すなわち $ri = 1_A$ 、 $ps = 1_C$ 、 $rs = 0$ 、 $pi = 0$ 、 $ir + sp = 1_E$ ）。
(c) のとき、 $\varphi = i\pi_1 + s\pi_2\colon A \oplus C \to E$ は同型で、 $\varphi\iota_1 = i$ 、 $p\varphi = \pi_2$ を満たす。
$F\colon \mathcal A \to \mathcal B$ がアーベル圏の間の加法関手で、上の列が (a)〜(c) を満たすなら、 $0 \to FA \xrightarrow{Fi} FE \xrightarrow{Fp} FC \to 0$ は短完全列で、やはり (a)〜(c) を満たす。

(a)〜(c) を満たす短完全列を分裂するという。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 8 件、定義なども含めて 9 件）。

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

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

双対圏もアーベル圏✓命題 4.2・加法圏とアーベル圏
- 核・余核・像・余像定義 2.1・加法圏とアーベル圏
完全性の判定✓補題 5.2・加法圏とアーベル圏
- 像分解✓定理 4.4・加法圏とアーベル圏
  - 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
  - アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏（上で展開済み）
- アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏
  - 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
  - 双対圏もアーベル圏✓命題 4.2・加法圏とアーベル圏（上で展開済み）
- 双対圏もアーベル圏✓命題 4.2・加法圏とアーベル圏（上で展開済み）
- 加群の圏はアーベル圏✓命題 4.6・加法圏とアーベル圏
  - 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
  - 加群の準同型定理✓定理 2.3・加群と PID 上の構造定理
完全性の基本操作✓補題 2.1・導来関手と δ 関手
- 核と余核の基本性質✓補題 2.2・加法圏とアーベル圏
- 像分解✓定理 4.4・加法圏とアーベル圏（上で展開済み）
- アーベル圏の mono・epi と平衡性✓命題 4.3・加法圏とアーベル圏（上で展開済み）
- 完全性の判定✓補題 5.2・加法圏とアーベル圏（上で展開済み）