数学の基礎

米田の補題

一つの対象は、圏の他のあらゆる場所からそこへ向かうすべての矢印のパターンによって、同型を除いて完全に決定される——米田の補題はその観察を精密な全単射に変え、埋め込み $A\mapsto\mathrm{Hom}(-,A)$ が充満忠実であるという系こそが、「対象をその写像によって研究する」ことをスローガンではなく厳密な方法にする唯一の事実である。

直観対象とはそれがすることである

電子部品を完全に知るために、その内部を見る必要はない——考えられるすべての周辺回路について、その部品がどのように配線され得るかを正確に知っていれば十分である。圏においても類似の事実が成り立つ:対象 $A$ は、あらゆる対象 $X$ について $\mathrm{Hom}(X,A)$ —— $A$ に向かう写像の集合——を一挙に知ることによって、同型を除いて完全に決定される。

あらゆる対象

X

からあらゆる矢印を

A

へ、一挙に集めたもの——それが前層

h_A

が記録するデータである。

大学表現可能な前層

定義: 前層 $h_A$

$\mathcal{C}$ の対象 $A$ に対し、表現可能な前層 $h_A=\mathrm{Hom}_{\mathcal{C}}(-,A)$ は各対象 $X$ に集合 $h_A(X)=\mathrm{Hom}_{\mathcal{C}}(X,A)$ を割り当て、各射 $g:X\to Y$ に前合成写像 $h_A(g):\mathrm{Hom}(Y,A)\to\mathrm{Hom}(X,A),\quad f\mapsto f\circ g$ を割り当てる。これにより $h_A$ は関手 $\mathcal{C}^{\mathrm{op}}\to\mathbf{Set}$ となる—— $g$ を右から合成することが割り当ての向きを逆にするため、反変である。

h_A(X) = \mathrm{Hom}_{\mathcal{C}}(X,A)

任意の関手 $F:\mathcal{C}^{\mathrm{op}}\to\mathbf{Set}$ に対し、米田の補題は $h_A$ から $F$ への自然変換が、単一の集合 $F(A)$ の元と全単射であると述べる: $\mathrm{Nat}(\mathrm{Hom}_{\mathcal{C}}(-,A),F)\cong F(A)$ 。この全単射は、逆方向に進む二つの写像 $\Phi$ と $\Psi$ から構成される。

\mathrm{Nat}(\mathrm{Hom}_{\mathcal{C}}(-,A), F) \cong F(A)

米田全単射の二つの方向
写像	方向	公式
$\Phi$	$\mathrm{Nat}(h_A,F)\to F(A)$	$\Phi(\eta)=\eta_A(1_A)$
$\Psi$	$F(A)\to\mathrm{Nat}(h_A,F)$	$\Psi(x)_X(f)=F(f)(x)$

発展全単射、段階的な証明

$\Phi$ は自然変換 $\eta:h_A\Rightarrow F$ を、可能な限り経済的な入力——単位射 $1_A\in h_A(A)=\mathrm{Hom}(A,A)$ ——で評価し、 $F(A)$ の元 $\eta_A(1_A)$ を生み出す。逆方向では、 $\Psi$ は元 $x\in F(A)$ から出発し、すべての対象 $X$ とすべての $f\in\mathrm{Hom}(X,A)$ について、 $x$ を $F(f)$ に沿って前へ押し出すことで $F(X)$ の元を再構成する: $\Psi(x)_X(f)=F(f)(x)$ 。 $\eta$ の自然性こそが $\Psi(\Phi(\eta))$ が $\eta$ を復元することを可能にする理由であり、これが次の定理で完全に証明される。

\Phi(\eta) = \eta_A(1_A)

\Psi(x)_X(f) = F(f)(x)

定理: 米田の補題

任意の関手 $F:\mathcal{C}^{\mathrm{op}}\to\mathbf{Set}$ と対象 $A$ について、上の写像 $\Phi$ と $\Psi$ は互いに逆であり、したがって $\mathrm{Nat}(\mathrm{Hom}_{\mathcal{C}}(-,A),F)\cong F(A)$ は集合の真の全単射である。

なぜ正しいのか?

