-
- いいね！0
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。自由モノイドの(すなわち「文字列」全体の集合を与える)X↦MXの話に戻る。モナドが与えられるとそのモナドに対応する「代数系」の概念が自然に定義されます。MXの代数系の構造(文字列が連結できること)はたった一つの写像μ_X:MMX→MXで表現されるのでした。続く
2017-02-07 22:38:50
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。同様に集合Aにモノイドの構造が入っていれば、集合Aの元を並べたものにAのモノイド構造を使って連結して得られるAの元を対応させる写像α:MA→Aが得られます。写像αはAのモノイド構造の情報をすべて持っている。このような(A,α)をM代数と呼びます。続く
2017-02-07 22:46:53
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。M代数の満たすべき公理系はモノイドの作用の公理系と完全に同じなので省略。モナドMはそれ1つだけでM代数と呼ばれる代数系のみたすべき条件をすべて知っているわけです。集合にそれから生成される自由モノイドを対応させるモナドはモノイドのみたすべき条件をすべて知っている。続く
2017-02-07 22:53:18
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。これは自由群を作るモナドなど他のたくさんの代数系についても同じです。 随伴函手の話に戻る。一般に圏C上のモナドTとT代数の圏C_T (C_TにはEilenberg-Moore圏という権威ありそうな名前が付いているが名前にびびるのは非数学的)のあいだには〜続く
2017-02-07 23:00:26
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き〜、T代数にT代数の構造を忘れたもの対応させる函手U_T:C_T→Cと、Cの対象Xに自由T代数TXを対応させる函手F_T:C→C_Tが自然に定まり、随伴函手対になり、自明にT=U_T F_Tとなります。T代数の正体がわかっていればこれで基本設定は〜
2017-02-07 23:07:37
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き〜終了なのですが、そうでないときには、具体的な随伴函手対U:D→C、F:C→DでモナドをT=UFと作ったとき、DがT代数の圏C_Tといつ同値または同型になるかを知る方法が必要。それがBeckのmonadicity定理です。MacLaneの圏論の教科書に書いてある。
2017-02-07 23:14:58
黒木玄 Gen Kuroki
@genkuroki
#数楽 証明を読んだこともないし、詳しくもないのですが、DeligneさんはBeckの定理を「群」の概念を理解するためにもっとも基本的だと思われる淡中圏の理論の整備に使ったそうです。
2017-02-07 23:38:45
黒木玄 Gen Kuroki
@genkuroki
#数楽 続く。群の定義は数学を少しかじった人達にはおなじみのものだと思いますが、実際に応用されるときには群そのものよりも、群の作用や表現の方が役に立つことが多いのです。群の作用や群の表現のように見えるもの達の方から群を作る方法があるのらば、群概念の応用範囲は大きく広がると〜続く
2017-02-08 00:09:17
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き〜考えられます。実際にそういう理論は作られており、現代ではそれらを総称して淡中双対性と呼ばれているようです。淡中先生は私が学生時代に習った先生達の先生です。各種の淡中双対性については→ ncatlab.org/nlab/show/Tann…
2017-02-08 00:12:34
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。群の表現のように見えるもの達(群の表現の圏のような圏)の中には条件を弱めると対応する群が無くなり、群概念を拡張する必要が出て来ます。量子群はそのような意味での群概念の一般化になっています。群では記述できない意味のある「対称性」が1970〜80年代に発見されました。
2017-02-08 00:18:25
黒木玄 Gen Kuroki
@genkuroki
#数楽 私がモナドの話を始めたのでfunctionalプログラミングに興味を持った人が覗いて見たら、淡中双対性というガチ数学の話になって残念に思っている人達がいるかもしれませんが、これは数楽の雑談なので仕方がない。続く
2017-02-08 00:34:36
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。というわけで、集合から自由モノイドを作るモナドM:C→Cの話に戻る。ここでC=(集合の圏)。このときC_M=(M代数の圏)=(モノイドの圏)となります。モノイドの圏の中には自由モノイドMX (Xは集合)達が含まれており、自由モノイド間の準同型g:MX→MYは〜続く
2017-02-08 00:46:06
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き〜、写像f:X→MYと一対一に対応しています。対応の作り方はf=η_X⚪︎gとg=f^*=μ_Y⚪︎Mfです。この対応は一般のモナドでも同様で、f↦f^*は、Haskellでの=<<::(X→MY)→(MX→MY)と書かれている"bind"です。続く
2017-02-08 00:53:32
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。要するにHaskellでのモナドのbindは、圏論でのモナド上の自由代数間の射の記述そのものであるわけです。私にはこういう直観抜きにモナドの応用を理解できることが信じられません。理解の仕方には色々な経路があるものです。
2017-02-08 00:57:04
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。一般に集合Xから生成される自由○○(○○はモノイドや群や環などの代数系の名前)をTXと書くと、TXからTYへの射(○○の準同型写像)はXからTYへの写像と自然に一対一に対応しています。これはXからTXへの写像(函数)にTXの元を代入できることを意味しています。続く
2017-02-08 01:03:29
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。文字数制限の縛りに負けて「代入」と書くべきところでカギカッコを略してしまった。函数f:X→TYにTXの要素を文字通りの意味で代入することはできないのですが、TXが自由○○ならば「代入」できる。より一般にTがモナドでも同様に「代入」できるわけです。続く
2017-02-08 01:08:31
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。自由○○(○○は代数系の名前、完全に一般の場合にはモナドTに対するT代数)に関する直観があれば、函数f:X→TYにTXの要素を代入できることは当然だと思えるようになります。Haskellではその操作をα∈TXについてα>>=fなどと書くわけです。
2017-02-08 01:14:37
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。まとめ：モナドTに対するTXはXに新たな要素や演算を追加して作られた自由代数(「代数」の意味はT代数の意味でおそろしく拡張されている)であり、函数f:X→TYにTXの元を「代入」することができ、射f^*:TX→TYが自然に得られる。続く
2017-02-08 01:26:50
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。以上の話は、自由モノイド、自由群などの例を知らず、「自由○○」という用語に関する直観を持たない人達にとってはありがたみがないかもしれませんが、そういう直観を持っていればHaskellのモナドについても「見たことがある！」と言えることを示した点で意味があると思います。
2017-02-08 01:32:15
黒木玄 Gen Kuroki
@genkuroki
#数楽 もう一度まとめると、 ・モナドTはT代数を定める。 ・TXはXに新たな要素や演算を追加することによって作られた自由T代数である。 ・だから函数f:X→TYにTXの要素αを「代入」してTYの要素が得られる。 ・その「代入」操作をHaskellではα>>=fと書く。
2017-02-08 01:38:39
黒木玄 Gen Kuroki
@genkuroki
#数楽 例：モナドMaybeをMaybe X=X⊔{Nothing}と定める。函数f:X→YはNothingをNothingに対応させることによって函数Maybe X→Maybe Yに拡張される。モナドの構造はNothingはNothingに移されるという規則で定まる。続く
2017-02-08 01:47:05
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。Maybeモナドは計算できない場合にはNothingを返す函数を定義するために使えます。 集合Xで生成される自由Maybe代数Maybe Xは集合XにNothingを追加して、Nothingは常にNothingに移すというルールで作られたものになっています。
2017-02-08 01:58:16
黒木玄 Gen Kuroki
@genkuroki
#数楽 続き。Maybeモナドのモナド演算μ_X:Maybe Maybe X→Maybe Xは:Maybe Maybe Xで重複して追加された2つのNothingを1つにまとめる写像に過ぎません。
2017-02-08 02:01:16
黒木玄 Gen Kuroki
@genkuroki
#数楽 例：任意の直和 Maybeモナドは{Nothing}を任意の集合Aに置き換えた自明な一般化TX=X⊔A (disjoint union、交わりを持たない和集合、直和)を持ちます。モナド演算は重複して追加されたAをひとつにまとめる写像と定義されます。
2017-02-08 02:10:26
黒木玄 Gen Kuroki
@genkuroki
#数楽 例：任意のモノイドS(たとえば文字列の集合S)に対して、TX=X×Sと定めると自然にTはモナドとみなせます。モナドの演算はμ_X:X×S×S→X×S, (x,a,b)↦(x,ab)です。これを使えばモノイドSの元(たとえば文字列)で計算のログを残すことができます。
2017-02-08 02:19:57