極限どうしの交換

命題 5.3（「極限と余極限」§5）・ ✓公理まで証明済み

$I, J$ を小さい圏、 $F : I \times J \to \mathcal{C}$ を双関手とし、各 $i$ について $F(i, -)$ の極限 $(L_i, \lambda^{i})$ があるとする。命題 2.3 により $i \mapsto L_i$ は関手 $L : I \to \mathcal{C}$ になる。 $L$ の極限 $(M, \mu)$ があるなら、 $(M, (\lambda^{i}_j \circ \mu_i)_{(i, j)})$ は $F$ の極限である。したがって、関係する極限がすべて存在するとき

\lim_{i} \lim_{j} F(i, j) \;\cong\; \lim_{(i, j)} F(i, j) \;\cong\; \lim_{j} \lim_{i} F(i, j)

である。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

極限の一意性と関手性✓命題 2.3・極限と余極限
- 表現対象の一意性✓系 4.3・米田の補題と表現可能関手
- パラメータ付きの表現可能性✓命題 5.1・米田の補題と表現可能関手
  - 選択公理公理 3.1・選択公理と Zorn の補題
  - 双関手の判定✓補題 4.3・圏・関手・自然変換
  - 表現と普遍元✓命題 4.2・米田の補題と表現可能関手（上で展開済み）
  - 米田の補題✓定理 3.1・米田の補題と表現可能関手
  - 米田の原理✓系 3.4・米田の補題と表現可能関手
    米田埋め込み✓系 3.3・米田の補題と表現可能関手この先をたどる →
    充満忠実な関手は同型を反映する✓補題 4.6・圏・関手・自然変換
表現と普遍元✓命題 4.2・米田の補題と表現可能関手
- 自然同型は成分ごとの同型✓命題 5.2・圏・関手・自然変換
- 米田の補題✓定理 3.1・米田の補題と表現可能関手

これを使っている定理

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

極限どうしの交換

閉包の状態

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

これを使っている定理

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