フィルター余極限と有限極限の交換

定理 6.4（「極限と余極限」§6）・ ✓公理まで証明済み

$I$ をフィルター圏、 $J$ を有限圏、 $F : I \times J \to \mathsf{Set}$ を双関手とする。標準写像

\kappa : \operatorname*{colim}_{i} \lim_{j} F(i, j) \longrightarrow \lim_{j} \operatorname*{colim}_{i} F(i, j), \qquad [i, (x_j)_j] \mapsto ([i, x_j])_j

は全単射である。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

Hom は極限を保つ✓命題 5.2・極限と余極限
- 積と等化子から極限✓定理 3.1・極限と余極限
- 具体的な圏の完備性と余完備性✓定理 4.1・極限と余極限
  - 積と等化子から極限✓定理 3.1・極限と余極限
  - 宇宙の閉性✓命題 2.3・圏・関手・自然変換
    Grothendieck 宇宙定義 2.1・圏・関手・自然変換
    順序対（クラトフスキー）定義 2.3・公理的集合論 ZFC
  - 商集合の普遍性✓定理 5.1・関係と同値関係
    同値類の基本性質✓補題 4.2・関係と同値関係この先をたどる →
  - 直和・直積・自由加群・有限生成・有限表示定義 2.2・加群・完全列・中山の補題
  - 部分加群・剰余加群・準同型定義 2.1・加群・完全列・中山の補題
  - 積位相の普遍性✓定理 3.4・積位相・商位相と Tychonoff の定理
    生成される位相の性質✓補題 2.2・積位相・商位相と Tychonoff の定理
  - 始位相・終位相の普遍性✓定理 2.4・積位相・商位相と Tychonoff の定理
    生成される位相の性質✓補題 2.2・積位相・商位相と Tychonoff の定理
    積空間と積位相定義 3.1・積位相・商位相と Tychonoff の定理
    商位相・商写像定義 4.1・積位相・商位相と Tychonoff の定理
    直和位相定義 4.6・積位相・商位相と Tychonoff の定理
  - 直和位相の普遍性✓命題 4.7・積位相・商位相と Tychonoff の定理
  - 商位相の普遍性✓定理 4.2・積位相・商位相と Tychonoff の定理
- 極限の一意性と関手性✓命題 2.3・極限と余極限
  - 表現対象の一意性✓系 4.3・米田の補題と表現可能関手
  - パラメータ付きの表現可能性✓命題 5.1・米田の補題と表現可能関手
    選択公理公理 3.1・選択公理と Zorn の補題
    双関手の判定✓補題 4.3・圏・関手・自然変換
    表現と普遍元✓命題 4.2・米田の補題と表現可能関手この先をたどる →
    米田の補題✓定理 3.1・米田の補題と表現可能関手
    米田の原理✓系 3.4・米田の補題と表現可能関手この先をたどる →
- 極限・余極限・完備定義 2.2・極限と余極限
集合のフィルター余極限の記述✓命題 6.3・極限と余極限
- フィルター圏の有限な条件✓補題 6.2・極限と余極限
フィルター圏の有限な条件✓補題 6.2・極限と余極限

これを使っている定理

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

フィルター余極限と有限極限の交換

閉包の状態

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

これを使っている定理

関連するノック 2 問

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