檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2019-01-16 (水)

ベックの分配法則の事例と計算法

| 18:48 | ベックの分配法則の事例と計算法を含むブックマーク

ここんところ「モナドのお勉強をしましょう」というゆるいシリーズ記事(番号とかは付けてない)を書いているのですが、今日はベックの分配法則の例を挙げます。

内容:

  1. リストモナドとバッグモナド
  2. ベックの分配法則
  3. 随伴系から作られるモナド
  4. 分配法則の具体的な記述
  5. その他の分配法則

リストモナドとバッグモナド

今回主に使うモナドは、(毎度おなじみの)集合圏Set上のリストモナド〈list monad〉 List = (List, ηList, μList) です。それと、集合Aからバッグ〈有限マルチセット〉の集合を作るバッグモナド〈bag monad〉 Bag = (Bag, ηBag, μBag) も考えます。その他の例は後で出します。

a1, ..., an∈A に対して、これらの要素のリストは [a1, ..., an] と書きます。これらの要素のバッグは、区切り記号を';'にして、[a1; ...;an] と書くことにします(とりあえずの記法)。リストとバッグ(それと有限集合)の違いは:

  • リストは順序が問題になるが、バッグは順序を問題にしない。[1, 2, 2] ≠ [2, 1, 2] だが、[1; 2; 2] = [2; 1; 2] である。
  • バッグは、有限集合とは違って、重複に意味がある。{1, 2, 2} = {1, 2} だが、[1; 2; 2] ≠ [1; 2] である。

リストもバッグも長さ(サイズ)を持つので、aの長さを |a| と書きます。空リスト/空バッグの長さは0です。モナドの構造を与える演算は:

  • ηList:A→List(A) in Set は、Aの要素からシングルトン・リストを作る演算。
  • μListA:List(List(A))→List(A) in Set は、入れ子のリストを平坦にする演算。
  • ηBag:A→Bag(A) in Set は、Aの要素からシングルトン・バッグを作る演算。
  • μBagA:Bag(Bag(A))→List(A) in Set は、入れ子のバッグを平坦にする演算。

これらが、モナドの結合律と左右の単位律を満たすことは練習問題ですが、計算法(のヒント)はこの記事の後のほうで説明しています。

ベックの分配法則

LとMが圏C上のモナドのとき、ベックの分配法則〈Beck's distributive law〉とは、次の形の自然変換で、とある条件を満たすものです。

  • δ::M*L⇒L*M:CC

ここで、'*'は図式順結合であることに注意してください。反図式順で書くなら:

  • δ::L・M⇒M・L:CC

なんで「分配法則」と呼ぶかは、L = List, M = Bag の例を考えるといいでしょう。ListとBagに関する分配法則δがあったとして、成分で書くと:

  • For A∈|Set|,
    δA:List(Bag(A))→Bag(List(A)) in Set

となります。Bag(A)の要素 a = [a1; ...; an] は、足し算 a1 + ... + an のようなものだと考えます。List(Bag(A))の要素は、 [b1, ..., bm] で、bi は、

  • (bi)ji = ai,ji (1 ≦ ji ≦ ni, ni = |bi|)

のように、二重インデックス族(行列とはちょっと違う) ai,ji で書けます(詳細は後述)。

リスト [b1, ..., bm] を、b1, ..., bm の掛け算(積)とみなしましょう。すると:

  • δA:(Aの要素を足し算したものを掛け算したもの) |→ (Aの要素を掛け算したものを足し算したもの)

となります。これは、“和の積”を“積の和”に展開する操作なので、分配法則による式変形(多項式計算)だと言っていいでしょう。

ベックの分配法則のより詳しいことは、以下の記事に書いてあります。なお、当時(2007年)は「ベックの法則」と呼んでいました。最近はやっぱり「分配」を付けたほうが混同を避けられると思ってます。記法も当時と最近では若干違います。

ベックの分配法則では、モナドLとモナドMの役割が違うので、

  • δは、Mに対するLの分配法則〈distributive law of L over M〉

と呼ぶことにします。通常の分配法則は「足し算に対する掛け算の分配法則〈The distributive law of multiplication over addition〉」なので、不自然な言い方ではないでしょう。

随伴系から作られるモナド

次のような圏を考えます。

  1. Mon : モノイドとモノイド準同型射の圏
  2. CMon : 可換モノイドとモノイド準同型射の圏
  3. ICMon : ベキ等可換モノイドとモノイド準同型射の圏
  4. Pted : 付点集合〈pointed set〉と付点を保つ写像の圏
  5. SRng : 半環(掛け算が可換とは限らない)と半環の準同型射の圏
  6. ISRng : 足し算がベキ等な半環と半環の準同型射の圏
  7. MonZ : 零〈吸収元 | absorbing element〉を持つモノイドとモノイド準同型射の圏

これらの圏の対象は、集合になんらかの構造を載せた構造付き集合〈structured set〉です。なので、構造付き集合にその台集合〈underlying set〉を対応させる忘却関手 UC:CSet を持ちます。以下、圏Cが何であっても、忘却関手 UC を単にUと書きます。

上記の圏の忘却関手は、随伴の左パートナー〈左随伴関手〉 FreeC:SetC を持ち、随伴系 (η, ε: FreeC -| U, FreeC:SetC) が存在します。今使った随伴系の書き方は、「随伴に関する注意事項 // 随伴系の方向」で説明しています。忘却関手の左パートナーは自由生成関手と呼びます。

随伴系があれば、それからモナド (FreeC*U, η, FreeC*ε*U) を作れます。ここで、'*'は関手の図式順結合記号です。次は、上記の圏と随伴系から作ったモナドの一覧です。

自由生成関手 モナドの名前
Mon FreeMon List
CMon FreeCMon Bag
ICMon FreeICMon FinPow(有限ベキ集合)
Pted FreePted Maybe, Pt(付点)
SRng FreeSRng NCPoly(非可換多項式)
ISRng FreeISRng INCPoly(ベキ等非可換多項式)
MonZ FreeMonZ ListZ(零付きリスト)

それほど馴染みがないと思われる下の3つのモナドの台関手を簡単に説明します。

  • non-commutative polynomials NCPoly(A) : 集合Aの要素を不定元として、係数なし(強いて言えば自然数係数)で構成された形式的多項式の集合。掛け算の可換性は仮定しない。
  • (additively-)idempotent non-commutative polynomials INCPoly(A) : 上記の非可換多項式において、足し算をベキ等だとしたもの。
  • lists with zeros ListZ(A) : List(A)∪{⊥}、通常のリスト以外に、特殊な要素⊥(連接の吸収元になる)を追加した集合。

今挙げた随伴系・モナド以外に、可換半環でパラメトライズ(インデキシング)された随伴系・モナドの族を紹介します。Rを可換半環として、R上の加群(左右の別はない)と加群準同型射の圏をModRとします。引き算ができるとは限らないので、正確には半加群ですが、めんどうなので加群と呼んでしまいましょう。ModRも構造付き集合の圏なので、忘却関手と自由生成関手による随伴系を構成できます。

  • (η, ε: FreeModR -| U, FreeModR:SetModR)

FreeModR(A) は、Aから生成されたR上の(あるいはR係数の)自由加群(自由に生成された加群)と呼びます。随伴系からモナドが構成できるので、モナドの表に追加すれば:

自由生成関手 モナドの名前
ModRFreeModR LinCombR(R-線形結合)

LinCombR(A) は、集合Aの要素達のR係数形式的線形結合〈formal linear combination over R〉の全体です。これは、R係数の1次式を計算するモナドです。可換半環Rを可換環にとれば、通常の加群の議論になり、体にとればベクトル空間の議論になります。

バッグモナドBagと有限ベキ集合モナドFinPowは、可換半環を使った記述が可能です。

  • Bag(A) ¥stackrel{¥sim}{=} LinCombN(A) = U(FreeModN(A)) in Set
  • FinPow(A) ¥stackrel{¥sim}{=} LinCombB(A) = U(FreeModB(A)) in Set

ここで、Nは自然数の半環、Bは{0, 1}に 1 + 1 = 1 と足し算を入れた半環です。バッグモナドは、N係数1次式のモナドと同じであり、有限ベキ集合モナドは、B係数1次式のモナドと同じです。

分配法則の具体的な記述

リストモナド、バッグモナド、有限ベキ集合モナドは、コレクション(モノの集まり)データ型を構成するモナドです。しかしながら、モナドの由来となる随伴系を見ると、代数的構造に対する自由生成-忘却スタイルの随伴系になっています。起源が代数的なので、計算も代数的になります。

δ::Bag*List⇒List*Bag:SetSet を、バッグモナドに対するリストモナドの分配法則だとして、δを具体的に記述することを考えます。バッグ [a1; ...; an] は形式的足し算 a1 + ... + an で、リスト [a1, ..., an] は形式的掛け算 a1・... ・an のことだと思いましょう。ここでの形式的とは、「形だけの」という意味で、[2; 3; 3] を 2 + 3 + 3 と書いても、8 と値を算出することはしないのです。あくまで「式(形式)」であって、「値(算出値)」は考えません。

バッグは足し算〈和〉、リストは掛け算〈積〉とみなすので、次のように書けます。

 ¥[a_1;¥:...;¥: a_n¥] ¥:=¥: ¥sum_{i = 1}^{n}a_i

 ¥[a_1,¥:...,¥: a_n¥] ¥:=¥: ¥prod_{i = 1}^{n}a_i

バッグのリスト、つまり“和の積”を書き下しましょう。幾つかのバッグ〈和〉をギリシャ文字αと添字番号を使って、α1, ..., αn とすると、それらのリスト〈積〉は:

 ¥[¥alpha_1,¥:...,¥: ¥alpha_n¥] ¥:=¥: ¥prod_{i = 1}^{n}¥alpha_i

各 i ごと(1 ≦ i ≦ n)の αi は:

 ¥alpha_i ¥:=¥: ¥[(¥alpha_i)_1;¥:...;¥: (¥alpha_i)_{n_i}¥] ¥:=¥: ¥sum_{j_i = 1}^{n_i}(¥alpha_i)_{j_i}

したがって、

 ¥[¥alpha_1,¥:...,¥: ¥alpha_n¥] ¥:=¥: ¥prod_{i = 1}^{n}¥sum_{j_i = 1}^{n_i}(¥alpha_i)_{j_i}

 ¥alpha_{i, j_i} ¥: :=¥: (¥alpha_i)_{j_i} と置くと、 ¥alpha_{i, j_i} は二重インデックス族ですが、行列とは違って、インデックスセットが(必ずしも)矩形にはなりません。j の動く範囲が i ごとに変化するので、インデックスセットの形がガタガタです。

記述を簡略にするためにインデックスセットに名前を付けておきましょう。

  • I := {1, ..., n}
  • Ji := {1, ..., ni}, ni = |αi|

iが動く範囲がIで、jiが動く範囲がJiです。この記号を使うと:

 ¥[¥alpha_1,¥:...,¥: ¥alpha_n¥] ¥:=¥: ¥prod_{i ¥in I}¥sum_{j_i ¥in J_i}¥alpha_{i, j_i}

ちょっと簡略になりました。この“和の積”が、“積の和”に変形されます。

“積の和”の記述のために、マルチインデックスを準備します。太字のインデックス j は、Ji 達の直積集合 J := J1×...×Jn を走るとします。j = (j1, ..., jn), ji∈Ji 。マルチインデックスを使って“積の和”を書けば:

 ¥sum_{{¥b j}¥in {¥b J}} ¥prod_{i ¥in I}¥alpha_{i, j_i}

分配法則が成立するなら、“和の積”と“積の和”が等しいので、

 ¥prod_{i ¥in I}¥sum_{j_i ¥in J_i}¥alpha_{i, j_i} ¥:=¥: ¥sum_{{¥b j}¥in {¥b J}} ¥prod_{i ¥in I}¥alpha_{i, j_i}

