このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

またインデックス付き圏が出てきたけど、これはどうなっている?

動機とか背景を説明する気力と時間がないし、ほとんど確認してない当てずっぽうを言います。やりたいことは、たくさんのモナド達を扱うことです。

Cに対する自己関手の圏 E = End(C) は、非対称な厳密モノイド圏です。非対称であれなんであれ、モノイド圏内のモノイド(モノイド対象、モノイド構造、内部モノイド)の圏は定義できるので、Monoid(E) = Monoid(End(C)) は作れて、それがC上のモナドの圏にほかなりません; Monad(C) = Monoid(E) = Monoid(End(C)) 。

圏Monad(C)の対象はモナドで、モナド M = (M, η, μ) と N = (N, η, μ) のあいだの射αは、台関手のあいだの自然変換 α::M⇒N で、モナド単位η、モナド乗法μを保存するものです。

C上のモナドMによるクライスリ圏を Kl(C, M) とします。だいぶ前に確認した記憶がある(?)のですが、モナドのあいだの射 α:M→N in Monad(C) があると、クライスリ圏のあいだの関手 Kl(C, M)→Kl(C, N) を誘導します。これが僕の勘違いだと話がメチャクチャなんですが、αにより共変に誘導される関手を Kl(C, α) と書くとすると、Kl(C, -) は、Monad(C) から圏の圏Catへの関手となります。

適当な圏IからCatへの関手がインデックス付き圏なので、クライスリ圏の構成 Kl(C, -) もインデックス付き圏です。標準的なインデックス付き圏の定義では、ICat が反変なので、共変であるKl(C, -)は余インデックス付き圏と呼ぶべきしょうが、あんまり気にしないことにします。

インデックス付き圏Kl(C, -)のベース圏はMonad(C)です。ここで、Cも動かしたらどうなるでしょうか? Cをインデックス(パラメータ)とするインデックス付き圏、つまり多段階のインデックス付き圏が登場しそうです。Kl(C, -)の下部構造として、C|→Monad(C) という対応をインデックス付き圏と考えればいいわけです。

とは言っても、C|→Monad(C) がインデックス付き圏になる保証はありません。少しやってみると、ベースの圏に何か細工しないとインデックス付き圏になってくれそうにありません。どうしたものか? というのが今日の問題です。

関手 F:CD に対して、F*:Monad(D)→Monad(C) が誘導されればいいのですが、単なる関手Fがあっても、圏D上のモナドをC上に引き戻すことはできません。関手 F':DC を一緒に考えて、F, F' が随伴対となるような場合を考えると、N:DD から F;N;F':CC を作ればモナドの引き戻しになるような気がします。つまり、ベースの圏に圏と随伴対からなる圏を取るのです。

上記のことが成り立っているか確認できてないのですが、成り立っているとウレシイだろうと気付いたのは、ブール値の行列の計算をしていた時です。上記のことが成立するなら、特殊な事例として行列の等式や不等式が導けます。その等式や不等式は、状態遷移の記述に使えます。