有限積はモノイダル構造を与える

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

圏 $\mathcal{C}$ が終対象 $1$ と任意の 2 対象の積をもつとし、積 $X \times Y$ と射影を選んでおく。 $X \otimes Y = X \times Y$ 、 $f \otimes g = f \times g$ （ $f : X \to X'$ 、 $g : Y \to Y'$ について $p_{X'}(f \times g) = f p_X$ 、 $p_{Y'}(f \times g) = g p_Y$ で定まる射）、 $I = 1$ とし、 $a$ 、 $l$ 、 $r$ 、 $c$ を「射影との合成が対応する射影になる」ただ一つの射とすると、 $\mathcal{C}$ は対称モノイダル圏になる。これをデカルト・モノイダル構造という。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

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

これを使っている定理

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

有限積はモノイダル構造を与える

閉包の状態

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

これを使っている定理

関連するノック 1 問

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