困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 (はてなBlog)

米田埋め込みはやっぱり役に立ちますね。米田埋め込みを利用するときに便利なツールを幾つか紹介します。それらのツール達は：

関手に使うラムダ記法
米田の星 (-)^米, (-)_米
関手・自然変換のテンソル積
マルチ米田埋め込みのドット記法

内容：

過去の事例： CPSと確率変数
困った時の米田頼み、もうひとつの例
米田埋め込み
ラムダ記法と米田の星
超巨大圏CATと直積
関手・自然変換のテンソル積
マルチ米田埋め込みとテンソル積
前層の圏とマルチ米田埋め込み
おわりに

過去の事例： CPSと確率変数

プログラミングにおいて、継続（continuation）という不思議な概念が登場します。継続を用いたプログラミング技法として、継続渡し方式（CPS; Continuation Passing Style）という何だかヨクワカラナイやり方があります。

継続／継続渡し方式に関わる不可解さは、米田埋め込み（Yoneda embedding）を使って解釈するとだいぶ解消します。

確率論で出てくる確率変数（random variable, stochastic variable）という概念に、僕はフラストレーションを募らせていました。なんなんだ!? アレは。確率変数を米田埋め込みとみなすと、事情はスッキリします。

「確率変数」の正体は米田埋め込み

これらの経験から、米田埋め込みはご利益がある、実にありがたいもんだと感じています。

困った時の米田頼み、もうひとつの例

イライラするくらい謎な現象に出会ったら、背後に米田埋め込みがいないか？と探ってみる。こういう行動様式を「困った時の米田頼み」と呼びましょう。比較的最近、また米田様のご利益に与〈あずか〉る機会がありました。ありがたや、ありがたや。

自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出来そうではありますが、バシッと決められないもどかしさを感じてました。

今まで米田頼みをしたことがなかったのですが、「ひょっとしたら」と思って米田埋め込みを探してみました。… ありましたね(ニコ)。これでたぶん、バシッと決められます。でも、今日この話はしません。まだ詰め切れてないので、もう少し考えてからにします。

この記事では、米田埋め込みをより便利に使うための準備をします。ちょっとした記法を導入するだけです。しかし、記法でモノの見方が変わることもあります（「記法バイアスと記法独立な把握：順序随伴を例として」参照）。

米田埋め込み

Cを圏とします。[C, Set]を、Cから集合圏Setへの関手の圏とします。[C, Set]は圏であり、その対象は関手、射は自然変換です。つまり、|[C, Set]| = Functor(C, Set)、F, G∈Functor(C, Set) に対してホムセットは [C, Set](F, G) = NatTransform(F, G)。同様に、[C^op, Set]は、Cから集合圏Setへの反変関手と自然変換からなる圏です。

米田埋め込みは、y:C→[C^op, Set] という関手です。“埋め込み”と呼ばれるのは、yは充満忠実（ホムセットごとに全単射な）関手であり、対象部分 |C|→Functor(C^op, Set) もup-to-isoで単射 *1となるからです。

米田埋め込みの定義を見ておきましょう。まず、A∈|C| に対して、関手 y(A):C^op→Set を、ホムセットにより次のように定義します。

y(A)(X) := (C(X, A) in Set)
y(A)(u:X→Y) := (λw∈C(Y, A).(u;w:X→Y) : C(Y, A)→C(X, A) in Set)

上記の定義で、y(A)(X)は(y(A))(X)の意味です。このような書き方はしばしば使われるので慣れてください。二番目で定義されるy(A)(u:X→Y)は、C(u, A)とも書きます。この書き方を使うなら、

y(A)(X) := C(X, A)
y(A)(u:X→Y) := (C(u, A) : C(Y, A)→C(X, A))

あるいは簡単に、

y(A) := C(-, A)

ここで、ハイフンは無名のラムダ変数で、対象も射もハイフンに代入できるものとします。

f:A→B in C のとき、自然変換 y(f:A→B)::y(A)⇒y(B):C^op→Set を定義できます。記法が煩雑になるのを防ぐために ψ := y(f:A→B) と置きます。ψの成分は、

ψ_X : y(A)(X)→y(B)(X) in Set

これは、

ψ_X : C(X, A)→C(X, B)

というホムセットのあいだの写像です。その定義は：

ψ_X := λv∈C(X, A).(v;f:X→B) : C(X, A)→C(X, B) in Set

ψが自然変換になることは、定義を追いかければ分かります（練習問題）。

さらに、A|→(y(A) = C(-, A))、(f:A→B)|→(y(f)::C(- A)⇒C(- , B):C^op→Set) という対応が関手であることも分かります（練習問題）。具体的には次が成立します。

