作用のモナドの代数は G 集合

命題 2.13（「モナドとモノイダル圏」§2）・ ✓公理まで証明済み

$G$ を小さい群とし、 $TX = G \times X$ 、 $T(f) = \mathrm{id}_G \times f$ 、 $\eta_X(x) = (e, x)$ 、 $\mu_X(g, (h, x)) = (gh, x)$ とする。

$(T, \mu, \eta)$ は $\mathsf{Set}$ 上のモナドである。
$T$ 代数 $(X, a)$ は、 $g \cdot x = a(g, x)$ によって $X$ への $G$ の（左）作用（定義 2.1［群の作用と Sylow の定理］）と 1 対 1 に対応し、代数の射は同変写像 $f(g \cdot x) = g \cdot f(x)$ と一致する。とくに $G$ 集合の圏は $\mathsf{Set}^{T}$ と同型である。
$G$ 集合の忘却関手はモナド的で、左随伴は $X \mapsto G \times X$ （ $G$ は左の成分に掛け算で作用する）である。

閉包の状態

✓ 公理まで証明済み

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

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

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

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