これが、分配法則の一般的な形です。j を (j1, ..., jn) に展開して書いたほうが見やすいかも知れません。

 ¥prod_{i ¥in I}¥sum_{j_i ¥in J_i}¥alpha_{i, j_i} ¥:=¥: ¥sum_{(j_1, ..., j_n)¥in {¥b J}}¥( ¥prod_{i ¥in I}¥alpha_{i, j_i} ¥)¥,,¥: {¥b J} = ¥prod_{i = 1}^{n}J_i

δA:List(Bag(A))→Bag(List(A)) in Set の具体的な記述は、[α1, ..., αn]∈List(Bag(A)) に対して、

 ¥delta_A(¥[¥alpha_1,¥: ...,¥:¥alpha_n¥]) ¥:=¥: ¥delta_A(¥prod_{i ¥in I}¥sum_{j_i ¥in J_i}¥alpha_{i, j_i}) ¥: :=¥: ¥sum_{(j_1, ..., j_n)¥in {¥b J}}¥( ¥prod_{i ¥in I}¥alpha_{i, j_i} ¥)

総和記号は形式的な和(つまりバッグ)、総積記号は形式的な積(つまりリスト)と解釈します。

バッグモナドに対するリストモナドの分配法則が、ベックの分配法則の公理(分配法則の法則)を満たすことを具体的に確認するときは、今述べた具体的な表示を使って具体的に計算します。結果は当たり前のことなんですが、一回は確認する必要があります。

その他の分配法則

今まで説明した、Bagに対するListの分配法則を δBag,List と書きましょう。他にも(ベックの)分配法則があるからです。

δBag,List とほとんど同じ構成で、有限ベキ集合モナドFinPowに対するListの分配法則 δFinPow,List を定義できます。

Maybeモナド(付点モナド)に対しても、Listの分配法則があります。δMaybe,ListA:List(Maybe(A))→Maybe(List(A)) は、⊥をひとつでも含むリストはすべて⊥にしてしまう写像として定義できます。

これで3つの(ベックの)分配法則が定義できました。

  1. δBag,List::Bag*List⇒List*Bag:SetSet
  2. δFinPow,List::FinPow*List⇒List*FinPow:SetSet
  3. δMaybe,List::Maybe*List⇒List*Maybe:SetSet

これらの分配法則は、モノイドの圏Mon上のモナドに“持ち上がり”ます。さらに、集合圏Set上のモナドへと“引き戻せ”ます。その結果、分配法則とSet上のモナドは、次のように対応します。

分配法則 Set上のモナド
δBag,List NCPoly
δFinPow,List INCPoly
δMaybe,List ListZ

“持ち上げ”や“引き戻し”に正確な意味を与えるには、モナドと随伴の一般論が必要ですが、一般論の前に事例を知っていれば理解の助けになるでしょう。

[追記]引き戻しに関しては、「リストモナドとテンソル空間モナドのあいだの準同型射 // モナドを随伴系に沿って引き戻す」に書いてありました。[/追記]

トラックバック - http://d.hatena.ne.jp/m-hiyama/20190116

2019-01-15 (火)

リストモナドとテンソル空間モナドのあいだの準同型射

| 11:20 | リストモナドとテンソル空間モナドのあいだの準同型射を含むブックマーク

異なる圏の上で定義された2つのモナドを比較したいことがあります。その目的に使える、“異なる圏上のモナドをつなぐ準同型射”は定義されています。そのようなモナド準同型射は一種類ではなくて、色々な定義があります。ここでは、一番扱いやすいと思われる、代数的モナド準同型射(クリメン/ソリヴェレスによる呼び名)の事例を出します。

集合圏Set上のリストモナドと、ベクトル空間の圏VectK上のテンソル空間モナドのあいだの、おそらくは一番素直な準同型射を構成します。

内容

  1. 動機と背景
  2. リストモナドとテンソル空間モナド
  3. モナドを随伴系に沿って引き戻
  4. リストモナドからテンソル空間モナドへの準同型射

動機と背景

モナドの形式論〈formal theory of monads〉を使うと、次の圏同値は比較的簡単に示せます。

  • 1MndAlg(K) ¥stackrel{¥sim}{=} 1MndEM-Alg(K)
  • 1MndAlg(K) ¥stackrel{¥sim}{=} (1MndKl-Alg(K))op

このことは、「最近のモナド論の概観と注意事項 1/2 // 参考文献と著者」で紹介した"クリメン/ソリヴェレス 2010"に書いてあります。

この圏同値に関わる具体例を提示するのがこの記事の動機/目的です。今日は、上記の圏同値自体は話題にしません。しかし、この記事の記号法が、"クリメン/ソリヴェレス 2010"と同じ記号法ではないので、現状僕が使っている記号の意味だけ簡単にメモしておきます。以下の箇条書きのなかで強調表示されている用語は「随伴に関する注意事項」で説明しています。Kは厳密2-圏だとします。

  • 1AdjL(K) : Kの対象を対象として、K内の随伴系〈adjunction | adjoint system〉を射とする1-圏。随伴系の左関手の方向を、1AdjL(K)の射(随伴系)の方向とする。左下の'1'は1-圏であることを示し、右下の'L'は左関手の方向を使うことを意味する。
  • MndOn(K)[A] : A∈|K| として、A上のモナドmonad on A〉を対象として、モナドのあいだの代数的準同型射〈algebraic homomorphism〉を射とする圏。代数的準同型射とは、モナドをモノイドとみなしてのモノイド準同型射のこと。
  • MndOn(K)[-] : 1AdjL(K) をインデックス付けベース圏〈indexing category〉とするインデックス付き圏〈indexed category〉。対象Aに対する値はMndOn(K)[A]で、AからBへの随伴により誘導される関手 MndOn(K)[B]→MndOn(K)[A] をリインデキシング関手とする。
  • Flatten(MndOn(K)[-]) : インデックス付き圏MndOn(K)[-]のグロタンディーク平坦化〈グロタンディーク構成〉。
  • 1MndAlg(K) : K内のモナドとそのあいだの代数的準同型射からなる圏。1MndAlg(K) := Flatten(MndOn(K)[-]) と定義する。
  • 1MndEM(K) : K内のモナドとそのあいだのアイレンベルク/ムーア型の準同型射からなる1-圏。アイレンベルク/ムーア型の準同型射については、"クリメン/ソリヴェレス 2010"参照。
  • 1MndKl(K) : K内のモナドとそのあいだのクライスリ型の準同型射からなる1-圏。クライスリ型の準同型射については、"クリメン/ソリヴェレス 2010"参照。
  • 1MndEM-Alg(K) : 1MndEM(K)の部分圏で、モナドの準同型射の台関手が右可随伴である(台関手が随伴系の左関手になる)準同型射だけからなる圏。
  • 1MndKl-Alg(K) : 1MndKl(K)の部分圏で、モナドの準同型射の台関手が左可随伴である(台関手が随伴系の右関手になる)準同型射だけからなる圏。

二番目の圏同値 1MndAlg(K) ¥stackrel{¥sim}{=} (1MndKl-Alg(K))op の右辺が反対圏になってますが、定義の仕方によっては、右肩のopは不要です。MndやAdjでは、誰が見ても明らかな射の方向はないので、射の方向は完全に恣意的(まったく無根拠に決める)ことになります。よって、opが付く/付かないも最初の(恣意的な)定義に依存します。定義の仕方は、著者/論文ごとにバラバラです。

厳密2-圏KとしてCATを選びます。CATは、必ずしも小さくない圏の2-圏です。Set∈|CAT| なので、Set上のモナドも扱えます。以下で扱う事例とは、1MndAlg(CAT) = Flatten(MndOn(CAT)[-]) の典型的な射をひとつだけ取り出して説明します。それは、Set上のリストモナドと、VectK上のテンソル空間モナドのあいだのモナド準同型射です。

リストモナドとテンソル空間モナド

モナドを表すのに、記号の乱用をして M = (M, η, μ) のように書きます。文字'M'をモナドとその台関手の両方の意味でオーバーロード〈多義的使用〉します。別なモナドNでも、単位ηと乗法μは同じ文字を使って N = (N, η, μ) と書きます。紛らわしいときは、N = (N, ηN, μN) とします。モナドが乗っている圏を明示したいときは、M = (M, η, μ) on C とします。台圏Cまで明示すれば、次のことが分かります。

  • M:CC in CAT
  • η::IdC⇒M:CC in CAT
  • μ::M*M⇒M:CC in CAT ('*'は関手の図式順結合)

リストモナド List = (List, η, μ) on Set は、最も有名なモナドと言っていいでしょう。リストモナドは、自由-忘却スタイルの随伴対に分解〈factorize〉できます。Monをモノイドの圏として:

  • 自由モノイド生成関手 FreeMon:SetMon in CAT
  • 台集合をとる忘却関手 U:MonSet in CAT

これらは随伴系 (η, ε: FreeMon -| U, FreeMon:SetMon) を構成します(随伴系の書き方については、「随伴に関する注意事項 // 随伴系の方向」参照)。Listは List = FreeMon*U と書けます。ここで、'*'は図式順の関手結合です。

Kを体として、K上のベクトル空間の圏をVectKとします。そして、K上の多元環の圏をAlgKとします。「多元環」とは、"algebra"に対する古い訳語で、いまどき「多元環」を使う人も少ないでしょうが、僕は「代数」より「多元環」をよく使います*1VectKAlgKのあいだの次の関手を考えます。

  • 自由多元環生成関手 FreeAlg:VectKAlgK in CAT
  • 台ベクトル空間をとる忘却関手 U:AlgKVectK in CAT

忘却関手を表す文字Uはオーバーロードしています。これらは随伴系 (η, ε: FreeAlg -| U, FreeAlg:VectKAlgK) を構成します。FreeAlg*U:VectKVectKモナドの台関手になります。

V∈|VectK| に対して、FreeAlg(V)は、Vのテンソル多元環〈tensor algebra〉とも呼ばれます。U(FreeAlg(V))は、テンソル多元環の掛け算を忘れたベクトル空間になるので、Vのテンソル空間と呼びましょう。Tens = FreeAlg*U と置いて、Tens = (Tens, η, μ) on VectKモナドになります。このモナドを、テンソル空間モナド〈tensor-space monad〉と呼びます。

Set上のリストモナドListと、VectK上のテンソル空間モナドTensは、作り方も雰囲気も似てます。無関係とは考えにくいですね。リストモナドとテンソル空間モナドを結ぶモナドの準同型射があって然るべきでしょう。

モナドを随伴系に沿って引き戻す

リストモナドListはSet上にあり、テンソル空間モナドTensはVectK上にあります。台となる圏が違っています。このため、異なる台圏を結ぶ算段が必要になります。

ところで、同じ台圏上のモナドのあいだの準同型射はどう定義されるのでしょうか。色々な定義があり得ますが、一番簡単なのは、モノイド準同型射として定義することでしょう。モノイド準同型射は、モノイドの単位と乗法〈積〉写像を保存する写像です。同様に、モナドの単位自然変換と乗法自然変換を保存する自然変換として、モナド間の準同型射を定義します。

2つのモナド (M, η, μ), (N, η, μ) on C に対して、自然変換 φ::M⇒N:CC が次の等式条件(の絵)を満たすときに、φはモナド準同型射です。

ここで、黒三角がη、黒丸がμです。

例えば、Maybe = (Maybe, η, μ) on Set から List = (List, η, μ) on Set へのモナド準同型として、自然変換φを次のように定義してみます。

  • For A in Set, φA:Myabe(A)→List(A) in Set,
    φA(a) := [a] if a∈A,
    φA(⊥) := []

ここで、[a] はシングルトンリスト、⊥はMaybeで追加した要素、[] は空リストです。φの自然性はすぐに示せるので、φはモナドMaybeをモナドListに埋め込む準同型射になります。このことは次のように書けます。

  • φ:Maybe→List in MndOn(CAT)[Set]

MndOn(CAT)[Set] は、CAT内でSet上に居るモナド達からなる圏です。

テンソル空間モナドSet上に居ないので、Set上に“移動”させます。移動の手段として、SetVectKのあいだの随伴系を使います。SetVectKのあいだには、典型的な自由-忘却スタイルの随伴系があります。それは:

  • (η, ε: FreeVect -| U, FreeVect:SetVectK)

ここで、文字'η'がモナドの単位とオーバーロードされていて、文字'U'も毎回オーバーロードですが、文脈で区別してください。

一般論として、随伴系 (η, ε: F -| U, F:CD) があると、D上のモナド N = (N, η, μ) on DC上に移動(引き戻し)できます。移動後のモナドを N' = (N', η', μ') on C とすると:

  • N' := F*N*U :CC
  • η' := η;(F*ηN*U) ::IdC⇒N':CC
  • μ' := (F*N*ε*N*U);(F*μ*U) ::N'*N'⇒N':CC