これによって圏論の研究者は、無限で捉えにくい自然変換の族を、 $F(A)$ の単一の具体的な元と交換できるようになる——表現可能な前層 $h_A$ から出る写像に関するすべての問いが、一つの集合に関する問いに帰着する。

証明

まず、すべての $x\in F(A)$ について $\Phi(\Psi(x))=x$ を確認する。定義を展開する: $\Psi$ の公式を $X=A$ 、 $f=1_A$ に特殊化すると $\Psi(x)_A(1_A)=F(1_A)(x)$ 。 $F$ は関手であるから、単位射 $1_A$ を $F(A)$ 上の恒等関数に送るので、 $F(1_A)(x)=x$ 。よって $\Phi(\Psi(x))=\Psi(x)_A(1_A)=x$ となり、求める通りである——この方向は関手の単位律しか使わない。

次に、より難しい方向、すべての自然変換 $\eta:h_A\Rightarrow F$ について $\Psi(\Phi(\eta))=\eta$ を確認する。両辺は自然変換 $h_A\Rightarrow F$ であるから、すべての対象 $X$ とすべての元 $f\in h_A(X)=\mathrm{Hom}(X,A)$ で成分が一致することを示せば十分である。

$x:=\Phi(\eta)=\eta_A(1_A)$ を用いて $\Psi$ の公式で $\Psi(\Phi(\eta))_X(f)$ を展開すると、これは $F(f)(\eta_A(1_A))$ に等しい。

次に $\eta$ 自身の自然性を、 $\eta_Y(f\circ g)=F(g)(\eta_X(f))$ の形で、 $g:=f:X\to A$ 、もう一方の変数を $A$ として用いる:その自然性四角形で $f:=1_A\in h_A(A)$ とすると、まさに $\eta_X(1_A\circ f)=F(f)(\eta_A(1_A))$ 、すなわち $1_A\circ f=f$ であるから $\eta_X(f)=F(f)(\eta_A(1_A))$ が得られる。

最後の二つの式を組み合わせると: $\Psi(\Phi(\eta))_X(f)=F(f)(\eta_A(1_A))=\eta_X(f)$ 。 $X$ と $f$ が任意であったため、二つの自然変換はどこでも一致し、 $\Psi(\Phi(\eta))=\eta$ となる。最初の段落と合わせて、 $\Phi$ と $\Psi$ は互いに逆な全単射である。

定理: 米田埋め込みは充満忠実である

米田埋め込み $y:\mathcal{C}\hookrightarrow[\mathcal{C}^{\mathrm{op}},\mathbf{Set}]$ 、 $y(A)=h_A$ は充満忠実である:すべての $A,B\in\mathcal{C}$ について $\mathrm{Nat}(h_A,h_B)\cong\mathrm{Hom}_{\mathcal{C}}(A,B)$ であり、この全単射は射 $f:A\to B$ を、 $f$ による後合成で与えられる自然変換 $h_A\Rightarrow h_B$ に送る。

なぜ正しいのか?

充満忠実性とは、翻訳 $A\mapsto h_A$ が情報を一切失わないという保証そのものである: $\mathcal{C}$ の異なる射は異なる自然変換になり、二つの表現可能な前層の間のすべての自然変換は $\mathcal{C}$ の実際の射から来る。これが対象をそこへの写像だけを通じて研究することを正当化する。

証明

目標関手を $F:=h_B$ として米田の補題を適用する。補題は全単射 $\mathrm{Nat}(h_A,h_B)\cong h_B(A)$ を与え、定義 $h_B(A)=\mathrm{Hom}_{\mathcal{C}}(A,B)$ を展開すると、まさに $\mathrm{Nat}(h_A,h_B)\cong\mathrm{Hom}_{\mathcal{C}}(A,B)$ が得られる。

残るは、この全単射のもとで自然変換 $\eta:h_A\Rightarrow h_B$ がどの $\mathcal{C}$ の射に対応するかを特定し、それが後合成であることを確認することである。 $\Phi$ の公式により、 $\eta$ は元 $\Phi(\eta)=\eta_A(1_A)\in\mathrm{Hom}(A,B)$ に対応する;この射を $f$ と呼ぶ。

