16
15

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

FreerモナドとCoyonedaについて

Last updated at Posted at 2016-01-08

この辺を読んで書いた、数学の人向けのメモ
http://fumieval.hatenablog.com/entry/2013/05/09/223604
http://halcat.org/scala/extensible/

Freerモナドとは何か

$\mathcal{H}$ をHaskellの圏だとかその類としたとき、

  • Coyonedaと呼ばれる、対象の間の写像 $\mathrm{Ob}(\mathcal{H})\to\mathrm{Ob}(\mathcal{H})$ から自由に生成される関手 $\mathcal{H}\to\mathcal{H}$
  • 関手 $\mathcal{H}\to\mathcal{H}$ から生成される自由なモナド( http://qiita.com/monae/items/0fe34a6bb1b285be172a

を定義することができる。これらを続けて行えば単なる $\mathrm{Ob}(\mathcal{H})\to\mathrm{Ob}(\mathcal{H})$ からモナドを作ることができる。
それがFreerモナドだとか、Operationalだとか色々呼ばれている。

Coyonedaの定義

(豊穣圏で話をするのが面倒なので、集合の圏 $\mathcal{Set}$ を基準にしてやります。クラスやら宇宙の大きさの話も雑です)

$\mathcal{C}$ を圏とする。$F$ を対象間の写像 $\colon\mathrm{Ob}(\mathcal{C})\to\mathrm{Ob}(\mathcal{Set})$ とするとき、$A\in\mathcal{C}$ に対し

F^+(A)=\coprod_{X\in\mathcal{C}}F(X)\times\mathrm{Hom}_{\mathcal{C}}(X,A)

と定めると、射の変換も自然に定義できて(右成分にかければいい) $F^+$ は関手 $\mathcal{C}\to\mathcal{Set}$ になる。
$F$ から $F^+$ を作る操作は、関手に対して対象間の対応だけ取り出す忘却の左随伴なので、$F^+$ を $F$ で生成された自由な関手と言っても差し支えないだろう。

要するに、集合から自由加群を生成するやつの単なるmulti-objectバージョン。
これをHaskellやScalaで書いたものが冒頭のリンク先に掲載されている。

なんでこれがCoyonedaと呼ばれているのか

反変関手 $\mathcal{C}^{\mathrm{op}}\to\mathcal{Set}$ の圏(前層の圏)を $\mathcal{C}^\wedge$ と書くことにする。
$A\in\mathcal{C}$ に対し $\mathrm{Hom}_{\mathcal{C}}(\bullet,A)$ はそのような関手、つまり $\mathcal{C}^\wedge$ の対象となっており、これを ${H_A}$ とおく。
対象 $A\in\mathcal{C}$ と関手 $F\in\mathcal{C}^\wedge$ を取ると、集合として自然に1:1対応($\mathcal{S}\mathcal{et}$ における同型)

F(A)\simeq\mathrm{Hom}_{\mathcal{C}^\wedge}(H_A,F)

があるというのが米田の補題。

そこで今度は共変関手 $G\colon\mathcal{C}\to\mathcal{Set}$ を取ろう。このときは自然に

G(A)\simeq G\otimes_{\mathcal{C}}H_A

となる。ここで出てきた共変関手と反変関手のテンソル積を具体的に書けば、右辺は

\big(\coprod_{X\in\mathcal{C}}G(X)\times\mathrm{Hom}_{\mathcal{C}}(X,A)\big)\big/{\sim}

である。割るのに使う同値関係 $\sim$ は普通の加群と加群のテンソル積でやったのと同様(書くのが面倒なので省略)。

関手の圏でのHomの定義を思い出せばこれが米田の双対版(直積→直和、Ker→Coker、Hom→テンソル)であることがわかる。
よく見るとさっきのやつが割る前のところに出てきているのでこれが名前の由来だろう。
割るか割らないかの違いは、そもそもにしてHomの元の同一性なんて計算する気がないので黙殺されていると思われる。

感想

当たり前のものに変な名前を付けるのをやめてほしい

16
15
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
16
15

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?