ここで、ηは随伴系の単位で、ηNモナドの単位です。'*'は関手の図式順結合および関手と自然変換のヒゲ結合で、';'は自然変換の図式順縦結合です。η'とμ'を絵(ストリング図)で描けば:

絵において、黒三角はモナドのηNで、黒丸は随伴のη, εとモナドのμです。圏D(を表す領域)をピンクに塗っています。

N' = (N', η', μ') on C が結合律と左単位律、右単位律を満たすことは絵算を使えば簡単に示せます。

VectK上のモナド Tens = (Tens, η, μ) をSet上に移動(引き戻し)する場合は:

  • Tens' := FreeVect*Tens*U:SetSet
  • η' := η;(FreeVect*ηTens*U)::IdSet⇒Tens':SetSet
  • μ' := (FreeVect*Tens*ε*Tens*U);(FreeVect*μ*U)::Tens'*Tens'⇒Tens':SetSet

Tens' = (Tens', η', μ') はSet上のモナドであり、もとのTensのSet上の代理となります。

リストモナドからテンソル空間モナドへの準同型射

リストモナドListからテンソル空間モナドTensへの準同型射は、次のように定義します; まず、Tensの代理としてのTens'をSet上に構成し、Set上の準同型 φ:List→Tens' in MndOn(CAT)[Set] を List→Tens の準同型射とします。φは、次の絵のような感じです。圏VectKを表す領域はピンクに塗ってあります。

集合Aに対して、自然変換φのA-成分は。

  • φA:List(A)→U(Tens(FreeVect(A)))

となります。U(Tens(FreeVect(A))) をもう少しわかりやすく記述しましょう。U(Tens(FreeVect(A))) は、なんだかんだで(詳細割愛)、集合Aの要素を不定元とするK係数非可換多項式全体の集合になります。K係数非可換多項式全体の集合を NCPolyK(A) とすれば、

  • U(Tens(FreeVect(A))) ¥stackrel{¥sim}{=} NCPolyK(A)

この同型はイコールとみなしてしまっていいでしょう。

a = [a1, ..., an] ∈ List(A) とすると、φA(a) は次のように与えられます。

  • φA:List(A)→NCPolyK(A) in Set
  • φA(a) := a1 ... an (すべて並べる)
  • φA([]) := 1

a1 ... an はリストの要素をすべて並べて掛け合わせた単項式で、NCPolyK(A) の要素とみなします。

このように定義したφが、Set上のモナド準同型射となるのは、φがモノイド準同型射で、単位と乗法を保つときです。絵で描けば:

これらを確認するのは、定義を追いかけるルーチンな作業です。ルーチンとは言え、具体的な計算はなかなか面倒なので、別な記事にするかも知れません。


冒頭で述べたように、モノイドの形式論からは、かなり抽象度の高い定理が得られます。具体的な感触を得るために実例が欲しいわけですが、その具体的の構成もけっこうめんどくさかったりします。今回の実例は、1MndAlg(CAT) 内の射をひとつだけ構成したのでした。その射が φ:(List on Set)→(Tens on VectK) in 1MndAlg(CAT) です。

φの周辺には、Set, Mon, VectK, AlgK という4つの圏(CATおよび1AdjL(CAT)の対象)があり、それらは随伴系(1AdjL(CAT)の射)で結ばれています。この四角形(対角線付き)は、事例としてなかなか面白いと思います。

*1:"algebra"はすべて「多元環」にするわけじゃないです。例えば、"Boolean algebra"は「ブール多元環」じゃなくて「ブール代数」です。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20190115

2019-01-12 (土)

2-豊饒圏と繰り返し豊饒圏

| 11:00 | 2-豊饒圏と繰り返し豊饒圏を含むブックマーク

昨日「2-豊饒圏」という記事を書きました。これは、「思い付きを忘れないうちに書いた」ものです。確認したり調べたりの作業はしてません。

とりあえず、「類似の概念を誰かが定義しているだろう」と思って調べたら … ない。あれっ? 意味のある概念なら何かしら既存の資料があるでしょうに、それがない … ということは無意味だったのか?

どうも、通常の豊饒圏論のなかで、2-豊饒圏と同じものは構成できそうです。その点からは無意味だったかも知れません。が、昨日の記事の冒頭で述べたような動機だと、2-豊饒圏のほうが使いやすそうです。使い勝手からは、無意味でもないでしょう。


2-豊饒圏」で述べたような、モノイド圏Vで2-豊饒化した圏を、V-2-圏V-2-category〉とも呼び、その全体をV-2-Catとします。

V-2-Catは、圏(1-圏)と考えます。その対象は、もちろん(小さな)V-2-圏です。射は、V-2-関手V-2-functor〉です。V-2-関手は、通常の関手と、ホムV-圏ごとのV-関手の族をうまいこと組み合わせて定義できるでしょう。(V-圏はV-豊饒圏のこと、V-関手はV-豊饒関手のことです。)

ちょっと考えただけですが、圏V-2-Catは、どうやら、圏(V-Cat)-Catと同じものだったようです。(V-Cat)-Catは、モノイド圏V-Catで豊饒化された圏の圏です。「豊饒圏の圏で豊饒化した豊饒圏の圏」です。あー、ヤヤコシイ。豊饒化を繰り返しているので、繰り返し豊饒圏〈iterated enriched category〉と呼んでおきましょう(別な名前が既にありそうだけど)。

まず、モノイド圏としてのV-Catについてザッと述べましょう。V = (V, ¥otimes, I, α, λ, ρ) は豊饒化ベース圏として、V-Catの対象は、(小さな)V-豊饒圏です。V-Catの対象であるV-豊饒圏は、C, Dなどの(斜体でない)文字で表します。

V-Catの射は、V-豊饒圏のあいだのV-豊饒関手V-enriched functor〉だとします。豊饒関手については、nLab項目を参照してください。

V-Catは通常の圏になりますが、モノイド構造も入れましょう。V-Catのモノイド積と単位対象は、¥odot, J とします。

C, D∈V-Cat として、それらのホム対象は、C(a, b), D(a', b') のように書きます。|D|の要素にダッシュ〈プライム〉を付けることにします。

C¥odotDを定義したいのですが、まず、対象集合は

  • |C¥odotD| := |C|×|D|

です。ここで、C¥odotD の'¥odot'は新しく定義するモノイド積の記号で、|C|×|D| の'×'は集合の直積の記号です。

次にホム対象の定義:

  • (C¥odotD)((a, a'), (b, b')) := C(a, b)¥otimesD(a', b')