次に $\Psi(\Phi(\eta))=\eta$ (上の定理を $F=h_B$ に適用したもの)を使って、 $\eta$ のすべての成分を $f$ から復元する:任意の対象 $X$ と任意の $g\in h_A(X)=\mathrm{Hom}(X,A)$ について、 $\Psi(f)_X(g)=h_B(g)(f)$ 。 $h_B$ の射への反変作用——前合成——を展開すると $h_B(g)(f)=f\circ g$ が得られる。よって $\eta_X(g)=f\circ g$ : $\eta$ のすべての成分は文字通り $f$ による後合成である。

$\Phi$ と $\Psi$ が互いに逆な全単射である(上で証明済み)こと、そして $f$ による後合成がまさに $\Psi(f)$ であることから、 $f$ を $f$ による後合成に送る割り当ては自体が全単射 $\mathrm{Hom}(A,B)\to\mathrm{Nat}(h_A,h_B)$ である——これがまさに $y$ が充満忠実であるという主張である。

大学応用:モジュライ空間と継続渡しスタイル

代数幾何学において、ある種の幾何学的対象(曲線、ベクトル束、……)のモジュライ空間は、まずテスト対象 $X$ をその幾何構造の $X$ 上の族の集合に送る関手 $F$ を書き下すことによって定義される;モジュライ空間は、存在するならば、 $F$ を表現する対象 $M$ 、すなわち $F\cong h_M$ である。米田埋め込みが充満忠実であることこそが、そのような $M$ が存在するとき一意な同型を除いて一意である理由である——Grothendieckの「点の関手」哲学は、すべてのスキームをその表現可能な前層に他ならないものとして扱う。関数型プログラミングでは、継続渡しスタイル関数の型 $\forall r.\ (a\to r)\to r$ は、その構成により、共変Hom関手 $\mathrm{Hom}(a,-)$ から恒等関手への自然変換の型である;(共変、双対の)米田の補題はまさに $\forall r.\ (a\to r)\to r \\cong\ a$ と述べ、CPS変換された値が通常の値を再パッケージしたものに他ならないという日常的な事実と一致する。

例: 二対象の圏で全単射を検証する

$\mathcal{C}$ が二つの対象 $0,1$ 、単位射、そして一つの非単位射 $\iota:0\to1$ を持つとする。 $A=1$ 、 $F=h_1$ 自身とする。この $F$ について $\mathrm{Nat}(\mathrm{Hom}_{\mathcal{C}}(-,A),F)\cong F(A)$ が成り立つこと、すなわち $\mathrm{Nat}(h_1,h_1)$ が $h_1(1)=\mathrm{Hom}(1,1)$ と同じ個数の元を持つことを、直接の列挙により検証せよ。

解答

まず $h_1$ を明示的に計算する: $h_1(0)=\mathrm{Hom}(0,1)=\{\iota\}$ (一元)、 $h_1(1)=\mathrm{Hom}(1,1)=\{1_1\}$ (一元、 $\mathcal{C}$ には $1$ から $1$ へ終わる他の射がないため)。よって $F(A)=h_1(1)$ はちょうど一元 $1_1$ を持つ。

米田の補題により、 $\mathrm{Nat}(h_1,h_1)$ もちょうど一元を持つはずである。これを直接確認する:自然変換 $\eta:h_1\Rightarrow h_1$ には成分 $\eta_0:\{\iota\}\to\{\iota\}$ と $\eta_1:\{1_1\}\to\{1_1\}$ が必要である。これらの集合はそれぞれ一元しか持たないため、各対象で可能な関数はちょうど一つ——恒等関数——であり、全体としてちょうど一つの候補 $\eta$ が得られる。

この候補が自然性を満たすことをなお確認する必要がある(ここでは自動的に満たされる。自然性四角形は $\eta_0(\iota)=\eta_0(1_1\circ\iota)=h_1(\iota)(\eta_1(1_1))=h_1(\iota)(1_1)=1_1\circ\iota=\iota$ を強制するが、どのみち利用可能な値が一つしかないため成り立つ)。

