モノイド圏内のモノイド対象の圏とパラメータ付きモナド

[追記]これは、 本編のコメント http://d.hatena.ne.jp/m-hiyama/20111107#c に対して書いたもの。[/追記]

C, D などは単なる圏、M, N などはモノイド圏を表すと約束する。モノイド圏のモノイド積と単位対象は、□, I を主に使う。以下の議論では、大きな圏を扱うと破綻するだろうから、適当なsmallnessは仮定する。

圏 C, D に対する関手圏は、通常 D^C と書かれるが、上付き指数が嫌なので [C, D] を使う。念のために定義を述べると：

1. 対象の集合： Obj([C, D]) = |[C, D]| = Func(C, D) = (CからDへのすべての関手)
2. ホムセット： [C, D](F, G) = Nat(F, G :C→D) = (FからGへのすべての自然変換)

M がモノイド圏なら [C, M] もモノイド圏

Mがモノイド圏のとき、関手圏 [C, M] には、Mのモノイド構造から誘導された標準的なモノイド構造を入れることができる。

記号を乱用して、M = (M, □, I) として、[C, M]上に定義される積と単位も □, I とすると、おおざっぱな書き方で：

1. (F□G)(x) := F(x)□G(x) （xは、Cの対象または射）
2. I(x) := (I in M) （定数関手）

モノイド対象の圏は、関手圏とみなせる

Mがモノイド圏のとき、M内のモノイド対象とモノイド準同型射が定義できて、その全体は圏となる。モノイド圏Mのモノイド対象（とモノイド準同型射）からなる圏を Mon(M) と書く。

モノイド圏とモノイド関手の全体からなる圏を MonCat とすると、Monは MonCat→MonCat という関手とみなせる。関手Monは表現可能で、その（共変の）表現対象は単体圏（the simplex category）Δ である。つまり：

• Mon(M) = MonCat(Δ, M) （= は圏同値）

関手圏（圏の指数）をMonCat内で考えるなら：

• Mon(M) = [Δ, M] （= は圏同値）

つまり、Mon = Mon(-) は、[Δ, -] = (-)^Δ in MonCat 。

圏の圏はデカルト閉

圏の圏Catは、圏の直積をモノイド積、1つの対象だけからなる圏を単位対象、圏同値をイコールのように扱って、デカルト閉になる。したがって、カリー化、反カリー化を行なってよい。

発見的な等式変形

Cは単なる圏、Mはモノイド圏として、以下の変形は不正確だがソレラシイ感じがする。「//」の後はコメント。

1. Mon([C, M]) // MonをΔで表現
2. [Δ, [C, M]] // 反カリー化
3. [Δ×C, M] // 直積の対称性
4. [C×Δ, M] // カリー化
5. [C, [Δ, M]] // Monの定義
6. [C, Mon(M)]

実際には、ブラケット [-, -] をオーバーロードしているので：

1. Mon(Cat(C, M) in MonCat)
2. MonCat(Δ, Cat(C, M) in MonCat)
3. Cat(Δ×C, M) in MonCat
4. Cat(C×Δ, M) in MonCat
5. Cat(C, MonCat(Δ, M)) in MonCat
6. Cat(C, Mon(M)) in MonCat

2から3への変形どうなってんの？ Δ×C は単なる直積か？ これらのあいだに、ほんとに自然な対応が作れるのか？ -- たぶん、なとかなるでしょ。

2つの圏、CatとMonCatを行ったり来たりして、外部ホムセットと内部ホム（指数）も行ったり来たりでヤヤコシイが、こういう等式（圏同値）変形ができるとウレシイかも。

たぶん、導かれること

発見的な等式変形でやったことはアヤシイけど、これに近い事実は期待していいだろう、つうことで：

• Cが圏、Mがモノイド圏のとき、Mon([C, M]) = [C, Mon(M)]

圏D上のモナドの圏を Monad(D) とすると、Monad(D) = Mon([D, D])。上記のMのところに、[D, D] を“代入”すると

• Mon([C, [D, D]]) = [C, Mon([D, D])] = [C, Monad(D)]