既約ルート系の分類

定理 7.7（「ルート系と Weyl 群」§7）・ ✓公理まで証明済み

既約ルート系の Dynkin 図は、次のいずれかである（添字は頂点の数）。

$A_\ell\ (\ell\ge1)$ ： $\ell$ 個の頂点が単線で一列につながった鎖。
$B_\ell\ (\ell\ge2)$ 、 $C_\ell\ (\ell\ge3)$ ： $\ell$ 個の頂点の鎖で、最後の 1 組だけが二重線のもの。 $B_\ell$ は矢印が端の頂点を向き（端が短いルート）、 $C_\ell$ は端の頂点から出る（端が長いルート）。
$D_\ell\ (\ell\ge4)$ ： $\ell-2$ 個の頂点の単線の鎖の一端に、2 つの頂点をそれぞれ単線で結んだもの。
$E_6$ 、 $E_7$ 、 $E_8$ ：分岐点が 1 つで、そこから単線の腕が 3 本出て、腕の頂点数（分岐点を除く）が $(1,2,2)$ 、 $(1,2,3)$ 、 $(1,2,4)$ のもの。
$F_4$ ：4 頂点の鎖で、中央の組が二重線、両端の組が単線のもの。
$G_2$ ：2 頂点を三重線で結んだもの。

逆に、これらの各図に対して、それを Dynkin 図とする既約ルート系が存在し、それは $\Phi$ を $\Phi'$ に写す線形同型を除いてただ一つである。

閉包の状態

✓ 公理まで証明済み

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

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

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

既約性と Dynkin 図の連結性✓補題 7.3・ルート系と Weyl 群
- Weyl 群の基本定理✓定理 6.2・ルート系と Weyl 群
  - 単純鏡映は他の正ルートを置換する✓補題 5.3・ルート系と Weyl 群
  - 削除条件✓補題 6.1・ルート系と Weyl 群
    単純鏡映は他の正ルートを置換する✓補題 5.3・ルート系と Weyl 群
許容系のグラフの制約✓補題 7.5・ルート系と Weyl 群
ルート系定義 4.1・ルート系と Weyl 群
基底（単純ルート）定義 5.1・ルート系と Weyl 群
基底の部分集合が定めるルート系✓補題 7.6・ルート系と Weyl 群
- ルート系定義 4.1・ルート系と Weyl 群
Cartan 行列はルート系を決める✓命題 7.1・ルート系と Weyl 群
- Weyl 群の基本定理✓定理 6.2・ルート系と Weyl 群（上で展開済み）

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