よって $\mathrm{Nat}(h_1,h_1)=\{\mathrm{id}_{h_1}\}$ はちょうど一元を持ち、 $F(A)=\{1_1\}$ がちょうど一元を持つことと一致する——全単射 $\mathrm{Nat}(\mathrm{Hom}_{\mathcal{C}}(-,A),F)\cong F(A)$ が具体的に成り立ち、 $\Phi(\mathrm{id}_{h_1})=(\mathrm{id}_{h_1})_1(1_1)=1_1$ が単一の元を直接復元する。

例: 米田としての継続渡しスタイル

関数型言語において、型 $\forall r.\ (a\to r)\to r$ の値とは、 $a$ を消費する任意の方法(関数 $a\to r$ )が与えられたとき $r$ を生成する関数 $k$ である。 $k$ が型 $a$ の通常の値によって完全に決定され、それを復元できることを示せ。

解答

$\mathcal{C}=\mathbf{Set}$ (あるいは型と関数の圏)と同一視し、対象 $a$ を固定し、 $F=\mathrm{Id}$ を恒等関手とする。値 $k:\forall r.\ (a\to r)\to r$ は、定義により、すべての型 $r$ に対する関数 $k_r:(a\to r)\to r$ の選択である——これはまさに共変関手 $\mathrm{Hom}(a,-)$ から $\mathrm{Id}$ への自然変換である(ここでの自然性は、「すべての $r$ について」が強制するパラメトリシティそのものである)。

(共変、双対の)米田の補題から $\Phi$ を適用する: $\Phi(k)=k(\mathrm{id}_a)$ は $k$ を $r:=a$ で、恒等関数 $\mathrm{id}_a:a\to a$ に対して評価し、型 $a$ の通常の値を生成する。これが「継続が値を決定する」方向である。

逆方向に $\Psi$ を適用する:値 $n:a$ が与えられたとき、すべての $r$ とすべての $g:a\to r$ について $\Psi(n)_r(g)=g(n)$ と定義する——つまり $\Psi(n)_r(g)=g(n)$ 、値の標準的なCPS変換である:「任意の消費者 $g$ が与えられたとき、 $n$ をそれに渡す継続」。

$F=\mathrm{Id}$ に適用した米田の補題により、これら二つの構成は互いに逆である: $\Phi(\Psi(n))=\Psi(n)_a(\mathrm{id}_a)=\mathrm{id}_a(n)=n$ が値を復元し、 $\Psi(\Phi(k))=k$ は上の定理の自然性の議論を $F=\mathrm{Id}$ に特殊化したものから従う。よって $\forall r.\ (a\to r)\to r \\cong\ a$ が成り立ち、継続渡しスタイルの値が通常の値の情報をちょうど、それ以上でもそれ以下でもなく運ぶことが確認される。

研究の最前線 2026年時点

米田の補題は今なお一般化され続けている:Jacob Lurieの∞圏的米田の補題(Higher Topos Theory, 2009)は、全単射を空間のホモトピー同値に格上げする。これは、自然変換の「等しさ」自体がより高次の構造を持つことを許すとき正しい主張である。ホモトピー型理論は、単価性公理を通じて、型理論の内部で同じ事実を再定式化する。応用面では、関数型プログラミングの「プロ関手光学」が米田風の埋め込みを用いて、合成可能なgetter/setterを自然変換として表現しており、2020年代のLeanのmathlibにおける圏論の形式化の努力は、米田の補題自体(とその∞圏的な仲間)を、形式化ライブラリの標準的な機械検証済みベンチマークの一つにし、この補題とそれを検証するために使われる証明支援系との歴史的な輪をさらに引き締めている。

$\Phi$ は自然変換 $\eta:h_A\Rightarrow F$ に対して何をするか?

$\Psi(\Phi(\eta))=\eta$ における一意性のステップは $\eta$ のどの性質に依るか?

継続渡しスタイルにおいて、型 $\forall r.\ (a\to r)\to r$ はどの型と自然に同型か?

米田埋め込みが充満忠実であることから、モジュライ関手 $F$ を表現する対象 $M$ について何が結論できるか?

参考文献

Saunders Mac Lane (1998). Categories for the Working Mathematician
Emily Riehl (2016). Category Theory in Context
Jacob Lurie (2009). Higher Topos Theory · arXiv:math/0608040