米田原理とシーケント計算

エミリー・リエル〈Emily Riehl〉の講義動画の最初のほう（10分くらい）で、ベクトル空間の分配法則の圏論的証明が紹介されています。これは、証明原理としての米田の補題／米田埋め込みとシーケント計算の関連性を示唆していて、なかなか興味深いですね。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\DA}{\downarrow}
\newcommand{\An}[1]{\langle #1 \rangle} % Angular
\newcommand{\twoto}{\Rightarrow}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
%\newcommand{\u}[1]{\underline{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
\newcommand{\To}{\longrightarrow}
\newcommand{\VRule}{\downdownarrows}
`$

内容：

• 米田埋め込み
• 米田原理
• 線形代数
• シーケントと推論
• 米田原理を使う
• 分配法則の証明
• おわりに

米田埋め込み

圏 $`\cat{C}`$ の前層達の圏〈category of presheaves〉と余前層達の圏〈category of copresheaves〉を次のように書きます。

$`\quad \cat{C}^\wedge := \mrm{PSh}(\cat{C}) = [\cat{C}^\op, \mbf{Set}]\\
\quad \cat{C}^\vee := \mrm{CoPSh}(\cat{C}) = [\cat{C}, \mbf{Set}]
`$

米田埋め込み〈Yoneda embedding〉を $`よ^\wedge_\cat{C}`$ 、余米田埋め込み〈coYoneda embedding〉（反変の米田埋め込み）を $`よ^\vee_\cat{C}`$ と書きます。

$`\quad よ^\wedge_\cat{C} : \cat{C}\to \cat{C}^\wedge \In \mbf{CAT}\\
\quad よ^\vee_\cat{C} : \cat{C}^\op\to \cat{C}^\vee \In \mbf{CAT}
`$

下付きの $`\cat{C}`$ は、文脈から明らかなら省略します。

$`\quad よ^\wedge : \cat{C}\to \cat{C}^\wedge \In \mbf{CAT} \\
\quad よ^\vee : \cat{C}^\op \to \cat{C}^\vee \In \mbf{CAT}
`$

また、$`a\in |\cat{C}|`$ に対する米田埋め込みの値は次のように略記することがあります。

$`\quad よ^a := よ^\wedge_\cat{C}(a) = \cat{C}(\hyp, a)\\
\quad よ^\vee_a := よ^\vee_\cat{C}(a) = \cat{C}(a, \hyp)
`$

さらに次の略記も使います。

$`\quad \hat{a} := よ^a = よ^\wedge_\cat{C}(a)\\
\quad \check{a} := よ^\vee_a = よ^\vee_\cat{C}(a)
`$

以下の呼び名／記法はすべて同じです。

1. $`a`$ に対する米田埋め込みの値 $`よ^a = よ^\wedge_\cat{C}(a)`$
2. $`a`$ により表現可能〈representable〉な前層 $`\cat{C}(\hyp, a)`$
3. $`a`$-プレックス〈$`a`$-plex〉 $`\hat{a}`$

双対的に：

1. $`a`$ に対する余米田埋め込みの値 $`よ^\vee_a = よ^\vee_\cat{C}(a)`$
2. $`a`$ により余表現可能〈corepresentable〉な余前層 $`\cat{C}(a, \hyp)`$
3. $`a`$-コプレックス〈$`a`$-coplex〉 $`\check{a}`$

米田原理

米田埋め込み $`よ = よ^\wedge = よ_\cat{C}^\wedge`$ は、充満な埋め込みです。これは次を意味します。

• $`よ`$ は、対象集合上で単射な充満忠実な共変関手*1である。

余米田埋め込み $`よ^\vee`$ も充満な埋め込みです。

• $`よ^\vee`$ は、対象集合上で単射な充満忠実な反変関手*2である。

$`よ`$ と $`よ^\vee`$ が充満な埋め込み（ホムセットごとに同型）であることから、次が言えます。

• $`a, b\in |\cat{C}|`$ に対して、$`\hat{a}\cong \hat{b}`$ ならば $`a \cong b`$ 。
• $`a, b\in |\cat{C}|`$ に対して、$`\check{a}\cong \check{b}`$ ならば $`a \cong b`$ 。

2つの対象 $`a, b`$ の米田埋め込み／余米田埋め込み（の値）が $`\cat{C}^\wedge, \cat{C}^\vee`$ において同型ならば、それらの対象は同型です。このことは、対象の同型性の証明に使える原理なので、米田原理〈The Yoneda principle〉と呼びます*3。

線形代数

$`K`$ を体として、$`K`$ 上のベクトル空間達と線形写像達の圏を $`\mbf{Vect}_K`$ と書きます。$`K`$ は固定するので省略して、$`\mbf{Vect} = \mbf{Vect}_K`$ と略記します。

ベクトル空間の直和 $`V \oplus W`$ は、圏論的には双積〈biproduct〉といいます。圏論的積〈直積〉かつ圏論的余積〈直和〉であるからです。ここでは、双積を直和として解釈するので、$`\oplus`$ ではなくて $`+`$ で書きます。

$`V\otimes W`$ はベクトル空間のテンソル積で、$`[V, W]`$ は内部ホムです。内部ホムはベクトル空間ですが、通常のホムセット（外部ホム）$`\mbf{Vect}(V, W)`$ は単なる集合だと解釈します。

テンソル積に関しては次が成立します。

$`\text{For }U,V, W\in |\mbf{Vect}|\\
\quad \mbf{Vect}(U\otimes V, W) \cong \mbf{Vect}(V, [U, W]) \In \mbf{Set}
`$

この同型を与える写像はカリー化〈currying〉（左から右）と反カリー化〈uncurrying〉（右から左）です。

直和に関しては次が成立します。

$`\text{For }U,V, W\in |\mbf{Vect}|\\
\quad \mbf{Vect}(U + V, W) \cong \mbf{Vect}(U, W) \times \mbf{Vect}(V, W)\In \mbf{Set}
`$

テンソル積と直和に関する分配法則は次の形です。

$`\text{For }U,V, W\in |\mbf{Vect}|\\
\quad U\otimes (V + W) \cong U\otimes V + U\otimes W \In \mbf{Vect}
`$

分配法則を圏論的な方法で示すことを目標にします。

シーケントと推論

長い矢印の左右にベクトル空間を置いた形（記号的表現）をシーケント〈sequent〉と呼びます。

$`\quad V \To W`$

シーケントの意味はホムセット $`\mbf{Vect}(V, W)`$ です。シーケントとは、ホムセットを簡略に書いたものだと思ってかまいません。

シーケントを上段と下段に並べた形はシーケントの推論〈inference〉です。

$`\quad V \To W\\
\VRule \gamma\\
\quad X \To Y
`$

これは、ホムセット $`\mbf{Vect}(V, W)`$ からホムセット $`\mbf{Vect}(X, Y)`$ への写像 $`\gamma`$ が在ることを意味します。例えば：

$`\quad U\otimes V \To W\\
\VRule \mrm{Curry}_{U, V, W}\\
\quad V \To [U, W]
`$

これは、次のように書き換えることができます。

$`\quad \mrm{Curry}_{U, V, W} :
\mbf{Vect}(U\otimes V , W) \to
\mbf{Vect}( V , [U, W]) \In \mbf{Set}
`$

ホムセット間の写像にイチイチ名前を付けるのは面倒なので、自然言語（日本語）による注釈でもかまいません。

$`\quad U\otimes V \To W\\
\VRule \text{カリー化}\\
\quad V \To [U, W]
`$

直和に関する法則を、シーケントと推論の形で書くと次のようになります。

$`\quad U + V \To W\\
\VRule \text{2つの線形写像に分解}\\
\quad U \To W \;,\: V \To W
`$

下段の意味はホムセットの直積 $`\mbf{Vect}(U, W)\times \mbf{Vect}(V, W)`$ です。

米田原理を使う

米田原理によれば、2つのベクトル空間 $`A, B`$ が同型であることを示すには、次の同型を示せばよいことになります。

$`\quad \check{A} \cong \check{B} \In \mbf{Vect}^\vee`$

余前層 $`\check{A}, \check{B}`$ は次のようでした。

$`\quad \check{A} := \mbf{Vect}(A, \hyp) \;: \mbf{Vect} \to \mbf{Set} \In \mbf{CAT}\\
\quad \check{B} := \mbf{Vect}(B, \hyp) \;: \mbf{Vect} \to \mbf{Set} \In \mbf{CAT}
`$

余前層の同型は次のことです。

$`\text{For }X\in |\mbf{Vect}|\\
\quad \mbf{Vect}(A, X ) \cong \mbf{Vect}(B, X) \In \mbf{Set}
`$

シーケント $`A\To X`$ からシーケント $`B\To X`$ への可逆な推論達の列があれば、上記のホムセット同型は得られます。

分配法則に関して言えば、次の2つのシーケントを結ぶ可逆な推論達の列があれば、分配法則が言えます。

$`\quad U\otimes (V + W) \To X \\
\quad U\otimes V + U\otimes W \To X
`$

分配法則の証明

以下のようなシーケントの推論達の列が、ベクトル空間の分配法則の証明を与えます。

$`\quad U\otimes (V + W) \To X \\
\VRule \text{カリー化}\\
\quad (V + W) \To [U,X] \\
\VRule \text{2つの線形写像に分解}\\
\quad V \To [U, X] \;,\: W \To [U,X] \\
\VRule \text{反カリー化 （二箇所）}\\
\quad U\otimes V \To X \;,\: U\otimes W \To X \\
\VRule \text{1つの線形写像に合成}\\
\quad U\otimes V + U\otimes W \To X
`$

すべての推論は可逆です。つまり、ホムセットのあいだの同型を与えます。これから、次の同型が存在します。

$`\text{For }X \in |\mbf{Vect}|\\
\quad \mbf{Vect}(U\otimes (V + W), X) \cong \mbf{Vect}(U\otimes V + U\otimes W, X) \In \mbf{Set}`$

$`X`$ は任意のベクトル空間なので、上記同型は余前層の同型を意味します。米田原理から、ベクトル空間の同型が言えます。

$`\quad U\otimes (V + W) \cong U\otimes V + U\otimes W \In \mbf{Vect}`$

おわりに

ベクトル空間の分配法則が証明できました。この結果自体は、要素を使って同型を構成しても証明できます。ここで使った方法は、ベクトル空間の要素（ベクトル）には一切言及していません。圏論的だと言えます。

シーケントと推論の形式を導入しましたが、これは、便利な記法と計算術です。シーケントはホムセットのことであり、推論はホムセットのあいだの写像です。形式的・記号的な計算はシッカリした“意味”を持ちます。

ここでの分配法則の証明は、便利な記法と計算術であるシーケント計算と、証明原理である米田原理をデモンストレートする事例でした。