このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

Circ構成の一般化、スワップ公式とスワップ構造

モナド

Cが圏で、MとKをEnd(c)の部分モノイドとする。つまり、

  • F, F'∈M ならば、FF' = F;;F' もMに入る。
  • Cの恒等関手（IとかCとか書く）はMに入る。
  • G, G'∈K ならば、GG' = G;;G' もKに入る。
  • Cの恒等関手（IとかCとか書く）はKに入る。

K×M でインデックスされた自然変換の族τがある。G∈K, F∈Mに対するτの成分は [G, F]τ と書くことにする。[G, F]τ :: GF⇒FG であり、[G, F]τをGとFのスワッパーと呼ぶ。スワッパー（の族）は次の公理を満たす。

  • [I, F]τ, [G, I]τは、それぞれF, Gの恒等自然変換になる。
  • [G, FF']τ = ([G, F]τ)F' | F([G, F']τ)
  • [GG', F]τ = G([G', F]τ) | ([G, F]τ)G'

これは、対称（置換）やブレイディングに対する同種の公式を弱くしたものである。対称性はなく、片方向だけの主張になっている。

F∈M, G∈K、a, b∈|C| のとき、f:a.F→b.G を両マグマ（通常、両代数と呼ぶが、「代数」を使いすぎなので）と呼ぶ。すべてのF, G, a, bの組み合わせで作られた両マグマの全体をDiMagとする。上記の公理を満たすスワッパー族があれば、DiMagは圏になる。

ということをちゃんと述べたいんだけど、まず、End(C)の2つの（同じでもいい）部分モノイドとスワッパー族からなる構造に名前が必要だ -- 思いつかん、暫定的にスワップ構造でいいや。典型例は、モノイド積の掛け算関手達（対象でパラメータ付けされる）とブレイディングによるスワップ。

S = (C, M, K, τ)を、圏C上のスワップ構造とする。両マグマはSから作られるので、DiMag(S)と書く。これを圏にするために、とりあえあず D = DiMag(S) として、|D| = |C| とする。対象はベースの圏と変わらない。a→b である射は、a.F→b.G という両マグマ。この定義ではホムセットが集合であるかどうか保証されないが、まーいいとする。

D = DigMag(S) における恒等射 a→a は、a^:a.I→a.I として定義する。恒等もCと変わらない。次に結合だが：

  • f:a.F→b.G
  • g:b.F'→c.G'

に対して、次の定義をする。

  • f#g = (f.F' ; [G, F']τ ; g.G) : a.F.F'→c.G'.G

単位律は直ちに示せる。h:c.F''→d.G'' を加えて結合律を示すが、定義より次の2つの式が出てくる。

  1. (f.F' ; b.[G, F']τ ; g.G).F'' ; c.[G'G, F'']τ ; h.G'.G
  2. f.F'.F'' ; b.[G, F'F'']τ ; (g.F'' ; c.[G', F'']τ ; h.G').G

関手性により展開して：

  1. f.F'.F'' ; b.[G, F']τ.F'' ; g.G.F'' ; c.[G'G, F'']τ ; h.G'.G
  2. f.F'.F'' ; b.[G, F'F'']τ ; g.F''.G ; c.[G', F'']τ.G ; h.G'.G

両端は揃っているから、次の2つが等しいことを示す。

  1. b.[G, F']τ.F'' ; g.G.F'' ; c.[G'G, F'']τ
  2. b.[G, F'F'']τ ; g.F''.G ; c.[G', F'']τ.G

まずは、スワップ公式による展開。

  1. [G'G, F']τ = G'([G, F']τ) | ([G, F']τ)G
  2. [G, F'F'']τ = ([G, F']τ)F'' | F'([G, F'']τ)

これを具体化して、ひとつ上の式に代入すると：

  1. b.[G, F']τ.F'' ; g.G.F'' ; c.G'([G, F']τ) ; c.([G, F'']τ)G
  2. b.([G, F']τ)F'' ; b.F'([G, F'']τ) ; g.F''.G ; c.[G', F'']τ.G

また両端は等しくなるんで、問題は次の2つの式の等しさになる。

  1. g.G.F'' ; c.G'.[G, F'']τ
  2. b.F'.[G, F'']τ ; g.F''.G

最後に残った等式

  • g.G.F'' ; c.G'.[G, F'']τ = b.F'.[G, F'']τ ; g.F''.G

は、τの自然性から得られる。b.F'-(g)→c.G' に対してGF''を適用してみると、

  • b.F'.G.F'' --(g.G.F'')---> c.G'.G.F''

これの自然性を考えると：



  (b.F').G.F'' --(g.G.F'')---> (c.G').G.F''

  |                              |

  | [G, F'']τ                   | [G, F'']τ

  |                              |

  v                              v

  (b.F').F''.G --(g.F''.G)---> (c.G').F''.G

書き下してみると：

  • g.G.F'' ; (c.G').[G, F'']τ = (b.F').[G, F'']τ ; g.F''.G

目的の等式が得られた。