y(f;g) = y(f);y(g) （右辺のコロンは、自然変換の図式順縦結合）
y(id_A) = ι_y(A)

ここでι_Fは、関手 F:C^op→Set が定義する恒等自然変換 F⇒F:C^op→Set です。

ラムダ記法と米田の星

前節のC(-, A)のように、ハイフン（やアンダースコア）を無名変数とした書き方はよく使われます。ラムダ記号を使えば：

C(-, A) = λx.C(x, A)

変数が1個ならハイフンでもいいのですが、複数の変数になるとハイフンではキビシイので、通常のラムダ記号／ラムダ束縛変数も使うことにします。ラムダ束縛変数の使い方に関して、次の規約を設けておきます。

X, Yなどの文字は対象を表す。
f, gなどの文字は射を表す。
x, yなどの文字は対象も射も表す。

例えば、λX.C(A, X)は共変のホム関手の対象部を表し、λ(x, y).C(x, y)は反変・共変の二項ホム関手全体を表します。

さて、A∈|C| で定義される反変関手をA^米で表すことにします。つまり：

A^米 := λx.C(x, A) : C^op→Set

上付きの文字はアスタリスクではなくて漢字の「米」です。米田の米〈よね〉からです。下付きの米は次のように定義します。

A_米 := λy.C(A, y) : C→Set

こちらは共変関手（opが付いてない）です。

f:A→B に対して、f^米:A^米⇒B^米:C^op→Set は前節で定義した自然変換です。つまり：

(-)^米 = y = (米田埋め込み)

同様に、(-)_米は C^op→[C, Set] という関手で、余米田埋め込み（coYoneda embedding）とでも呼ぶべきものです。次の点に注意してください。

(-)^米 = y は共変関手 C→[C^op, Set] であるが、この共変関手の特定の値 A^米:C^op→Set は反変関手である。

(-)_米は反変関手 C^op→[C, Set] であるが、この反変関手の特定の値 A_米:C→Set は共変関手である。

上付き／下付きで使う'米'を米田の星（Yoneda star, Yoneda asterisk）と呼ぶことにします。口頭では「うえヨネ」「したヨネ」と発音すればいいでしょう。

超巨大圏CATと直積

“圏の圏”を通常Catと書きますが、これは“小さな圏の圏”です。例えば、SetはCatの対象になりません。CATを必ずしも小さくない（ただしホムセットは小さい*2）圏の圏だとします。Set∈|CAT| が成立するとします。また、Cat∈|CAT| であり、同時に Cat⊆CAT（充満部分圏）でもあるとします。

CATは存在するのか？そんなものを考えていいのか？という疑問はありますが、ここは楽観的に「あれば便利だから、あることにしちゃえ」という方針でいきます。僕はよく知らないのですが、集合論に強い公理を付け加えれば、CATを合理化できるようです。

この記事内では、集合A, Bの直積を一時的にA $\odot$ Bと書きます。その理由のひとつは、Setを他のモノイド圏 V = (V, $\odot$ , I) に取り替えても成立する議論をするからです。' $\odot$ 'は、直積かも知れないし、他のモノイド積かも知れない、という含みがあります。もっと切実な理由は、'×'を使うと混乱してしまう危険があるからです。

記号'×'は、圏CAT内での“圏の直積”／“関手の直積”のために使います。C, D∈CAT に対して、C×Dは直積圏です。また、F:C→C', G:D→D' in CAT に対して、F×Gは関手の直積で、

F×G:C×C'→D×D'
(F×G)(A, B) = (F(A), G(B))
(F×G)(f:A→B, f':A'→B') = (F(f:A→B), G(f':A'→B'))

ホムセットに関して次の等式が成立します。

(C×D)((A, B), (X, Y)) = C(A, X) $\odot$ D(B, Y)

もう一度繰り返しますが、'×'はCATにおける圏の直積／関手の直積で、' $\odot$ 'はSetにおける集合の直積／写像の直積です。慣れてしまえば、どちらも'×'と書いても大丈夫ですが、当面（たぶんこの記事内だけ）は区別します。

関手・自然変換のテンソル積

F:C→Set, G:D→Set を2つの関手とします。新しい関手F $\otimes$ Gを次のように定義します。

F $\otimes$ G := λ(x, y).F(x) $\odot$ G(y) : C×D→Set

これは、次のように書いても同じです。

(F $\otimes$ G)(x, y) := (F(x) $\odot$ G(y) in Set)

もっと丁寧に書くと、(A, B)∈|C×D| に対しては、

(F $\otimes$ G)(A, B) := (F(A) $\odot$ G(B) in Set)