結合を与える射の族は次のように定義します。

  • δ(a, a'), (b, b'), (c, c'):(C¥odotD)((a, a'), (b, b'))¥otimes(C¥odotD)((b, b'), (c, c'))→(C¥odotD)((a, a'), (c, c')) in V
    δ(a, a'), (b, b'), (c, c') := γa,b,c¥otimesγ'a',b',c'

ここで、δが定義すべき族で、γがCの結合、γ'がDの結合です。対象集合の定義を考慮すると、δはwell-definedになります。

C¥odotDの恒等は次のようです。

  • τ(a, a'):I→(C¥odotD)((a, a'), (a, a')) in V
    τ(a, a') := λI-1;(ιa¥otimesι'a')

ここで、τが定義すべき族で、ιがCの恒等、ι'がDの恒等です。λIは I¥otimesI→I in V という同型射です。λI = ρI なのですが、これの証明は難しいです。

最後に、単位対象 J∈|V-Cat| を定義します。

  • |J| := {0}
  • J(0, 0) := I
  • γ0,0:J(0, 0)¥otimesJ(0, 0)→J(0, 0) in V
    J(0, 0) := λI
  • ι0:I→J(0, 0) in V
    ι0 := idI

これで、モノイド圏 V-Cat = (V-Cat, ¥odot, J) の素材は揃いました。が、V-Catにおける結合律子α, 左単位律子λ, 右単位律子ρと、それらが従う法則を示さないといけません。めんどくさいけど、頑張ればできるでしょう。

V-Catがモノイド圏であることがわかれば、決まりきった手順で (V-Cat)-Cat を構成できます。(V-Cat)-Cat の射は豊饒関手です。豊饒自然変換(2-射)までは考えないで、(V-Cat)-Catは1-圏とします。

この状況で次の圏同値が成立するはずです(ちゃんと確認してないけど明らかに思える(苦笑*1))。

  • V-2-Cat ¥stackrel{¥sim}{=} (V-Cat)-Cat

*1:明らかに思えたが実は違っていた、ってこともあるので、細部までちゃんとやらないとダメなんですが、細部がめんどくさい。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20190112

2019-01-11 (金)

2-豊饒圏

| 17:22 | 2-豊饒圏を含むブックマーク

2種類以上の、異なったタイプの“計算”を組み合わせて使いたいとき、ある圏に対して高次の豊饒化を施すことで“組み合わせ”が実現できそうです。

内容:

  1. 動機
  2. 言葉に関する注意
  3. 1-豊饒圏
  4. 2-豊饒圏
  5. 事例
  6. 項計算と論理計算

動機

なんか思い付きを記録するとき、動機を書かないと、後で「なんでこんなこと考えたんだ?」ってなります。なので、きっかけと動機を書きます。

確かマイク・ステイ〈Mike Stay〉(とお仲間達)が、"computational calculus"って言葉を使っていて、「翻訳に困るなー」と思ったことがあります。"computational calculus"は、「コンピュータを使った解析学」という意味もあるようですが、ステイ達は、

  • "computational calculus" vs. "logical calculus"

という文脈で使っています。

論理では、論理式やシーケントを対象とした計算をしますが、これが"logical calculus"です。普通に「論理計算」と訳せばいいですね。それに対して、数の計算や式の計算が"computational calculus"です。「計算計算」じゃ酷いし、意味的に「コンピュータ計算」ではないし…。論理では、数や式(論理式ではない式)を「項」と呼ぶので、「項計算」としておきます。この訳語を使うと:

  • 項計算 vs. 論理計算

項計算も論理計算も、圏論的定式化ができます。が、項計算と論理計算の境界線がよくわからないのです。境界線は恣意的なのかも知れません。そうだとしても、境界線を表現する方法があったほうがいい気がします。

そこで、項計算を行う圏の上に、論理計算を行うレイヤーを豊饒化〈enrichment〉により乗っける、と考えてはどうかな、と思ったのです。

言葉に関する注意

「ほうじょう」の漢字表記には、「豊饒」と「豊穣」があります。稲などが豊かに実るイメージの「豊穣」のほうがふさわしそうですが、行きがかり上「豊饒」を使い続けます。

"enriched category"は「豊饒圏」、"enriching category"は「豊饒化ベース圏」または「豊饒化圏」とします。"V-enriched category"は「V-豊饒圏」です。

1-豊饒圏

豊饒圏の定義を思い出しましょう。豊饒圏を作るための素材は、集合Xとモノイド圏Vです。a, b∈X ごとに、ホム対象〈hom-object | homobject〉 hom(a, b) を対応させる写像

  • hom:X×X→|V|

と、結合を与える射の族

  • For a, b, c∈X,
    γa,b,c:hom(a, b)¥otimeshom(b, c)→hom(a, c) in V

があって、結合律、左右の単位律を満たすとき、豊饒圏が定義されます。より詳しくは、次の記事達を参照してください。

豊饒圏の定義をみると、対象は通常の集合を使っています。射の概念は通常の圏論とは違って、ホム対象により置き換えています。対象は次元0の射、普通の射は次元1の射とみなせるので:

  • 次元0の射の概念は、通常の集合論ベースの定義を使う。
  • 次元1の射の概念は、モノイド圏V内のホム対象として定義する。

次元1のところで豊饒化ベース圏Vが登場するので、通常の豊饒化を1-豊饒化〈1-enrichment〉と呼び、作られた豊饒圏は1-豊饒圏〈1-enriched category〉としましょう。あえて「1-」を付けたのは、「2-」とか「n-」を考える心づもりがあるからです。

2-豊饒圏

n-豊饒圏〈n-enriched category〉は、ある種のn-圏ですが、

  • 次元(n - 1)以下の射の概念は、通常の集合論ベースの定義を使う。
  • 次元nの射の概念は、モノイド圏V内のn-ホム対象として定義する。

任意のnに対する一般論は難しいので、n = 2 に限定します。つまり、次のような2-豊饒圏〈2-enriched category〉を扱います。

  • 次元1以下の射の概念は、通常の集合論ベースの定義を使う。
  • 次元2の射の概念は、モノイド圏V内の2-ホム対象として定義する。

Cを通常の圏〈ordinary category〉として、0-射(=対象)と1-射(=射)の概念は通常どおりとして、2-射の集合=2-ホムセットの代わりに、2-ホム対象〈2-homobject〉を考えます。2-射の結合に相当する概念も必要です。2-射の結合は縦結合と横結合の二種類があるので、2-ホム対象上の結合演算も二種類になります。

定義のために、言葉の準備をしましょう。f, g∈Mor(C) に対して、

  • fとgが共端 ⇔ dom(f) = dom(g) かつ cod(f) = cod(g)
  • fとgが(この順で)隣接 ⇔ cod(f) = dom(g)

共端は"parallel"〈平行〉といいますが、意訳してます。

Vはモノイド圏で、毎度の記号の乱用で V = (V, ¥otimes, I, α, λ, ρ) とします。このVが豊饒化ベース圏です。2-豊饒化〈2-enrichment〉(=2-豊饒圏の構成)の際に、結合律子α、左単位律子λ、右単位律子ρも考慮する必要があります。面倒なら、Vを厳密モノイド圏だとしてもかまいません。

さて、2-ホム対象 2-hom は、Mor(C)×Mor(C) から |V| への写像ですが、全域的には定義できません。共端な f, g に対してだけ 2-hom(f, g)∈|V| が定義されます。

  • 2-hom : {(f, g)∈Mor(C)×Mor(C)| fとgは共端} → |V|

fとgの共通のdom/codを A, B として、2-hom(f, g) = 2-hom(f, g:A, B) のように書くこともあります。

2-hom(f, g)が集合とは限らないので、2-hom(f, g)の要素という概念はないかも知れません。したがって、モノ(集合の要素)としての2-射という概念も保証はされません。ハッキリと在るのは、2-射ではなくて2-ホム対象だけです。この点は、通常の2-圏とは異なります。

2-ホム対象が定義されただけでは2-豊饒圏にはなりません。縦結合に相当するβと、横結合に相当するγが必要です。βもγも、Cの射でインデックスされたVの射の族です。ここでは、Cの図式順結合を'*'で書きます。

  • βf,g,h:2-hom(f, g)¥otimes2-hom(g, h)→2-hom(f, h) in V
  • γf,g,h,k:2-hom(f, g)¥otimes2-hom(h, k)→2-hom(f*h, g*k) in V

Cの射の両端(domとcod)も書いたほうが分かりやいかも知れません。

  • βf,g,h:2-hom(f, g:A, B)¥otimes2-hom(g, h:A, B)→2-hom(f, h:A, B) in V
  • γf,g,h,k:2-hom(f, g:A, B)¥otimes2-hom(h, k:B, C)→2-hom(f*h, g*k:A, C) in V

他に、恒等射に相当する族ι〈イオタ〉も必要です。

  • ιf:I→2-hom(f, f:A, B) in V

これらの族達が、結合律、単位律、交替律〈interchange law | exchange law〉を満たすことを要求します。法則の定義の際は、直積をモノイド積とする集合圏Setにより2-豊饒化された2-豊饒圏が、通常の厳密2-圏になるようにします。弱2-圏〈双圏〉を模倣する弱い定義もありますが、話が難しくなります。

事例

4種の豊饒化ベース圏を考えましょう。

B

集合{0, 1}に 0 < 1 と順序を入れます。順序集合からは圏を定義できるので、対象集合が{0, 1}である圏ができます。掛け算をモノイド積にすると、モノイド圏が出来上がります。こうして出来た厳密モノイド圏を B = (B, ・, 1) とします。

P

集合{x∈R| x ≧ 0}に通常の順序を考えます。順序集合からは圏を定義できるので、対象集合が{x∈R| x ≧ 0}である圏ができます。足し算をモノイド積にすると、モノイド圏が出来上がります。こうして出来た厳密モノイド圏を P = (P, +, 0) とします。

FdVect

適当な体Kを固定して、有限次元ベクトル空間の圏 FdVect = FdVectK を考えます。射は線形写像です。ベクトル空間および線形写像のテンソル積をモノイド積とすれば、モノイド圏になります。このモノイド圏を FdVect = (FdVect, ¥otimes, K, α, λ, ρ) とします。

Set

集合圏Setに直積を考えるとモノイド圏になります。このモノイド圏を Set = (Set, ×, 1, α, λ, ρ) とします。


適当な圏(普通の圏)Cに対して、Bで2-豊饒化すると、1-ホムセット(普通のホムセット)にプレ順序構造が入った圏ができます。プレ順序'≦'に関する不等式 f ≦ g が2-射に相当します。

CPで2-豊饒化すると、1-ホムセットに一般化距離が入った圏ができます。一般化距離とは、距離の公理から次の2つを除いたものです。

  • d(a, b) ならば a = b
  • d(a, b) = d(b, a)

つまり、距離ゼロでも異なる点を許します。そして、距離が対称である必要もありません。

CFdVectで2-豊饒化すると、1-ホムセットがK-線形圏の構造を持つような圏ができます。2-hom(f, g)∈|FdVect| なので、2-hom(f, g) はベクトル空間です。このベクトル空間の要素(=ベクトル)として2-射を考えることができます。2-射(=ベクトル)は、双線形写像で縦結合/横結合されます。

CSetで2-豊饒化すると、1-ホムセットが圏の構造を持つような圏ができます。2-hom(f, g) は集合です。この集合のの要素として2-射を考えることができます。これは通常の厳密2-圏です。

項計算と論理計算

冒頭の「動機」の話に戻ります。普通の圏Cのなかで、対象は型、射は項と解釈して項計算ができます。さらに、項に対する命題を考えて論理計算をしたいとしましょう。

1-射 f, g に対して、なにか不等式 f ≦ g (みたいなもの)を考えるとします。この不等式の真偽値(どの程度正しいか)を [f ≦ g] と書き、真偽値の値は圏Vの対象として定まるとします。この設定では、Vは真偽の程度と推論の圏だということになります。Vとして、モノイド圏とみなしたハイティング代数をとると適切かも知れません。

項計算の上に論理計算を乗っける、という操作が、通常の圏Cに対して、“真偽値の圏”で2-豊饒化することで実現されそうです。

前節の例には、論理とは無関係の例もあります。ということは、論理に限らず、異なる種類の計算を組み合わせるときに、2-豊饒化が使えそうです。厳密高次圏の定義では、集合圏ベースの豊饒化を繰り返しますが、使う豊饒化ベース圏を取っ替え引っ替えしながら豊饒化を繰り返すという操作があってもよさそうです。高次の混合豊饒化とでも呼ぶべき操作ですね。

マイク・ステイ達の議論では(記憶がおぼろげだが)、項計算と論理計算の定式化にモナドやベックの分配法則が出てきたような気がします。V-豊饒圏という概念がモナドとして定義できるなら、複合モナドが混合豊穣圏に対応し、複合モナドを作るための条件としてベックの分配法則も出てくるでしょう。

以上の話は、半分くらい予想で言っている(裏が取れてない)ので、確実性は乏しいですが、2以上のnに対する“V-n-豊饒圏”という概念は無意味ではないとは思います。

2019-01-08 (火)

最近のモナド論の概観と注意事項 2/2

| 18:18 | 最近のモナド論の概観と注意事項 2/2を含むブックマーク

最近のモナド論の概観と注意事項 1/2」の続きです。前回記事で導入した言葉や記号は、この記事でも使います。

内容:

  1. ところで、なんでモナド
  2. モナド論の主題:モナドと随伴系
  3. 色々な厳密2-圏内のモナドと随伴系
  4. モナドの2-随伴状況
  5. 2-随伴について
  6. その他の問題点や注意点

ところで、なんでモナド

昨年(2018年)の9月に「モナドはモノイドだが、モノイドじゃない」という記事を書きました。そのなかで:

2,3日前からn(不明)回目のマイ・モナドブームです。今回のブームのテーマは、「2-圏論からモナドを考える」です。キャッチフレーズは「モナドはモノイドじゃない」かな。

このブームは、諸般の事情で盛り上がることはありませんでした。が、くすぶり続けてはいて、昨年の年末になって「気になっていたことを調べよう」となったわけです。

僕がモナドに興味を持つ主たる理由は、プログラム構文論・意味論を記述する手段としてです。プログラム構文論・意味論では、さまざまな場面で、さまざまな形で、モナドまたはモナド類似物〈monad-like entity〉がたびたび登場します。

そのテの事例を僕はある程度は知っているのですが、事例に出会うたびに泥縄式にゴニョゴニョ調べているわけで、どうも系統的に理解している気がしない。なので、高次圏を使ったフォーミュレーションから、包括的に把握したいな、と思うのですよ。

現状では、高次圏ベースのモナド論のサワリを理解しただけです。それでも、チラリと見えた景観と、自分が戸惑ったところを(主に自分のために)記録しておきます。

モナド論の主題:モナドと随伴系

モナド論の主題は、モナドmonad〉と随伴系〈adjunction | adjoint system〉だと言っていいでしょう。モナドの全体をMnd、随伴系の全体をAdjと書きます。今言った「…の全体」は曖昧で雰囲気的ですが、とりあえずはモンヤリとした話をします。

随伴系からモナドが作られることはよく知られています。随伴系からモナドを作る構成を mnd:Adj→Mnd とします。逆に「モナドを随伴系に分解〈factorize〉できるか?」という問題があります。この問題の解(分解)の存在は、一般的には保証されませんが、古典的非形式論(つまり、CatCATでの議論)では解が存在します。しかし、一意的ではありません。典型的な解(分解)としては、アイレンベルク/ムーア構成〈Eilenberg-Moore construction〉とクライスリ構成〈Kleisli construction〉があります。これらを(存在すると仮定して)、emadj:Mnd→Adj, kladj:Mnd→Adj とします。

今、非常に曖昧に述べた Mnd, Adj, mnd, emadj, kladj を細部までキッチリと定義して、その相互関係を調べることが“モナドの基本理論”でやるべきことです。

形式モナド論では、モナドと随伴系が棲む場所として、抽象的な厳密2-圏Kを想定します。Mnd, Adj は、厳密2-圏Kをパラメータにして、

  • Mnd(K) : K内のモナドの全体
  • Adj(K) : K内の随伴系の全体

となります。パラメータKは、mnd, emadj, kladj にも付くので:

  • mndK:Adj(K)→Mnd(K)
  • emadjK:Mnd(K)→Adj(K)
  • kladjK:Mnd(K)→Adj(K)

mndKは任意の厳密2-圏Kに対して定義可能ですが、emadjK, kladjK が存在する(定義できる)ことは保証されません。厳密2-圏Kが、emadjKを持つとき、アイレンベルク/ムーア構成を許容する〈admitting Eilenberg-Moore construction〉と言います。同様に、kladjKを持つならクライスリ構成を許容する〈admitting Kleisli construction〉と言います。

アイレンベルク/ムーア構成とクライスリ構成は、厳密2-圏論のなかで形式的に定義できるので、「アイレンベルク/クライスリ構成を許す/クライスリ構成を許す」は厳密2-圏が持つ性質とみなせます。つまり、次のような単項述語 admitsEilenberg-MooreConstruction, admitsKleisliConstruction が定義できます。

  • For K in s2-Cat#r, admitsEilenberg-MooreConstruction(K) := ナニヤラカニヤラ
  • For K in s2-Cat#r, admitsKleisliConstruction(K) := ナニヤラカニヤラ

s2-Cat#rは3-圏ですが、admitsEilenberg-MooreConstruction(K) である対象Kの全体 {K∈Obj(s2-Cat#r) | admitsEilenberg-MooreConstruction(K)}を対象集合にして、充満部分3-圏を作れるので、それを s2-CatEM#r と書きます。同様に、クライスリ構成を許容する厳密2-圏からなる3-圏は s2-CatKl#r と書きます。

K in s2-CatEM#r ならば、emadjK:Mnd(K)→Adj(K) を使ってよく、K in s2-CatKl#r ならば、kladjK:Mnd(K)→Adj(K) を使っていいわけです。K in s2-CatEM-Kl#r = s2-CatEM#rs2-CatKl#r ならば、K内で古典的非形式論のかなり部分を再現できます。

色々な厳密2-圏内のモナドと随伴系

モナドの全体と随伴系の全体は、厳密2-圏Kをパラメータにして、Mnd(K), Adj(K) と書くのでした。圏の圏Catは、自然変換まで考えれば厳密2-圏(Cat in s2-CAT)なので、K = Cat として、Mnd(Cat), Adj(Cat) を考えることができます。これは、非形式大域モナド論となります。

集合圏Setは、モナドの台圏〈基礎圏〉としてよく使われます。Set in Cat ではなく、Set in CATCAT = Cat#1)なので、(Set = 0-Cat#0) in (CAT = 1-Cat#1) in s2-Cat#2 という系列のなかで考えることになります。Mnd(CAT), Adj(CAT) を扱う非形式大域モナド論のなかで、Set in CAT を台圏として固定した局所モナド論が、Set上のモナド論になります。もちろん、Set特有の性質を使って、一般論だけでは無理な細かい議論が出来ます。

厳密2圏は、CatCAT以外にも色々あります。「モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き) // 2-圏の例 10選」で10個の例を挙げてあります(非厳密2-圏も含まれます)。いくつかの厳密2-圏に関して、Mnd(K)とAdj(K)を考えてみます。Mnd(K)もAdj(K)も、高次の圏的構造〈higher categorical structure〉を持ちます(持たせることが出来ます)が、その対象部分(0Mnd(K), 0Adj(K) と書く)だけを述べます。

順序集合の圏 Ord

厳密2-圏としてのOrdに関しては、「モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き) // 2-圏の例 10選」を見てください。

Aが順序集合、f:A→A が自己単調写像で、f;f≦f, idA≦f を満たすとき(順序に関する)閉包作用素〈closure operator〉と呼びます(位相に関する閉包作用素とは違います)。(A, f, f;f≦f, idA≦f) はOrd内のモナドになるので:

  • 0Mnd(Ord) = (閉包作用素の全体)

Ord内の随伴系がガロア接続〈Galois connection〉であることはよく知られています。

  • 0Adj(Ord) = (ガロア接続の全体)

Ord内のモナド/随伴系に関することは次の記事にも書いてあります。

関係の圏 Rel

厳密2-圏としてのRelに関しては、「モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き) // 2-圏の例 10選」を見てください。

Aが集合、R:A→A がA上の(二項)関係で、R;R⊆R, ΔA⊆R (ΔA := {(x, y)∈A×A| x = y})を満たすとき、RはA上のプレ順序関係(推移的・反射的関係)です。(A, R, R;R⊆R, ΔA⊆R) はRel内のモナドになるので:

  • 0Mnd(Rel) = (プレ順序関係の全体)

Rel内の随伴系は、次のような関係のペア (R, S) です。

  • R:A→B, S:B→A in Rel
  • ΔA⊆R;S
  • S;R⊆ΔB

興味深いのは、S = Rt(Rtは、関係Rの転置、(x, y)∈R ⇔ (y, x)∈Rt)としたとき、

  • ΔA⊆R;Rt は、Rが全域〈total〉であることを表す。
  • Rt;R⊆ΔB は、Rが単葉〈univalent | 一価〉であることを表す。

(R, Rt)という形の随伴系とは、全域かつ単葉であるRのことなので、Rは写像と同一視できて、

  • ((R, Rt)という形の随伴系の全体) = (写像の全体)

となります。

スパンの圏 Span(C)

ファイバー積〈引き戻し〉が存在する圏Cに対して、そのスパンの圏はSPAN(C)と書きます。SPAN(C)は厳密2-圏にはなりません。ホムセットに同値関係を入れて商集合をとると厳密2-圏になります。これをSpan(C)と書きます。次の記事を参照してください。

商集合をとった後のホムセットが(考えている宇宙のなかで)小さくなるかはアヤシイです。

ホムセットのサイズは気にしないことにすれば、Span(C)は厳密2-圏となります。Span(C)内のモナドは、圏C内部圏〈internal category〉(の同値類)になります。内部圏については、nLab項目を参照してください。

  • 0Adj(Span(C)) = (Cの内部圏の全体)

通常の圏〈ordinary category〉は、Setの内部圏なので、0Adj(Span(Set))は、通常の圏の全体になります。

0Adj(Span(C))も機械的に定義できますが、0Adj(Span(C))の要素が既存の構造なのかどうか? 僕は知りません。

いずれにしても、Span(C)におけるモナド論は、C-内部圏論のひとつの形を提示すると思われます。厳密2-圏ではなくて、弱2-圏ベースで考えてみたのが「モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き)」の内容です。

