米田モナド、図式平坦化モナド、ペースティングモナド
本編で書いた米田モナドだが、
次の論文にほとんど書いてある。
上記本文では、単に前層モナドと言っている。台が前層関手だから。前層モナド=米田モナドは、PSh:Cat→CATではなくて、PSh:Cat→CoCOMP という関手のプロファイルとしている。CoCOMPは余完備で局所小な圏の圏。確かに、PSh(C)が単に局所小では漠然とし過ぎている。カン拡張を作る場合でも、余完備性がいるから、CATに入ります、は条件が弱い。
次に図式平坦化モナド、まずは簡単な例から。
Sを1-箙の圏の部分圏だとする。とりあえず、有限離散箙の圏をSとする。S∈|S| にたいして、関手圏と同じ要領で図式の圏 [S, C]が作れる。φ:S→T という箙射があると、引き戻し φ*:[T, C]→[S, C] が定義できるので、S|→[S, C] はインデックス付き圏となる。余前層の圏の構成と同じ。
上記のインデックス付き圏のグロタンディーク平坦化を図式の圏と呼び DiagS(C) と書く。単に、Diag(C)とも書く。
1∈|S| とすれば、[1, C] C なので、C→Diag(C) の埋め込みは作れる。この埋め込みを ηC:C→Diag(C) と書く。
あとはモナド乗法。Diag(Diag(C)) → Diag(C) は面倒だが、グロタンディーク平坦化と同じように作れるだろう。
Diagモナドは、圏の圏CATに働く。アイレンベルク/ムーア圏EM(CAT, Diag)は、最初に選んだSにより変わるが、離散有限の形状(Sの対象を形状と呼ぶ)を選ぶと、そのアイレンベルク/ムーア代数は、デカルト圏だと思う。
CATは2-圏なので、Diagは実際は2-モナドだと思うが、2-モナドがよく分かってない。
形状の圏Sとアンビエント圏Cに対するDiagS(C) は、Cに値を持つモデル(意味論)の圏になる。Sが指標の圏で、Cが計算の圏。
次にペースティングモナド。これは普通の図式計算法をモナドの形にしたもの。そもそも圏の定義が、特殊なペースティングモナド(リスト連接モナド)のアイレンベルク/ムーア代数になっている。
n-箙Aを考え、Aのセルの集合に貼り合わせデータを一緒に考えたものをペースティング図と呼ぶ。ペースティング図のペースティング図をペースティング・スキーマと呼ぶ(確か?)。ペースティングスキーマをペースティング図に落とす操作をモナド乗法とするモナドが存在するだろう。
少なくとも1-箙に関しては構成できる。
1-箙 | n-箙 |
---|---|
頂点 | 0セル |
アロー | 1セル |
- | i-セル |
隣接条件 | 貼り合わせデータ |
パス | ペースティング図 |
パスのパス | ペースティングスキーマ |
連接 | ペースティング |
ペースティングモナドがn-圏を定義するモナドで、平坦化モナドが極限を定義するモナド。
コンピュータッドと相対コンピュータッドの話を入れないとダメだが、後で考えよう。