どうやら、米田埋め込みを単位とするモナドがありそうです。ちゃんと構成するのはけっこう大変。このモナドを定義するためのアウトラインを示します。
内容:
伝説としての米田モナド
Cを圏として、米田埋め込み〈Yoneda embedding〉yCは、Cから“Cの前層の圏”PSh(C)への関手 yC:C→PSh(C) です。この米田埋め込みyを単位とするモナドがあるらしいという話は、キュリア(Pierre-Louis Curien)の論文で知りました。次に示す論文の第7節"Profunctors as a Kleisli category"にそのことが書いてあります。
- Title: Operads, clones, and distributive laws (2012)
- Author: Pierre-Louis Curien
- Pages: 24ページ
- URL: https://arxiv.org/abs/1205.3050
しかし、サイズの問題があり正面からモナドを構成するのは難しいため、モナドの代わりにクライスリ構造〈Kleisli structure〉というもの*1を定義しています。
米田埋め込みを単位とするモナドを米田モナド〈Yoneda monad〉と呼ぶことにします。米田モナドの存在を感じ取った人はキュリアだけではないはずです。ずっと昔、おそらくは圏論の草創期から、相当多くの人々が気づいていたであろう、という意味で「圏論のフォークロアのひとつ」と言っていいでしょう。
次節で、米田モナドについて素朴に説明します。その説明どおりには事が進みません。問題を回避して、なんとか米田モナドを定義するプランをその後の節で示します。
前層構成子の上のモナド: 楽観的な導入
Cを圏とします。関手 Φ:Cop→Set を、C上の前層〈presheaf〉と呼びます。前層は、単に集合圏Setへの(反変)関手に過ぎません。「前層」という呼び名は歴史的な産物(遺物?)です。
関手圏[Cop, Set]を、Cの前層の圏〈category of presheavess〉と呼び、PSh(C)と書きます。
- PSh(C) = [Cop, Set]
- |PSh(C)| = |[Cop, Set]| = Functor(Cop, Set) = (C上の前層=Set値反変関手の全体)
- PSh(C)(Φ, Ψ) = [Cop, Set](Φ, Ψ) = NatTransform(Φ, Ψ:Cop→Set) = (関手Φから関手Ψへの自然変換の全体)
PSh(C)は、自然変換の縦結合を結合とする圏です。したがって、CにPSh(C)を対応させる写像(大きいかも知れない写像)は、|Cat|→|Cat| を定義します(ホントか?)。PShは、「前層の圏」の構成法により圏から圏を作り出す操作なので、前層構成子〈presheaf constructor〉と呼ぶことにします。
今のところ、PShは関手ではありません。関手 F:C→D に対するPSh(F)は定義されてないからです。PShを拡張する反変関手なら比較的簡単に作れます。実は、反変関手じゃダメなんですが、練習問題としてやってみましょう(オマケ扱い)。
F:C→D を関手とするとき、Fopによる前層Γの引き戻し F◎(Γ) = Fop*Γ ('*'は図式順の関手の結合記号)は、PSh(D)→PSh(C) を定義します。Psh←(F) = F◎ : PSh(D)→PSh(C) と置くと、前層構成子PShの拡張であるPSh←が反変関手になることを確認できます。
いま、PSh←は反変関手だと言いましたが、どこからどこへの関手でしょうか? Cを小さい圏に限定すれば、小さい圏の圏Cat上でPSh←が定義されます。PSh←の行き先はCatでしょうか -- そうはなりません、先ほど |Cat|→|Cat| だとウソ言いました。Cが小さくても、関手圏[Cop, Set]が小さいとは限りません。つうか、小さくないです。
必ずしも小さくない圏も許す圏の圏をCATとします。PSh←はCAT上なら自己反変関手になるでしょう(なるのか?)。PSh←は引き戻しを利用するので反変関手でしたが、PSh→(Γ)を、前層Γの前送り(押し出し)で定義すれば、共変の自己関手PSh→もたぶん定義できるでしょう(できるのか?)。米田埋め込みは、yC:C→PSh(C) の形なので、自然変換 y::IdCAT⇒PSh→:CAT→CAT とみなせそうです(ホント?)。
CAT上の自己関手PSh→と自然変換 y::Id⇒PSh→ は既にあります(って、あるのか?)。あと、自然変換 μ::PSh→*PSh→⇒PSh→ がうまいこと見つかれば、CAT上のモナド (PSh→, y, μ) ができます。これが米田モナド(のはず?)です。
サイズの問題とフレイド/ストリートの定理
前節では、随分と楽観的でいいかげんな議論をしました。圏の圏CAT上のモナドとして、ホントに米田モナドが存在するのでしょうか? モナド乗法μの構成はなんだかよく分かりません。その前に、共変の前層関手PSh→はwell-definedでしょうか。そもそもCATなんて使って大丈夫なの??
Iを単一の対象と恒等射だけを持つ自明な圏とします。I∈|CAT| はいいですよね。前層構成子PShが|CAT|上に働いているとすれば、PSh(I) = [Iop, Set] Set ですから、Set∈|CAT| です。もう一度PShを作用させると、PSh(Set) = [Setop, Set] ができます。[Setop, Set]はとてつもなく大きな圏で、ホムセット[Setop, Set](F, G)も小さな集合とは限りません。
ホムセットも巨大になると、普通には扱いようがないので、ホムセットは小さい(局所小〈locally small〉)は要求したいところです。あらためて、CATは、“ホムセットは小さい圏(局所小圏)”の圏だとします。それでも Set∈|CAT| は成立します。PSh(Set)はもはやCATに収まらないので、PShをCAT上の自己関手に拡張することは出来ません。
PSh:|CAT|→|CAT| という前提は諦めざるを得ません。となると、モナドの構成も出来なくなるのですが、モナドの問題はいったん棚上げして、今は前層構成子PShの定義を確立することに集中します。
Cがなんらかの圏だとして、どんなときにPSh(C)は局所小な圏になるでしょうか? この問題に対して、フレイド/ストリート(Peter Freyd, Ross Street)の定理が答えてくれます。
- Title: ON THE SIZE OF CATEGORIES (1995)
- Authors: PETER FREYD AND ROSS STREET
- Pages: 6p. (実質5p.)
- URL: http://www.tac.mta.ca/tac/volumes/1995/n9/v1n9.pdf
フレイド/ストリートによれば、次の2つの命題は同値です。
- 圏Cが小さい圏と圏同値である。
- 圏Cが局所小で、前層の圏PSh(C)も局所小である。
小さい圏と圏同値となる圏を本質的に小さい〈essentially small〉といいます。この言葉を使うと、フレイド/ストリートの(サイズに関する)定理は次の主張です。
- 圏Cは本質的に小さい ⇔ 圏Cは局所小、かつPSh(C)は局所小
これはかなりありがたい定理です。圏の圏Catの定義として、“本質的に小さい圏の圏”を採用しても、|Cat|上のPSh(C)は局所小にとどまります。
例えば、有限集合の圏FinSetを考えます。FinSetは小さい圏でしょうか? この世にあるすべての有限集合の集まりって集合なの? たぶん違うでしょう。しかし、圏Fを次のように定義してみます; |F| = N、ホムセットを F(n, m) := Set({1, 2, ..., n}, {1, 2, ..., m}) として定義。Fは対象が可算個、すべてのホムセットは有限集合という小規模な圏です。FinSetはFと圏同値なので、本質的に小さい圏です。したがって、PSh(FinSet)も局所小な圏になります。
有限次元ベクトル空間の圏FdVectKも、同様な議論で本質的に小さいことが示せるので、PSh(FdVectK)も局所小な扱いやすい圏です。
というわけで、Catを“本質的に小さい圏の圏”としても話はうまくいきそうです。が、今日のところは無難に、Catは“小さい圏の圏”としておきます。圏同値な圏を“同じ”とみなすなら、小さい圏でも本質的に小さい圏と“同じ”で、一般性はそこなわれません*2。次がいえます。
- 圏Cが小さいなら、 前層の圏PSh(C)は局所小である。
これによって、PSh:|Cat|→|CAT| の存在が保証されます。
相対モナド
PSh:|Cat|→|CAT| なのは確実になりました。しかし、|Cat| ≠ |CAT| なので、PShの繰り返し適用が出来ません。通常のモナドの定義ではPShが自己共変関手になる状況を前提しているので、このままではうまくいきません。アルテンキルヒ達(Thorsten Altenkirch, James Chapman, Tarmo Uustalu)による相対モナドにより対処できます。彼らの論文タイトルは、ズバリ「自己関手じゃなくてもモナド作れるよ」です。
- Title: Monads Need Not Be Endofunctors
- Authors: Thorsten Altenkirch, James Chapman and Tarmo Uustalu
- Pages: 15p.
- URL: http://jmchapman.github.io/papers/Relative_Monads.pdf
モナドの定義には、モノイド・スタイルと拡張スタイルがあります(「モナドの定義とか」参照)。モノイド・スタイルは関手上に載った代数系として定義するので代数スタイルと呼んだこともあります。拡張スタイルは、クライスリ拡張オペレータを中心とするもので、プログラミングで使うには便利な定義です。
相対モナドの定義は、まずは拡張スタイルで与えられます。キュリアが使っていたクライスリ構造は、相対モナドとほぼ同じものです。関手 J:C→D の上に相対モナドを定義するのです。J上の相対モナド〈relative monad〉は次のもので構成されます。(T(X), J(X)をTX, JXなどと括弧無しで書いています。)
- 写像 T:|C|→|D|
- X∈|C| に対して、ηX:JX→TX in D
- X, Y∈C と k:JX→TY in D に対して k#:TX→TY in D
η = {ηX | X∈|C|} を単位〈unit〉、kに対するk#をクライスリ拡張〈Kleisli extension〉と呼びます。
上記の素材 T, η, (-)# が相対モナドであるためには、次の法則を満たす必要があります。
- X, Y∈|C|, k:JX→TY in D に対して、ηX;k# = k
- X∈|C| に対して、(ηX)# = idTX
- X, Y, Z∈|C|, k:JX→TY, ℓ:JY→TZ に対して、(k;ℓ#)# = k#;ℓ#
Jがところどころ挿入されている以外は、普通のモナドの定義と同じです。この定義からはじめて、クライスリ圏やアイレンベルグ/ムーア圏を構成できます。また、相対モナドもモノイド(類似構造)として代数的にも定義できます。詳細はアルテンキルヒ達の論文を見てください。
相対モナドとしての米田モナド
米田モナドを相対モナドとして定義しましょう。前節の定義に出てきた素材が、米田モナドでは何に相当するかまとめてみます。
相対モナドの定義 | 米田モナド |
---|---|
圏C | 圏Cat |
圏D | 圏CAT |
関手 J:C→D | 包含関手 Cat→CAT |
写像 T:|C|→|D| | 前層構成子 PSh:|Cat|→|CAT| |
単位射 ηX:JX→TX in D | 米田埋め込み yC:C→PSh(C) in CAT |
クライスリ拡張 k#:TX→TY | 米田拡張 K#:PSh(C)→PSh(D) |
クライスリ拡張とは、モナドの理論のなかで使われる用語です。それに対して米田拡張〈Yoneda extension〉は圏の一般論での用語です。米田拡張についてはnLabに記事があります。
米田モナドにおけるクライスリ拡張が米田拡張になっています。また、米田拡張は、米田埋め込みとカン拡張により構成されます。関手Jは包含関手なので自明です。前層構成子PShと米田埋め込みyは定義済みです。となると、米田モナドの定義問題は、米田拡張(-)#の構成と分析に集約されます。
上の表で列挙した米田モナドの素材が、実際に相対モナドになるためには、先に挙げた法則を満たす必要があります。しかし、法則が等式で成立することは期待できず、up-to-iso(isoは自然変換で与えられる)での法則になります。
- C, D∈|Cat|, K:C→PSh(D) in CAT に対して、yC*K# K
- C∈|Cat| に対して、(yC)# IdPSh(C)
- C, D, E∈|Cat|, K:C→PSh(D), L:D→PSh(E) に対して、(K*L#)# K#*L#
左カン拡張の存在
カン拡張〈Kan extension〉に関しては、nLabの項目がけっこう詳しい解説になっています。
nLab項目と同じ記号を使うとします。p:C→C' という特定の関手があったとして、F:C→D を C'→D まで拡張しましょう、という話です。G:C'→D が p*G = F ('*'は図式順の関手結合)を満たすなら「pに沿ったFの拡張」と言えますが、拡張のなかで普遍的なもの(最良な近似)がカン拡張です。カン拡張には左カン拡張〈left Kan extension〉と右カン拡張〈right Kan extension〉があります。
米田拡張では、pとして 米田埋め込み yC:C→PSh(C) を取ります。F:C→D の、yCに沿った左カン拡張が米田拡張でした。左カン拡張がいつでも存在するわけではありません。したがって、米田拡張も存在するとは限りません。
nLab項目のなかで、左カン拡張が存在する条件について述べられています。nLab項目のProposition 2.8によると、次の条件が満たされるなら F:C→D の左カン拡張が存在します。
- Cが小さい圏である。
- Dは余完備〈cocomplete〉である。
Cが小さいことは前提にしていました。Dが勝手な圏とするなら、余完備性は保証できません。しかし、米田モナドにおいては、F:C→PSh(D') で、D'も小さい圏の場合しか考えません。Dは勝手な圏ではなくて、D = PSh(D') の形に書けるということです。
小さい圏D'をあらためてDと置き直して、F:C→PSh(D) とします。小さい圏Dに対してPSh(D)が余完備かどうかが問題になります。
前層の圏の性質として次があります。
The category of presheaves PSh(C) is the free cocompletion of C.
前層の圏PSh(C)は、Cの自由余完備化である。
前層の圏がもとの圏の余完備化になっているので、PSh(D)は余完備です。
Cが小さい圏で、PSh(D)は余完備なので、F:C→PSh(D) のyCの沿った左カン拡張は存在します。それをF#と置きます。F |→ F# という対応は厳密〈strict〉な一意対応ではありませんが、up-to-isoで一意とは言えます。
残るは
圏Cat、圏CAT、前層構成子 PSh:Cat→CAT、F:C→PSh(D)に対する米田拡張 F#:PSh(C)→PSh(D) の存在は、なんとかなりました。後は、先に挙げた3つの等式(up-to-isoなので同型式と言うべきか)です。
が、僕はカン拡張の計算がろくに出来ないので、3つの等式がよく分かりません、ザンネン。ちゃんと計算している資料も見つからない(あまり熱心に探してないけど)。しかし、状況証拠は揃っているし、キュリアも米田モナドを仮定した議論をしているので、“幻のモナド”ってことはないでしょう。
「困った時の米田頼み、ご利益ツールズ」で述べたように、米田埋め込みだけでも強力な道具になっているので、米田モナド(正確に言うと相対疑モナドかな)の全体を使うともっと強い事を言える可能性があります。