モナドの2-随伴状況

厳密2-圏Kに対するMnd(K)とAdj(K)には、さまざまな圏的構造を入れることができます。そのなかでも一番便利そうなのは、Mnd(K)にもAdj(K)にも厳密2-圏の構造を入れる場合でしょう。

厳密2-圏の構造が入ったMnd(K)とAdj(K)を、s2Mnd(K), s2Adj(K) と書くことにします。Kも厳密2-圏だったので、

  • K, s2Mnd(K), s2Adj(K) in s2-Cat#r

宇宙の階数rは目的により適当に決めますが、話を簡単にするため、以下 r = 0 として階数は省略します。

s2Mnd(K), s2Adj(K) 以外に、s2Idをs2-Cat上の恒等関手として、

  • s2Id(K) = K

とします。

s2Id(K), s2Mnd(K), s2Adj(K) はいずれもs2-Catのなかに居ますが、これらは2-随伴状況〈{2-bi}{adjoint | adjunction} {situation | context}〉を形成しています。2-随伴状況とは、「背後には2-随伴系があるぞ」という程度の割と漠然とした意味です。2-随伴系の定義は安定していません(次節)。

2-随伴状況をより正確に言うには、MndとAdjにさらに修飾が付くのですが、修飾の説明はせずにとりあえず結果だけを言うと:

  • K in s2-CatEM に対する s2RAdjL(K) と s2MndEM(K) のあいだに、アイレンベルク/ムーア・2-随伴ペア〈Eilenberg-Moore 2-adjoint pair〉が存在する。
    • 左2-関手 mndK: s2RAdjL(K) → s2MndEM(K)
    • 右2-関手 emadjK: s2MndEM(K) → s2RAdjL(K)
  • K in s2-CatKl に対する s2MndKl(K) と s2LAdjL(K) のあいだに、クライスリ・2-随伴ペア〈Kleisli 2-adjoint pair〉が存在する。
    • 左2-関手 kladjK: s2MndKl(K) → s2LAdjL(K)
    • 右2-関手 mndK: s2LAdjL(K) → s2MndKl(K)