そして、f:A→C in C, g:B→D in D に対しては、

(F $\otimes$ G)(f, g) := (F(f) $\odot$ G(g):F(A) $\odot$ G(B)→F(C) $\odot$ G(D) in Set)

別な書き方として：

F $\otimes$ G := (F×G)* $\odot$ : C×D→Set

ここで、'×'は関手の直積、'*'は関手の図式順結合です。 $\odot$ :Set×Set→Set は集合圏の直積で、二項関手です。

F $\otimes$ GをFとGのテンソル積（tensor product）と呼ぶことにします*3。FとGが値を取る圏がSetでなくても、モノイド圏 V = (V, $\odot$ , I) ならば関手のテンソル積を定義できます。

次に、自然変換 α::F⇒H:C→Set と β::G⇒K:D→Set のテンソル積α $\otimes$ βを定義しましょう。α $\otimes$ β::F $\otimes$ G⇒H $\otimes$ K:C×D→Set となります。具体的には、次の成分を定義すればOKです。

(α $\otimes$ β)_{(X, Y)} : (F $\otimes$ G)(X, Y)→(H $\otimes$ K)(X, Y)

関手のテンソル積の定義から、この成分は F(X) $\odot$ G(Y)→H(X) $\odot$ K(Y) なので、次のように定義できます。

(α $\otimes$ β)_{(X, Y)} := (α_X $\odot$ β_Y : F(X) $\odot$ G(Y)→H(X) $\odot$ K(Y) in Set)

この定義が、実際に F $\otimes$ G⇒H $\otimes$ K:C×D→Setという自然変換を定義することを確認するのは練習問題。

以上に定義した関手・自然変換のテンソル積は、任意の関手・自然変換に定義できるものではありません。値を集合圏（他のモノイド圏でもいいけど）に取る関手とそのあいだの自然変換に対してだけ定義できます。

この節で定義した“テンソル積”に対する適切な定式化は、おそらくラックス・モノイド関手*4でしょう。ラックス・モノイド関手については次の記事を参照してください。

Catを“小さい圏の圏”として、C∈|Cat| に対して F(C) := [C, Set] とします。Cが小さくても関手圏[C, Set]が小さいとは限りません（つうか、大きくなります）。F:C→D in Cat に対して、F(F):F(D)→F(C) in CAT が引き戻しとして定義できるので、Fは反変関手 F:Cat^op→CAT になります。

先に定義した“テンソル積”は、 $\otimes$ _C,D:F(C)×F(D)→F(C×D) という二項関手の族になります。 $\otimes$ _C,D達は、結合律を満たします。

Jを自明な圏（単一対象と恒等だけからなる圏）とします。F(J) = [J, Set] $\stackrel{\sim}{=}$ Set です。ε:J→F(J) を、Jの単一対象にSetの単元集合を対応させる関手とします。εがラックス・モノイド関手としての単位となります。

CatもCATも直積に関するモノイド圏とみなして、F:Cat→CATと $\otimes$ _C,Dとεが、ラックス・モノイド関手を構成するようです。

マルチ米田埋め込みとテンソル積

Cの米田埋め込みは、C→[C^op, Set] という関手でした。複数の圏 C₁, C₂, ..., C_n に対して、次の形の米田埋め込みも考えられます。

C₁×C₂×...×C_n→[C₁^op×C₂^op×...×C_n^op, Set]

これは、C = C₁×C₂×...×C_n と置いてしまえば通常の米田埋め込みと変わりませんが、それでも複数の圏が介在する状況を調べておく価値はあります。

C₁×C₂×...×C_n→[C₁^op×C₂^op×...×C_n^op, Set] の形をした米田埋め込みをマルチ米田埋め込み（multi-Yoneda embidding）と呼ぶことにします。ここでは、n = 2 のケース、2つの圏C, Dに対する C×D→[C^op×D^op, Set] を考えます。

通常の米田埋め込み y:C→[C^op, Set] はCに依存するので、（必要があれば）y_Cと書くことにします。y_C×Dを考えると：

y_C×D:C×D→[(C×D)^op, Set]

(C×D)^op = C^op×D^op なので、次の形になります。

y_C×D:C×D→[C^op×D^op, Set]

y_C×Dの具体的な形を調べることで、次の公式を示しましょう。

(A, B)^米 = A^米 $\otimes$ B^米
(f, g)^米 = f^米 $\otimes$ g^米

米田の星(-)^米はyと同じ意味でした。

(A, B)^米 = y_C×D(A, B)
(f, g)^米 = y_C×D(f, g)

