代数の圏と同型ならモナド的

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

$(T, \mu, \eta)$ を $\mathcal{C}$ 上のモナド、 $G : \mathcal{D} \to \mathcal{C}$ を関手とし、圏の同型 $\Phi : \mathcal{D} \to \mathcal{C}^{T}$ （逆関手 $\Phi^{-1}$ をもつ関手）で $U^{T}\Phi = G$ を満たすものがあるとする。このとき $F = \Phi^{-1}F^{T}$ は $G$ の左随伴で、随伴 $F \dashv G$ のモナドは $(T, \mu, \eta)$ 、比較関手は $\Phi$ である。とくに $G$ はモナド的である。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

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

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

前提をたどる証明が使う定理・定義（直接 2 件）

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

Eilenberg–Moore の随伴✓定理 2.5・モナドとモノイダル圏
- 普遍射の族から随伴✓定理 2.7・随伴関手と随伴関手定理
  - 選択公理公理 3.1・選択公理と Zorn の補題
  - 随伴の三つの定義の同値✓定理 2.3・随伴関手と随伴関手定理
  - パラメータ付きの表現可能性✓命題 5.1・米田の補題と表現可能関手
    選択公理公理 3.1・選択公理と Zorn の補題
    双関手の判定✓補題 4.3・圏・関手・自然変換
    表現と普遍元✓命題 4.2・米田の補題と表現可能関手この先をたどる →
    米田の補題✓定理 3.1・米田の補題と表現可能関手
    米田の原理✓系 3.4・米田の補題と表現可能関手この先をたどる →
- 随伴の三つの定義の同値✓定理 2.3・随伴関手と随伴関手定理
比較関手✓定理 2.8・モナドとモノイダル圏
- 随伴の三つの定義の同値✓定理 2.3・随伴関手と随伴関手定理

これを使っている定理証明で参照している 2 件

リストモナドの代数はモノイド✓命題 2.12・モナドとモノイダル圏
作用のモナドの代数は G 集合✓命題 2.13・モナドとモノイダル圏

代数の圏と同型ならモナド的

閉包の状態

前提をたどる 証明が使う定理・定義（直接 2 件）

これを使っている定理 証明で参照している 2 件

前提をたどる証明が使う定理・定義（直接 2 件）

これを使っている定理証明で参照している 2 件