マクレーンを読んでて米田の補題を示したはいいが何やってるか全然わからないし、議論する階層も深すぎて何を扱ってるのかもよくわからなかったのでしょうもない
例を作った。式は
だが、右のから何か元をとってきてそこからどんな自然変換ができるかを見てみることにした。
それぞれの登場人物は、以下のようにする。
- 圏: モノイドの圏。
- 関手: からへの忘却関手
- : 「という4文字のアルファベットを並べた文字列」というモノイド
そして、の元として文字列「」をとり、これがでどんな自然変換を生むかを見る。
「AabB」を使って、モノイドを固定したときに自然変換を作りたい、つまり
モノイド準同型がでのどこに写るかを定めたい。
そのためには以下の図式を使うのだった。
ここで、この図式の左側はモノイドの圏の図式で、右側が集合の圏の図式なことに注意する。
ここで、右の四角の左上に恒等写像を流せば、図式の可換性より
となるが、このを今は文字列「」と定めるというのが
の定義だった。つまり、
であり、
ということになる。
具体的にこの自然性を使ってみる。
いま、「という2文字のアルファベットを並べた文字列」というモノイドを考える。
また、先のモノイドはと書くことにする。
さらに、モノイド準同型を文字数を数えるモノイド準同型とする。
ただし、は0以上の自然数。このとき、自然性より次の図式が得られる。
ここで、この図式の左側はモノイドの圏の図式で、右側が集合の圏の図式なことに注意する。
ここで、図式の左上に、大文字を小文字に、小文字をそのままにするモノイド準同型
を入れてみる。すると、
↓→というたどりかたでは、
一方、→↓というたどりかたでは、
となり、確かに一致する。↓→でのはモノイドの元であり、
→↓でのは集合の元であることに注意する。
つまるところ、「準同型を忘却させて関数を作り、そこに『AabB』をわたす」という操作は自然である」ということになった。
忘却関手を使うとこのへんがごちゃごちゃになるしもうちょっと込み入った関手を使えばよかったのかなあ。