このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

困った時の米田頼み、ご利益ツールズ

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

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

内容:

過去の事例: 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)。同様に、[Cop, Set]は、Cから集合圏Setへの反変関手と自然変換からなる圏です。

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

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

  • 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):CopSet を定義できます。記法が煩雑になるのを防ぐために ψ := 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):CopSet) という対応が関手であることも分かります(練習問題)。具体的には次が成立します。

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

ここでιFは、関手 F:CopSet が定義する恒等自然変換 F⇒F:CopSet です。

ラムダ記法と米田の星

前節の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) : CopSet

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

  • A := λy.C(A, y) : CSet

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

f:A→B に対して、f:A⇒B:CopSet は前節で定義した自然変換です。つまり:

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

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

  • (-) = y共変関手 C→[Cop, Set] であるが、この共変関手の特定の値 A:CopSet反変関手である。
  • (-)反変関手 Cop→[C, Set] であるが、この反変関手の特定の値 A:CSet共変関手である。

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

超巨大圏CATと直積

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

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

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

記号'×'は、圏CAT内での“圏の直積”/“関手の直積”のために使います。C, DCAT に対して、C×Dは直積圏です。また、F:CC', G:DD' 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)\odotD(B, Y)

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

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

F:CSet, G:DSet を2つの関手とします。新しい関手F\otimesGを次のように定義します。

  • F\otimesG := λ(x, y).F(x)\odotG(y) : C×DSet

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

  • (F\otimesG)(x, y) := (F(x)\odotG(y) in Set)

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

  • (F\otimesG)(A, B) := (F(A)\odotG(B) in Set)

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

  • (F\otimesG)(f, g) := (F(f)\odotG(g):F(A)\odotG(B)→F(C)\odotG(D) in Set)

別な書き方として:

  • F\otimesG := (F×G)*\odot : C×DSet

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

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

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

  • \otimesβ)(X, Y) : (F\otimesG)(X, Y)→(H\otimesK)(X, Y)

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

  • \otimesβ)(X, Y) := (αX\odotβY : F(X)\odotG(Y)→H(X)\odotK(Y) in Set)

この定義が、実際に F\otimesG⇒H\otimesK:C×DSetという自然変換を定義することを確認するのは練習問題。

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


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

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

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

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

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

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

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

  • C1×C2×...×Cn→[C1op×C2op×...×Cnop, Set]

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

C1×C2×...×Cn→[C1op×C2op×...×Cnop, Set] の形をした米田埋め込みをマルチ米田埋め込み(multi-Yoneda embidding)と呼ぶことにします。ここでは、n = 2 のケース、2つの圏C, Dに対する C×D→[Cop×Dop, Set] を考えます。

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

  • yC×D:C×D→[(C×D)op, Set]

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

  • yC×D:C×D→[Cop×Dop, Set]

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

  • (A, B) = A\otimesB
  • (f, g) = f\otimesg

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

  • (A, B) = yC×D(A, B)
  • (f, g) = yC×D(f, g)

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

(A, B) = λ(x, y).(C×D)((x, y), (A, B))
         = λ(x, y).C(x, A)\odotD(y, B)
         = λ(x, y).A(x)\odotB(y)
         = A\otimesB

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

  • (f, g)(X, Y) : (A, B)(X, Y)→(C, D)(X, Y)
  • (f\otimesg)(X, Y) : (A\otimesB)(X, Y)→(C\otimesD)(X, Y)

先の計算から:

  • (A, B)(X, Y) = (A\otimesB)(X, Y) = C(X, A)\odotD(Y, B)
  • (C, D)(X, Y) = (C\otimesD)(X, Y) = C(X, C)\odotD(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\otimesg)(X, Y)(v, w)
= (fX\odotgY)(v, w)
= (fX(v), gY(w))
= (v;f, w;g)

よって、(f, g) = f\otimesg が成立します。

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

  • (A1, ..., An) = A1\otimes ... \otimesAn
  • (f1, ..., fn) = f1\otimes ... \otimesfn

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

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

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

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

  • C := [Cop, Set]

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

  • y:CC

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

  • y●●:C2C●●

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

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

  • y : C×CopC (ここで、C = [Cop×C, Set])

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

  • y(A, B) = A\otimesB
  • y(f, g) = f\otimesg

おわりに

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

*1:関手 F:CD の対象部分が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)とか呼ぶべきじゃないかと思う今日このごろ。