(A, B)∈C×D に対して実際に計算してみます。

(A, B)^米 = λ(x, y).(C×D)((x, y), (A, B))
         = λ(x, y).C(x, A)D(y, B)
         = λ(x, y).A^米(x)B^米(y)
         = A^米B^米

次に、f:A→C in C, g:B→D in D として、(f, g)^米とf^米 $\otimes$ g^米を計算してみます。X, Y∈|C×D| として、自然変換の(X, Y)成分を考えます。

(f, g)^米_{(X, Y)} : (A, B)^米(X, Y)→(C, D)^米(X, Y)
(f^米 $\otimes$ g^米)_{(X, Y)} : (A^米 $\otimes$ B^米)(X, Y)→(C^米 $\otimes$ D^米)(X, Y)

先の計算から：

(A, B)^米(X, Y) = (A^米 $\otimes$ B^米)(X, Y) = C(X, A) $\odot$ D(Y, B)
(C, D)^米(X, Y) = (C^米 $\otimes$ D^米)(X, Y) = C(X, C) $\odot$ D(Y, D)

(v:X→A)∈C(X, A), (w:Y→B)∈D(Y, B) だとして、

 (f, g)^米_{(X, Y)}(v, w)
= (v, w);(f, g)
= (v;f, w;g)

 (f^米g^米)_{(X, Y)}(v, w)
= (f^米_Xg^米_Y)(v, w)
= (f^米_X(v), g^米_Y(w))
= (v;f, w;g)

よって、(f, g)^米 = f^米 $\otimes$ g^米が成立します。

2つの圏に関するマルチ米田埋め込みを考えましたが、より一般に、マルチ米田埋め込みの値（埋め込んだ先）はテンソル積で展開できます。

(A₁, ..., A_n)^米 = A₁^米 $\otimes$ ... $\otimes$ A_n^米
(f₁, ..., f_n)^米 = f₁^米 $\otimes$ ... $\otimes$ f_n^米

前層の圏とマルチ米田埋め込み

米田埋め込みの余域となる圏は[C^op, Set]です。この圏は、Cの前層の圏（category of presheaves）と呼ばれます。C^op→Set という関手を前層（presheaf）と呼ぶからです。

[C, Set]は単なる（共変の）関手の圏ですが、余前層の圏（category of copresheaves）と呼ぶことがあります。単なる関手をわざわざ余前層と呼ぶのもどうかな？と思いますが、シュルマン（Mike Shulman）は「余前層」がふさわしい文脈があるのだ、と言ってました。

さて、Cの前層の圏は頻繁に登場するので、毎回[C^op, Set]と書くのは面倒です。略記を導入します。Cにハットを載せた記法をたまに見ますが、ここでは右肩にドットを付けることにします。

C^● := [C^op, Set]

この記法を使うと、米田埋め込みは次のように書けます。

y:C→C^●

マルチ米田埋め込み C×C→[C^op×C^op, Set] は次のように書きます。

y^●●:C²→C^●●

[(C^op)ⁿ, Set]を表すのに、Cの右肩にドットをn個載せることにして、対応するマルチ米田埋め込みもyの右肩にドットをn個載せて表します。

余前層の圏への余米田埋め込みは y_●:C→C_● と下付きドットにします。この記法の応用として、共変と反変が混じった米田埋め込みも簡略に記述できます。例えば、

y^●_● : C×C^op→C^●_● （ここで、C^●_● = [C^op×C, Set]）

y^●_●は、米田の星とテンソル積で次のように書けます。

y^●_●(A, B) = A^米 $\otimes$ B_米
y^●_●(f, g) = f^米 $\otimes$ g_米

おわりに

今回紹介したツール達は、前層の圏・余前層の圏・米田埋め込みを扱う際に重宝するものです。「困った時の米田頼み」で、米田様にお願いするとき、これらのご利益ツールズがあると、ご利益にありつくチャンスが増えると思います。

*1:関手 F:C→D の対象部分がup-to-isoで単射とは、(F(A) $\stackrel{\sim}{=}$ F(B) in D) ⇒ (A $\stackrel{\sim}{=}$ B in C) なことです。

*2:ホムセットも小さくない圏を扱いたいときもありますが、今回はそこまで大きな圏は登場しないので、局所小（locally small）の条件を入れておきます。

*3:「テンソル積」があまりにも多用されるので、この言葉を使うことに躊躇はあったのですが、それ以外に適切な呼び名が思い浮かばない。

*4:ラックス・モノイド関手は、関手を台（underlying thing）とするモノイド類似代数系なので、ラクソイド（laxoid）とか呼ぶべきじゃないかと思う今日このごろ。