前回紹介した"バスケス-マルケス 2015"(https://arxiv.org/abs/1510.04724)は、これらの2-随伴状況を解説しています。ただし、使っている記号が違うので、対応を示します。

檜山 バスケス-マルケス
s2RAdjL(K) AdjR(K)
s2MndEM(K) Mnd(K)
mndK (EMの) ΦE
emadjK ΨE
s2MndKl(K) Mnd(K)
s2LAdjL(K) AdjL(K)
kladjK ΨK
mndK (Klの) ΦK

MndEM, MndKl という書き方は"クリメン/ソリヴェレス 2010"(https://www.uv.es/~solivere/Articles/Kleisli%20and%20Eilenberg-Moore%20constructions%20as%20parts%20of%20biadjoint%20situations.pdf)に倣いました。RAdjLといった書き方は次の論文から採りました*1

MndとIdのあいだにも2-随伴状況があります。こちらは、2-随伴ペアではなくて、2-随伴トリオになります。Mnd-Idの2-随伴トリオについては、"ザワドウスキ 2010"(https://arxiv.org/abs/1012.0547)に簡単な記述があります。バスケス-マルケスのMndを、ザワドウスキはMndopと書いており、これは"ブーム 2018"(https://arxiv.org/abs/1810.11300)が使っている水平方向の反対圏の記法と同じです。記法は人により全くバラバラなので、注意が必要です。

2-随伴について

Id(K) = K, Mnd(K), Adj(K) などは、厳密2-圏とみなすことができて、それらのあいだに2-随伴状況/2-随伴系があります。しかし、2-随伴〈2-adjunction | 2-adjoint system〉の定義は安定していません。

nLab項目"2-adjunction"によると:

A 2-adjunction is a common name for various kinds of adjunctions in 2-category theory; not only adjunctions between 2-categories themselves, but more generally adjunctions within an arbitrary 3-category.


2-随伴とは、2-圏論におけるさまざまな種類の随伴に対する総称的な呼び名である。2-圏のあいだの具体的随伴だけでなく、任意の3-圏内のより一般的随伴概念もある。

単に「2-随伴」といっただけでは、さまざまな種類の随伴概念のどれかを示す、というだけでハッキリはしません。「2-圏のあいだの具体的随伴」とは、今話題にしているような、K, L in s2-Cat の2-随伴のことです。これを形式化すると、3-圏の対象 K, L in T, T in ?3-Cat に対する2-随伴が定義できる、ということです。

nLabによると、現在提案されている2-随伴は:

  1. 厳密2-随伴〈strict 2-adjuncation〉
  2. 双随伴〈biadjunction〉
  3. 疑随伴〈pseudoadjunction〉
  4. ラックス2-随伴〈lax 2-adjunction〉

厳密2-圏のあいだのアイレンベルク/ムーア・2-随伴とクライスリ・2-随伴に関しては、厳密2-随伴で足りるような気がします(ちょっと自信がないが)。しかし、アイレンベルク/ムーア構成とクライスリ構成の背後には、もっと高次で大規模な随伴構造が存在しているような気もします。

MndとIdのあいだには随伴トリオが存在しますが、随伴トリオをチャンと扱うには多項随伴系〈multivariable adjunctions〉が必要かも知れません。多項随伴系の2次元版、つまり、多項・2-随伴系も存在しているはずです。

モナドと随伴を調べるのに、高次(2次元以上)のモナドと随伴が必要になる -- ここでもマイクロコスモ原理が働いているようです。

その他の問題点や注意点

前節で、随伴の圏Adjは厳密2-圏 s2Adj(K) とみなせると言いました。しかし、Adjを厳密二重圏〈strict double category〉とみなすほうが都合がいいこともあります。厳密二重圏とみなした随伴の圏を sdAdj(K) としましょう。

厳密2-圏 s2Adj(K) と 厳密二重圏 sdAdj(K) は、とりあえずは別物で、関連性は明らかではありません。これらを統合するには、3-圏 sc3Adj(K) を導入するとよさそうです。前置プレフィックスの"sc3"は厳密柱状3-圏〈strict cylindrical 3-category〉のつもりです。

今、厳密柱状3-圏 sc3Adj(K) についてこれ以上述べませんが、厳密2-圏 s2Adj(K) も厳密二重圏 sdAdj(K) も、厳密柱状3-圏 sc3Adj(K) から取り出すことができます。

随伴とモナドを取り扱うとき、留意すべき概念に、

  • メイト
  • 反対圏

があります。

メイトは、随伴系におけるホムセット同型 D(F(A), Y) ¥stackrel{¥sim}{=} C(A, G(Y)) を拡張した概念で、自然変換の集合のあいだのメイト対応(同型)を通じて「互いにメイト」という関係が定義できます。s2Adj(K), dAdj(K) の構成のときには、メイトが必須です。

AdjもMndも厳密2-圏Kをもとに作られ、それ自身が厳密2-圏になります。しばしば2-圏の反対圏を考えます。とはいえ、2次元以上の圏では、方向がニ方向以上あるので、“どの方向に対して反対か”に注意する必要があります。「高次圏の反対圏をどう書くか」でブーム〈Gabriella Böhm〉の書き方を紹介しましたが、他に色々な書き方があります。よく確認しないと混乱します。


アイレンベルク/ムーア構成とクライスリ構成に関わる2-随伴状況や、厳密二重圏/厳密柱状3-圏としてのAdjなど、その詳細は述べられませんでしたし、述べるにはけっこうな準備も必要です。マイ・モナドブームがゆるやかに続くなら、さらに続きがあるかも知れません。

*1:元の論文では、下付きのLはデフォルトなので省略して書かないのですが、デフォルトと省略は諸悪の根源なので書くことにします。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20190108

2018-12-30 (日)

随伴に関する注意事項

| 14:54 | 随伴に関する注意事項を含むブックマーク

最近のモナド論の概観と注意事項 1/2」より:

タイトルに「1/2」を付けているので、もう一回続きを書く予定でいます(たぶん来年だろうが)。次回は、モナド論の中心的なトピックとか、事前に知っておくとよさそうな予備知識とか、誤解・勘違いしそうな所について書きます。

2/2は来年ですが、注意事項のひとつを取り出して今年最後の記事にします。

内容:

  1. 随伴系の方向
  2. 随伴に関わる曖昧な言葉と明確化
  3. 構造か命題か

随伴系の方向

圏論の随伴をちゃんと抑えよう」より:

上下左右をきちんと区別しないと話がワヤクチャになる典型的な例に、随伴〈adjoint, adjunction〉の定義があります。僕も「どっちが右だっけ?」「域だっけ、余域だっけ?」「εって、単位? それとも余単位?」とか、ねんじゅう迷っています。

随伴系には、さまざまな“方向”が出てきます。随伴系自体が方向を持つ(持たせたい)のですが、その基準は特になく、著者・場面ごとにバラバラです。ホントに頭が痛いわ!

随伴系の書き方」で、次のような随伴系の書き方を紹介しました。(http://www.tac.mta.ca/tac/volumes/29/31/29-31.pdf

このまま採用するのは難しいので:

ただし、逆ターンスタイルにη, εを埋め込んだ記号を使うのは難しいので、代替案としては次のようかな。

  • (η, ε): F -| G :DC

僕が出したこの書き方 (η, ε): F -| G :DC とほぼ同じ書き方をしている例を見つけました。(http://www.cs.cornell.edu/courses/cs6117/2018sp/Lectures/Adjunctions.pdf

今出した例では、随伴系の方向は、ペアの右の関手と同じ方向にしています。しかし、誰でもいつでもそうするとは限りません。「随伴系の書き方」で反対方向を採用する例も出しました。(http://www.math.uchicago.edu/~may/VIGRE/VIGRE2007/REUPapers/FINALAPP/Anderson.pdf

最近のモナド論の概観と注意事項 1/2」で紹介した"バスケス-マルケス 2015"(https://arxiv.org/abs/1510.04724)では、次のような注意書きがあります("of"が抜けているようなので追加)。左の関手に合わせています。

We take the direction of an adjunction as the direction of its corresponding left adjoint functor

しかし、同じ論文内でも場合により反対方向にしています。この「場合により」を判断するのがけっこう大変です。

随伴系の方向も明示するために、次の書き方に変更します。

  • (η, ε: F -| G, F:CD)
  • (η, ε: F -| G, G:DC)

一番目は、Fと同じ方向を随伴系の方向として、二番目は、Gと同じ方向を随伴系の方向とします。

随伴に関わる曖昧な言葉と明確化

「随伴」「左(または右)随伴」「左(または右)随伴を持つ」のような言葉は、安易に使うのは危険なようです。次のような言葉で代替したほうがよいでしょう。

  1. 随伴系〈adjunction | adjoint system〉
  2. 随伴系の左(または右)関手〈left/right functor of an {adjunction | adjoint system}〉
  3. 左(または右)パートナー〈left/right partner〉
  4. 左(または右)可随伴〈left/right adjointable〉
  5. 左(または右)随伴付き〈with left/right adjoint〉

随伴系は、前節で述べた記法で、(η, ε: F -| G, F:CD) と書けます。これは、随伴系の構成素〈constituents〉を並べたもので、法則として2つのニョロニョロ等式〈{snake | zigzag | zig-zag | triangle | triangular} {equation | identity | relation}〉を満たします。

随伴系 X = (η, ε: F -| G, F:CD) の構成素であるFをXの左関手、GをXの右関手と呼ぶことにします。これは、先に随伴系Xがあるときの呼び名です。

随伴系 X = (η, ε: F -| G, F:CD) が与えられている前提で、FはGの左パートナーであり、GはFの右パートナーになります。「パートナー」は、与えられた随伴系のなかにおける、構成素のあいだの相互関係を意味しています。(「圏論の随伴をちゃんと抑えよう // 左と右を忘れるんだが」も参照。)

関手 F:CD右可随伴とは、Fを左関手とする随伴系が存在することです。これは、関手Fの性質として、随伴系の存在を主張しているだけで、特定の随伴系を指定しているわけではありません。左可随伴も同様です。

関手 F:CD右随伴付きとは、Fに対して特定の随伴系が指定されており、その随伴系のなかでFが左関手となっていることです。「右パートナー付き」のほうが適切だと思いますが、「右随伴」という言葉は残しました。左随伴付きも同様です。

最初から随伴系が与えられているのか? それとも関手が与えられて随伴系を探す話なのか? それが曖昧だと問題意識を把握できないので、今述べたような区別を意識したほうがいいでしょう。

構造か命題か

F -| G という記法は安定しているので安心して使えます。しかし、これが何を意味するかは文脈により変わります。

「F -| G」、あるいは「随伴ペア F, G」が、随伴系 (η, ε: F -| G, F:CD) または (η, ε: F -| G, G:DC) の略記として使われることがあります。随伴系は構成素と法則からなる構造なので、この場合「F -| G」は構造を意味します。

一方で、「F -| G」が命題を簡潔に表現するために使われることがあります。その意味は次のようです(3つは同値な命題です)。

  • Fを左関手、Gを右関手とするような随伴系が存在する(あるいは構成可能である)。
  • Fは右可随伴である。
  • Gは左可随伴である。

構造はモノ、命題はコトですから、別なんですが、同じ記号を使って表現されることがあるので注意が必要です。

2018-12-26 (水)

最近のモナド論の概観と注意事項 1/2

| 16:49 | 最近のモナド論の概観と注意事項 1/2を含むブックマーク

モナドの理論を高次圏論を使って定式化すると、だいぶスッキリします。しかし、ベースになる高次圏論の概念・用語・記法が安定してないので、解説を読むのに苦労します。解説の解説(ガイダンス)があるといいような気がするので、ザッと書いてみます。落とし穴を指摘した道案内といったところです。

この記事と、あともう一回続きを書く予定です。

内容:

  1. 最近のモナド論とは
  2. モナド論を分類すれば
  3. モナド論をホストする圏
  4. 参考文献と著者
  5. 続きは

最近のモナド論とは

モナドの理論は、形式理論(後述)も含めて、1960年代/1970年代に完成したと言っていいでしょう。代表的な著作を挙げれば*1

  • ベック〈J. Beck〉の"Distributive Laws"が1969年
  • ストリート〈R. Street〉の"The Formal Theory of Monads"が1972年
  • グレイ〈J. Gray〉の"Formal Category Theory: Adjointness for 2-Categorires"が1974年

もちろん、その後もさまざまな方向への発展や、さまざまな分野への応用は続きましたが、中核的な内容は前世紀に出来上がっていたのです。

記事タイトルの「最近」とは、ここ20年くらいの話です。モナド論の中核的な内容が、高次圏論を用いて整理されました(もともと、モナドは高次圏的な概念ではありますが)。昔から知られていた事実でも、新しい側面からの解釈が生まれたりしました。今世紀に入って「今風にリフォーム(あるいはリフォーミュレーション)された」と言えばいいでしょうか。

しかし、モナド論を整理・リフォームするために使われる低次元の高次圏論〈low-dimensional higher category theory〉自体が未整理で混乱した様相を呈しています。このため、せっかくの今風のモナド論も、分かりにくく見えてしまいます。

低次元の高次圏論の(だらしなくザンネンな)用語法につては次の記事に書いてあります。僕の立場(つうか好み)による用語の選択もしています。

圏の“弱さ”が色々あって、話が難しくなったり曖昧になったりする事情は次の記事:

圏のサイズの問題と、それに対する楽観的態度については:

高次圏論(特に低次元部分)は、現状ではグチャグチャしているのですが、モナド論は高次圏論のよい応用なので、モナドをきっかけと題材として低次元高次圏論に入門するのもアリだと思います。

モナド論を分類すれば

モナドの理論を、次のようなダイコトミー〈二分法〉により分けておくと便利そうです。

  • 局所 vs. 大域
  • 形式 vs. 非形式

組み合わせると、次のようなモナド論があることになります。

  1. 非形式局所モナド
  2. 非形式大域モナド
  3. 形式局所モナド
  4. 形式大域モナド

このなかで、形式局所モナド論はあまり意味がないので取り除き、形式大域モナド論を単に形式モナド論とも呼ぶことにします。

局所モナド〈local theory of monads〉とは、特定の圏Cを固定して、C上のモナドだけを考えることです。C上のすべてのモナドを考えるかも知れませんが、異なる圏上のモナドを一緒に考えることはしません。それに対して大域モナド〈global theory of monads〉は、モナドの台圏〈underlying category〉を固定せずに、すべての圏の上のすべてのモナドを同時に考えます。

「形式〈formal〉」という言葉は注意が必要です。論理やプログラミング理論の形式体系〈formal system〉の意味の「形式」とは(無関係ではありませんが)違いますモナドは、圏、関手、自然変換を使って定義されます。それを、2-圏の対象、2-圏の射、2-圏の2-射に置き換えた定義から出発する理論がモナドの形式論〈formal theory of monads〉、あるいは形式モナドです。

圏の圏Catは、典型的な2-圏なので、Cat上で形式モナド論を展開できます。これが、通常の(形式化しない)モナド論です。非形式モナド論では、具体的に与えられた特定の2-圏(CatまたはCAT)内のモナドを考えますが、形式モナド論は、(適当な条件を満たす)2-圏ならどれでも通用する形で理論を構成します。

モナドは、「2-圏K内の対象C上のモナド」という特徴付けがされますが、モナドが居る環境である2-圏KCat(またはCAT)に固定し、さらにモナドの台Cも固定した議論が非形式局所モナドです。台を固定しないで、Cat(またはCAT)内の任意の対象を許した形が非形式大域モナドです。さらに、モナドが居る環境を(適当な条件を満たす)任意の2-圏にして考えると形式大域モナド論=形式モナドになります。

モナド論をホストする圏

前節の分類は、モナドをどこで考えるか? に関わっています。つまり、モナド論を展開する“場”が問題なのです。この“場”もまた圏(高次圏〈n-圏〉)です。よって、“場”となる圏をハッキリさせておきましょう。

一般的な“圏の圏”を次の形で表すことにします。

  • ρ-Cat#r

ρは圏の次元と“弱さ”を表します。n次元の“弱さ”を表すラベルの集合をWnとします。n = 0, 1, 2, 3 に関しては:

n Wn
0 {0}
1 {1}
2 {s2, w2}
3 {s3, ..., w3}

nが3以上になるとWnはよく分かりません。一番“強い”種類である sn (厳密n-圏という種類)はハッキリしています。wn は一番”弱い”種類ですが、nが大きくなると(おそらく n = 5 以上では)wn-圏の定義を具体的に書き下すことは事実上不可能になります。順序集合(またはプレ順序集合)としてのWnを明確にするのはとても難しいでしょう。

2-Catのような書き方は曖昧なので、s2-Cat, w2-Cat を使います。“弱さ”がハッキリしないときは、?3-Catのように、「不明」と明示して書くことにします。ワイルドカード'*'を使って *n-Cat と書くと、任意の“弱さ“を持つn-圏を意味することにします。

下付きの"#r"で使うrは整数で、圏のサイズの階層を表します。U0は、可算無限集合ωを要素として含むグロタンディーク宇宙とします。そして、U0U1U2 ∈ ... をグロタンディーク宇宙の所属系列とします。このような所属系列が存在することは、楽観的な仮定ですが、それについては「入れ子の宇宙を可能とする公理」参照。

宇宙Ur内で考えた“小さなn-圏の(n+1)-圏”を ρ-Cat#r(ρ∈Wn)と書きます。wn-Catr∈|w(n+1)-Catr+1| が成立します。

よく使う圏は、次のように略記します。

  • Set := 0-Cat#0
  • SET := 0-Cat#1
  • Cat := 1-Cat#0
  • CAT := 1-Cat#1
  • s2-CAT := s2-Cat#1
  • Bicat := w2-Cat#0
  • BICAT := w2-Cat#1

Set∈|CAT|, Cat∈|s2-CAT| が成立します。

Cがn-圏で、0 < k ≦ n を整数だとして、kC は、(k + 1)次元以上の射をすべて捨ててしまったk-圏を意味します*2。例えば、1Cat は、“小さい圏の圏”ですが、自然変換を考えないものです。0C = |C|, nC = C が成立します。

C |→ kC は、圏(n-圏)を加工して圏を作る対応です。構成素の一部を捨てているので、切り捨て〈truncation〉です。切り捨ては、実はけっこう重要な操作です。

参考文献と著者

僕が眺めた(読んだとは言ってない)論文を古い順に並べます。

クリメン/ソリヴェレス 2010

アイレンベルク/ムーア構成〈Eilenberg-Moore construction〉とクライスリ構成〈Kleisli construction〉の関係を調べているときに引っかかった論文で、この話題(アイレンベルク/ムーア構成とクライスリ構成)に関して、丁寧に書かれた良い解説だと思います。また、例が、順序、論理、位相、一般代数〈universal algebra〉などから引かれていて面白いです。

ただし、読みやすくはないですね。あまり一般的でない用語・記法(例:conjugateとtranspose)が、他の文献への参照で済まされているのですが、参照先が(昔の紙の資料で)入手にしくいんですよ。前半がかなり冗長な感じなので、そこを圧縮してもうちょいセルフ・コンテインドにして欲しかった。また、記号のオーバーロードが激しい(例:圏EM、関手EM)ので、これも読みにくい原因かも。

ザワドウスキ 2010

短い論文ですが、密度が高くて難しいです。3-圏、4-圏を使ってモノイド・モナドを解説してますが、後半は僕にはよく理解できません。前半で、アイレンベルク/ムーア構成とクライスリ構成が今風に導入・定義されています。が、定義が特殊ケース過ぎる気もします。

なお、arXiv.org にある2010年投稿論文(上記)の、出版(ジャーナル掲載)されたバージョンがあります。

バスケス-マルケス 2015

"クリメン/ソリヴェレス 2010"と"ザワドウスキ 2010"の内容を咀嚼してより分かりやすく書いています。これは読みやすいです。中心となる概念の定義が付録にまとまっているので、付録を最初に、あるいは必要な時点で参照しないとワケわからないことになります。

ブーム 2018

今年出た論文ですが、定義を比較する目的で最初の数ページを眺めただけです。モノイド構造を持つモナドを一般化した形式論らしいです(読んでないのでよく知らんが)。


名前をカタカナ表記するために調べた情報を記します。

クリメン/ソリヴェレス

J. Climent Vidal と J. Soliveres Tur は、スペインのバレンシア大学の人のようです。省略されている J. は二人とも Juan で、スペイン語では「ホアン」と発音するようですが、「カタルーニャ語の人名であるジョアン(Joan)をスペイン語式に読んだもの」だとか。カタルーニャ出身なのかも知れません。

名前が3つの部分からなるので、最後の Vidal と Tur で呼べばいいかと思ったのですが、他から参照されるときに J. Climent and J. Soliveres と書かれていたので、クリメン〈Climent〉/ソリヴェレス〈Soliveres〉とします。クリメンさんは、Juan と Climent の間にもうひとつ名前(の要素)が入るみたいです、メールアドレスが Juan.B.Climent@uv.es なので。

ザワドウスキ

ポーランドのワルシャワ大学の人のようです。Zawadowski の発音がForve(https://ja.forvo.com/)にもPronounceNames(https://www.pronouncenames.com/)にもなかったので、みたまんまで「ザワドウスキ」とします。

バスケス-マルケス

メキシコのインカーネット・ワード大学バヒオ校〈Universidad Incarnate Word Campus Bajio〉の人みたい。テキサス州サンアントニオにあるインカーネット・ワード大学のメキシコ・キャンバスなんじゃないのかな、たぶん。Incarnate Word のメキシコ(スペイン語)での発音は、「インカルナテ・ウオルー」に近いようです。

Vazquez-Marquez はハイフンで繋がっているので、これでひとつの名字なんでしょう。

ブーム

ハンガリーのブダペストにあるウィグナー物理研究所〈Wigner Research Centre for Physics, Budapest〉の人みたいです。ファーストネームのガブリエラ〈Gabriella〉から女性だと思います。

続きは

タイトルに「1/2」を付けているので、もう一回続きを書く予定でいます(たぶん来年だろうが)。次回は、モナド論の中心的なトピックとか、事前に知っておくとよさそうな予備知識とか、誤解・勘違いしそうな所について書きます。

*1:ベックのモナド性定理〈Beck's monadicity theorem〉も1960年代の代表的な成果ですが、原典が分かりませんでした。

*2:「高次圏: 用語法と文脈(主に2次元)」では、C(k)という書き方をしていました。

2018-12-21 (金)

高次圏の反対圏をどう書くか

| 14:02 | 高次圏の反対圏をどう書くかを含むブックマーク

Cに対して、反対圏Copは一種しかないですが、高次圏の反対圏はイッパイ作れます。2次元の圏の場合でも、結合は2種類あるので、反転する/しないの組み合わせは4通りあります。

番号 第一の結合 第二の結合
1 反転しない 反転しない
2 反転する 反転しない
3 反転しない 反転する
4 反転する 反転する

これらをどう区別して書くか? 特に決まった書き方はないですね。ちょっと笑ってしまったのが、次の記法。

横方向の反転は下付きのopですが、縦方向の反転はopを90度回転して使ってます。

このopの例に限らず、文字/文字列の回転と鏡映を使いたいことはあります。手軽に出来るようになるといいんですけどね。

この記法の出典は:

2018-12-12 (水)

順序集合のカン拡張と特徴述語論理

| 19:10 | 順序集合のカン拡張と特徴述語論理を含むブックマーク

圏論における随伴系やモナドの概念を、順序集合に関して考えるとガロア接続や閉包作用素になります。同様に、圏論におけるカン拡張を順序集合に関して考えることができます。が、それだけだと実感に乏しく面白くもありません。カン拡張(右カン拡張と左カン拡張)を、述語論理の限量子と捉えてみます。

内容:

  1. 圏と順序集合
  2. 基本的な言葉と記法
  3. 劣拡張と最大劣拡張
  4. ミート完備な順序集合
  5. 最大劣拡張の構成
  6. 最小優拡張と書き方の約束
  7. 特徴述語論理
  8. おわりに

圏と順序集合

圏論に関する話を、順序集合に関する話にダウングレードすると、議論が容易になります。例えば、2つの関手が随伴対であることは、2つの単調写像がガロア接続を形成することと同じです。それについては:

モナドの順序的対応物に関しては:

「圏 → 順序集合」というダウングレードは簡単です。なぜなら、順序集合は特殊な圏とみなせるからです。Cがやせた圏〈thin category〉とは、次が成立することです。

  • A, B∈|C| に対して、ホムセット C(A, B) が空集合か単元集合のどちらか。

やせた圏は、プレ順序集合〈preordered set〉と同じです。さらに、やせた圏Cが次の性質を持てばとてもやせた圏〈very thin category〉です。

  • C(A, B) ≠ ¥emptyset かつ C(B, A) ≠ ¥emptyset ならば、A = B

とてもやせた圏は順序集合になります。より詳しくは次を参照:

何か圏論の一般的な概念があったとき、やせた圏/とてもやせた圏に制限すれば、それだけでプレ順序集合/順序集合に関する概念が出てきます。

基本的な言葉と記法

カン拡張に関しては、ここでは触れません。次の記事を参照してください。

圏の一般論と順序の理論の対応関係もいちいちは指摘しませんが、主要な用語の対応は次の表のとおりです。

圏の一般論 順序の理論
右拡張 劣拡張
右カン拡張 最大劣拡張
左拡張 優拡張
左カン拡張 最小優拡張

カン拡張における上下左右: 入門の前に整理すべきこと」で使った記号と、この記事内の記号との対応は:

圏の一般論 順序の理論
C, D, E 順序集合 A, B, C
関手 K:CD 単調写像 k:A→B
関手 F:CE 単調写像 f:A→C
関手 G, H:DE 単調写像 g, h:B→C
自然変換 α::F⇒G:CD 不等式 f ≦ g on A in B
右カン拡張 KF 最大劣拡張 kf
左カン拡張 KF 最小優拡張 kf

ここから先、A, B, C などは順序集合を表し、その順序は一律に'≦'で表します。f, g, h などは単調写像〈{monotone | monotonic} {map | mapping | function}〉を表します。順序集合AからBへの単調写像の全体を BA または [A, B] と書きます。AとBが順序集合のとき、次の文はすべて同じ意味です。

  • f:A→B は単調写像
  • f∈BA
  • f∈[A, B]

f, g∈[A, B] に対して、f ≦ g は次のように定義します。

  • f ≦ g :⇔ ∀a∈A.( f(a) ≦ g(a) )

a, b∈A に対して、a ≦ b であることを次のようにも書きます。

  • a ≦ b in A

f ≦ g in [A, B] のことを次のようにも書きます。

  • f ≦ g on A in B

圏のホムセットと同じ記法を順序集合に対しても使います。A(a, b) は次のような集合です。

  • A(a, b) := if a ≦ b then {(a, b)} else ¥emptyset

この定義より、

  • A(a, b) は、空集合か単元集合のどちらか。
  • A(a, b) ≠ ¥emptyset ⇔ a ≦ b

劣拡張と最大劣拡張

k:A→B と, f:A→C を2つの単調写像とします。g:B→C が、kに沿ったfの劣拡張〈lower extension of f along k〉だとは、次の不等式が成立することです。

  • 任意の a∈A に対して、g(k(a)) ≦ f(a)

A⊆B で、kが包含写像(埋め込み写像)の場合を考えると:

  • fは、Bの部分集合Aでしか定義されてない。
  • gは、B全体で定義されている。この意味で拡張
  • A上では、g ≦ f が成立しているので、gは順序的に〈下方 | lower〉である。

実際にはkは何でもいいのですが、上記の特殊な状況を考えると、劣拡張という呼び名が納得できるでしょう。ただし、kが包含写像でない場合は、「拡張」という呼び名は、国語辞書的にはまったく不適切になります。「概念が一般化されると呼び名が不適切になる」ことはよくあることなので、諦めましょう*1

(kに沿った)fの劣拡張の全体を LowExt(k, f) とすると、

  • LowExt(k, f)⊆[B, C]
  • [B, C] の順序をそのまま受け継いで LowExt(k, f) も順序集合。

順序集合 LowExt(k, f) に最大元が在ることは保証されませんが、もし最大元があれば、それを、fの最大劣拡張〈greatest lower extension〉と呼びます。gが、(kに沿った)fの最大劣拡張であるとは次のことです。

  1. g:B→C は、kに沿ったfの劣拡張である。
  2. h:B→C がkに沿ったfの劣拡張であるならば、h ≦ g on B in C 。

最大劣拡張が存在するなら一意です。g, g':B→C が、kに沿ったfの最大劣拡張とします。gが最大劣拡張でg'が劣拡張であることから g' ≦ g 、同様に g ≦ g' 、これらより g = g' です。

Cがタチの良い順序集合のとき、k:A→B と f:A→C を元にして最大劣拡張を構成することができます。Cに要求される性質(タチの良さ)と、最大劣拡張の具体的構成を次節以降で述べます。

ミート完備な順序集合

Aが順序集合で、X⊆A とします。このとき、次のような要素 a∈A が存在すれば、それをXのミート〈meet〉と呼びます

  1. ∀x∈X.( a ≦ x )
  2. b∈A が ∀x∈X.( a ≦ x ) を満たすならば、b ≦ a

一番目を満たすaは、Xの下界〈かかい | lower bound〉といいます。二番目の条件から、aは下界のなかで最大なものなので、ミートを最大下界〈greatest lower bound〉とか下限〈infimum〉とも呼びます。

AとXの選び方により、AにおけるXのミートは存在したりしなかったりですが、存在するなら一意に存在します(練習問題)。そのミートを、次のように書きます(どの書き方でもよい)。

  • A(X)
  • infA(X)
  • glbA(X)

ここでは、∧A(X) という書き方を使い、Aが分かっているときは単に ∧(X) とも書きます。Iがインデックス集合で、α:I→A が写像のとき、∧(αの像) を色々な書き方で表します。

¥bigwedge_{i ¥in I} ¥alpha_i

¥bigwedge (i ¥in I |¥: ¥alpha_i)

¥bigwedge (¥alpha_i |¥: i ¥in I)

¥bigwedge ¥{¥alpha_i |¥: i ¥in I¥}

書き方の相違はホントにどうでもいいことなので、主に ∧(i∈I | α(i)) を使います('∧'をデカくもしない)。

順序集合Aが、任意の X⊆ A に対してミートを持つとき、ミート完備〈meet complete〉と呼びます。Aがミート完備なら、Pow(A)をAのベキ集合として、写像

  • ∧:Pow(A)→A

がチャンと定義されている〈well-defined〉ことになります。

Aがミート完備なら、任意の写像(インデックス族) α:I→A に関して、∧(i∈I | α(i)) は ∧(αの像) と同じなのでやはりチャンと定義されています。

最大劣拡張の構成

k:A→B, f:A→C という単調写像がある状況で、kに沿ったfの最大劣拡張を構成しましょう。ただし、Cはミート完備であるという条件を付けます。

上記のような k, f が与えられているとして、g:B→C を次のように定義します。

  • b∈B に対して、g(b) := ∧(x∈k-1(b)| f(x))

ここで、k-1(b) は、k:A→B の逆像集合です(記法k-1逆写像を意味しないので注意)。k-1(b)はAの部分集合で、fをk-1(b)に制限した写像(インデックス族) k-1(b)→C に対するミートは、Cのミート完備性から一意に存在します。したがって、b|→g(b) はチャンと定義された写像です。

今定義した g:B→C が、kに沿ったfの最大劣拡張であることを示すには、次の2つのことを示すことになります。

  1. gは、kに沿ったfの劣拡張である。
  2. hがkに沿ったfの劣拡張ならば、h ≦ g 。

一番目を示しましょう。a∈A に対して、

  • g(k(a)) ≦ f(a)

が言えればOKです。gの定義から、x∈k-1(b) ⇒ g(b) ≦ f(x) ですが、b = k(a) と置けば、a∈k-1(b) なので、g(k(a)) = g(b) ≦ f(a) が成立します。これで一番目は示せました。

次にニ番目を示しましょう。b∈B に対して、

  • h(b) ≦ g(b)

が言えればOKです。gの定義 g(b) := ∧(x∈k-1(b)| f(x)) から、c∈C がなんであっても、

  • [ア] 任意の x∈k-1(b) に対して c ≦ f(x) ならば、c ≦ g(b)

b = k(a) となるaが存在するときを考えます。hがfの劣拡張であることから、

  • [イ] h(b) = h(k(a)) ≦ f(a)

上記の[ア]に、x←a, c←h(k(a)) と代入すれば、次が出ます。

  • [ウ] a∈k-1(b) だから、h(k(a)) ≦ f(a) ならば、h(k(a)) ≦ g(b)

[イ]より実際に h(k(a)) ≦ f(a) なので、[ウ]を考慮すれば、

  • h(b) = h(k(a)) ≦ g(b) in C

が成立します。

b = k(a) となるaが存在しないときは、g(b) = ∧(x∈¥emptyset| f(x)) = ∧(¥emptyset) = (Cの最大元) 。

  • h(b) ≦ (Cの最大元) in C

はbがなんでも成立するので、この場合も h(b) ≦ g(b) は言えます。

以上から、bがなんであっても h(b) ≦ g(b) となり、gは劣拡張のなかで最大であることが分かりました。

最小優拡張と書き方の約束

今までの議論の不等号の向きを逆にすると、最小優拡張を定義できます。Cに関する条件としてはジョイン完備性を考えます。ほとんど繰り返しですが、ジョイン完備性の定義は書いておきましょう。

X⊆A に対して、次のような要素 a∈A が存在すれば、それをXのジョイン〈join〉と呼びます

  1. ∀x∈X.( x ≦ a )
  2. b∈A が ∀x∈X.( x ≦ b ) を満たすならば、a ≦ b

一番目を満たすaは、Xの上界〈じょうかい | upper bound〉といいます。二番目の条件から、aは上界のなかで最小なものなので、ジョインを最小上界〈least upper bound〉とか上限〈supremum〉とも呼びます。Xのジョインが存在するなら一意的です。

順序集合Aが、任意の X⊆ A に対してジョインを持つとき、ジョイン完備〈join complete〉と呼びます。Aがジョイン完備なら、Pow(A)をAのベキ集合として、写像

  • ∨:Pow(A)→A

がチャンと定義されます。

k:A→B, f:A→C の状況で:

  • g:A→C が、kに沿ったfの優拡張〈upper extension of f along k〉だとは、任意の a∈A に対して、f(a) ≦ g(k(a)) が成立すること。
  • g:A→C が、(kに沿った)fの最小優拡張であるとは:
    1. g:B→C は、kに沿ったfの優拡張である。
    2. h:B→C がkに沿ったfの優拡張であるならば、g ≦ h on B in C 。

Cがジョイン完備なとき、gを次のように定義すると、gは、kに沿ったfの最小優拡張になります。

  • g(b) := ∨(x∈k-1(b) | f(x))

kに沿ったfの最大劣拡張と、kに沿ったfの最小優拡張を(それがあれば)次の書き方で表すことにします。

  • (kに沿ったfの最大劣拡張) = kf
  • (kに沿ったfの最小優拡張) = kf

kf は、右カン拡張 KF の順序集合バージョン、kf は、左カン拡張 KF の順序集合バージョンです。

特徴述語論理

k:A→B, f:A→C で、Cがミート完備かつジョイン完備である状況で考えます。順序集合 A, B, C を次のように解釈します。

  • Aは、個体の領域〈domain of individuals〉と考える。個体の領域を、述語論理では議論の領域〈domain of discourse〉と呼ぶこともある。
  • Bは、Aに属する個体を特徴づける値・量の領域と考える。
  • Cは、論理的真偽値の領域と考える。ただし、二値真偽値とは限らない。

Cが真偽値の領域なので、写像 f:A→C は、個体に真偽値を対応させる述語ということになります。Cがミート完備・ジョイン完備であることから、述語に対する ∧, ∨ や、論理定数 T, ⊥ を定義することができます。無限も許す∧演算として全称限量子∀、無限も許す∨演算として存在限量子∃も導入できます。

通常の述語論理でお目にかからないのは、領域Bと写像 k:A→B です。kはBの値によってAの個体を特徴付ける写像と考えます。分かりやすい例は、Bの要素が属性値であるときです。例えば、Aが人の集合で、B = N とします。k:A→B は、人に年齢を対応付ける写像とします。年齢は人を特徴付ける値のひとつです。

年齢とはまったく異なった例として、A⊆B であり、k:A→B は包含写像のときを考えます。この場合、kはAの各個体をより広い“場”であるB内に埋め込んでいます。別な場に置くことも特徴付けと(ちょっと無理矢理に)考えれば、kは特徴付けの写像と言ってもいいでしょう。以下では、k:A→B を特徴付け写像〈characterizer〉と呼びましょう。

個体領域Aと特徴付けのための領域Bも順序集合ですが、離散順序も順序なので、単なる集合 A, B と単なる写像 k:A→B であっても順序集合と単調写像だとみなせます。

これで、順序集合/単調写像に関する構造を述語論理として捉える状況設定が出来たので、kに沿ったfの最大劣拡張 kf 、kに沿ったfの最小優拡張 kf を限量子付き命題として解釈しましょう。次の記法を導入します。

  • (kf)(b) = (∀x∈A, k(x) = b.f(x))
  • (kf)(b) = (∃x∈A, k(x) = b.f(x))

これらの命題(述語)は、B上の命題(述語)になり、そのインフォーマルな内容的解釈は、

  • k(x) = b であるすべてのxに対して f(x) である。
  • k(x) = b であるxで、f(x) であるxが存在する。

B = 1 = {0} として、k:A→B を自明な写像とするとき、∀x∈A, k(x) = 0.f(x) と ∃x∈A, k(x) = 0.f(x) は、特徴付けなしの ∀x∈A.f(x) と ∃x∈A.f(x) に同じになります。一方で、特徴付けを含む論理式の意味は、次の(通常の)論理式と同じです。

  • ∀x∈A.(k(x) = b ⊃ f(x))
  • ∃x∈A.(k(x) = b ∧ f(x))

おわりに

特徴述語論理に関しては、限量子を定義しただけですが、これがカン拡張(の一側面)の論理的対応物なのではないかと思います。述語論理は、ハイパードクトリン(短い記述はココ)などにより定式化できます。特徴述語論理を完全に定式化すると、いったいどんな構造になるのでしょう。

カリー/ハワード/ランベックの教義によれば、「圏論、論理、型理論/プログラム論」のあいだには対応関係(類似性)があるはずです。特徴述語論理をあいだにはさむことによって、カン拡張に対応する型理論/プログラム論的概念が見つかるかも知れません。限量子が関係するなら、依存型っぽいナニカかも知れません(よく知らんけど)。

*1:最近、僕がよくこのテの注意書きをするのは、国語辞書的な解釈に拘る人が、どうも相当数いるらしいと気付いたからです。「拡張してないのに、なんで『拡張』なんだ?」とか気にするのはまったく不毛です。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181212

2018-12-10 (月)

野菜そば

| 12:09 | 野菜そばを含むブックマーク

次のメニューの英訳部分がどうも解せなかったのですが、

googleで出すことに成功。「そば」はちゃんと訳すので「傍」にしました。

「椎茸うま煮そば」は出せませんでした。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181210