以前、モナドは自己関手圏におけるモノイドであるという話をしたことがあるのだけど、この時は理解が足りなくてFreeモナドにまで踏み込めなかった。今日調べていたら、Free Monoid Objectsというわかりやすいエントリを見つけたので簡単に紹介。
まず、以前のスライドの中ではモノイド対象をモノイダル圏の中で特定の条件を満たす対象と射の組(M, μ、η)と定義をしたけど、紹介したエントリでは関手として定義している。もうちょっと具体的に言えば、1、M、M□M、M□M□M、・・・というモノイド対象のみからなるシンプルなモノイダル圏(これをTh(Mon)と呼ぶ)を考えて、そこからの関手Fがモノイド対象を定義するという見方。この見方がありがたい点は2つ挙げられる。
- (モノイダル)自然変換がモノイド準同型になってくれる*1
- モノイド F,F':C^Th(Mon)→C とモノイド準同型 τ:F→F'について、FMとτ_Mを対応させることで簡単に忘却関手を得られる
忘却関手の左随伴を、普通は"自由"関手と呼ぶ。じゃあこの忘却関手に左随伴はあるのかということだけど、元エントリによれば「closed category with countable coproducts」であれば持つっぽい。可算直和により、1+C+C□C+C□C□C+...と定義する事で自由モノイドの台対象が得られる。ηは直和の定義による埋め込み1→1+C+...でよい。μは、モノイダル積□が直和を保存すれば(ちょっと面倒だが)定義できる。closed categoryであればcolimitが保存されることからこれが成り立つ。直和の定義による埋め込みC→1+C+...を考えるとこれがunitとなり、これによって左随伴となる。
Setsで考えてみると、これはきちんと自由モノイドの定義になっている。1+C+C×C+C×C×C+...はCの要素を任意個とって並べた列だし、μは(ちょっと面倒だが)連結に該当することが確かめられる。unitは値が1つの列としての埋め込みになっていて、ああ、我々の知る自由モノイドだなとわかる。
これを自己関手の圏で考えると、即座にFreeモナドが得られる。ただし、自己関手の圏における直和の存在とモノイド積、即ち関手の結合が直和を保存するかは検討が必要だろう。前者は元の圏が直和を持てば関手圏でも(F+F')f := Ff +F'fとすれば直和を定義できる。後者は正直に白状すると細かく検討できてないのだが、Sets上であれば関手圏はCCCなので条件は満たすだろう。
*1:と書きつつ、モノイダル自然変換の定義はあまりわかってない・・・
