商環の同値関係a/s≡b/tをat=bsで定義してはいけない理由(あとまたAlloy)

またAtiyah-MacDonaldの可換環論入門を読んでいて、こんなことが書いてあった。

そのつくり方は、a,s∈A, s≠0なるすべての順序対(a, s)をとり、これらの組に対して次のように同値関係を定義することからなる。 (a,s)\equiv (b,t) \iff at-bs=0.この定義はAが整域であるときだけうまく昨日する。なぜなら、この関係が推移的であることの証明は消去律が成り立つこと、すなわちAは0と異なる零因子をもたないことを意味しているからである。

確かに商環の定義を at-bs=0としていけないとは習ったのだが、なんでそうしてはいけないのか、どんな例で推移律が失敗するのかを考えたことはなかった。とりあえず電車のなかで Z/4Zを積閉集合{1, 3}で商環にしたときのことを考えてみたのだがうまく行かなかったのでAlloyで調べてみた。

コードはgistに上げてある:
https://gist.github.com/ashiato45/0d0d0272dc6b2dc0ab22db2673a35d6b

  • isMultClosedでiが積閉集合であることの判定をする。
  • pEquiv [a, s, b, t]でa/sとb/tが上の意味で「等しい」かどうかを判定する。この関係をa/s \sim b/tと書くことにする。

これでmain3で、
「mcを積閉集合とし、a,b,cを環の元とし、s,t,uをmcの元とし、 a/s\sim b/t b/t\sim c/uがみたされているとする。このとき、 a/s\sim c/uが成り立つ。」と主張し、「check main3」でその反例を探しにいく。すると、次のような例がみつかった。
f:id:sle:20170531232016p:plain
これは、環 Z/2Zを考え、積閉集合として環全体をとり、 a/s=0/1, b/t=0/0, c/u=1/0を考えることに相当する。確かに at-bs=bu-ct=0だが、 au-cs=1となっていて、 0/1\sim 0/0, 0/0\sim 1/0だが 0/1\not\sim 1/0となっている。

そういうわけで一応反例は見つかったのだが、分母に0が来るのはなんとなく反則感があるので「積閉集合に0が入らない」という制約を追加して調べてみる。これがmain4である。実行すると、次のような例がみつかった。和と積は次のように入っている。
f:id:sle:20170531232919p:plain

this/Ring<:add={Ring$0->Element$0->Element$0->Element$2,
Ring$0->Element$0->Element$1->Element$3,
Ring$0->Element$0->Element$2->Element$0,
Ring$0->Element$0->Element$3->Element$1,
Ring$0->Element$1->Element$0->Element$3,
Ring$0->Element$1->Element$1->Element$2,
Ring$0->Element$1->Element$2->Element$1,
Ring$0->Element$1->Element$3->Element$0,
Ring$0->Element$2->Element$0->Element$0,
Ring$0->Element$2->Element$1->Element$1,
Ring$0->Element$2->Element$2->Element$2,
Ring$0->Element$2->Element$3->Element$3,
Ring$0->Element$3->Element$0->Element$1,
Ring$0->Element$3->Element$1->Element$0,
Ring$0->Element$3->Element$2->Element$3,
Ring$0->Element$3->Element$3->Element$2}
this/Ring<:mult={Ring$0->Element$0->Element$0->Element$0,
Ring$0->Element$0->Element$1->Element$1,
Ring$0->Element$0->Element$2->Element$2,
Ring$0->Element$0->Element$3->Element$3,
Ring$0->Element$1->Element$0->Element$1,
Ring$0->Element$1->Element$1->Element$1,
Ring$0->Element$1->Element$2->Element$2,
Ring$0->Element$1->Element$3->Element$2,
Ring$0->Element$2->Element$0->Element$2,
Ring$0->Element$2->Element$1->Element$2,
Ring$0->Element$2->Element$2->Element$2,
Ring$0->Element$2->Element$3->Element$2,
Ring$0->Element$3->Element$0->Element$3,
Ring$0->Element$3->Element$1->Element$2,
Ring$0->Element$3->Element$2->Element$2,
Ring$0->Element$3->Element$3->Element$3}

これは環 Z/2Z\times Z/2Zで、積閉集合として \{(0, 1), (1, 1)\}を考えている。
すると、 (1, 0)/(0, 1)\sim (0, 0)/(0, 1), (0, 0)/(0, 1)\sim (1, 0)/(1, 1)となっているが、
 (1, 0)/(0, 1)\not\sim (1, 0)/(1, 1) (1, 0)\cdot (1, 1) - (0, 1)\cdot (1, 1) = (1, 1) \neq (0, 0)よりわかる。

整域じゃない環について商環を真剣に考えたことがなかったので良い例が手に入って面白かった。あと、またAlloyが使えたので満足。

Alloyを使って可換環(有限)を調べてみる

ashiato45.hatenablog.jpで、prime avoidance lemma

環Aとそのイデアル\frak aと素イデアル\frak p_1,\dots,\frak p_nについて、
\frak a \subset \bigcup_{i=1}^n \frak p_iとなっているとする。
このとき、あるiに対して\frak a \subset \frak p_iとなる。

から素イデアル条件を外したときの反例を探していて、とりあえずn=2だと見つからないということを証明したのでした。
そこで、n=3のときの反例をAlloyで探そうとAlloyの勉強をしていたのですが、その前にid:qnighyさんが見つけてくれました(記事参照)。
とはいえ、やはりここでAlloyの使い方を覚えて反例探しを効率化したかったので、私は私でAlloyを使って見つけようと思っていたのでした。
ashiato45.hatenablog.jp
この記事で練習は済んだので、早速反例を探してみます。
コードはhttps://gist.github.com/ashiato45/bf148bfd114e45b0857baba6231e2a7cに貼ってあります。
あとちょっと補足しておくと、Alloyを使っている以上有限のものしか相手にできないので、もしも反例が無限の環にしかないのならお手上げです。

コードは群のときと大体同じです。今回は加法に対する単位元はzeroと名前をつけてあり、乗法に対する単位元はunと命名してあります。
oneにしなかったのは、Alloyのキーワードとぶつかっているからで、とりあえずフランス語の「1」にしておきました。
途中で可換環の定義が正しくできていることを確かめるために例を表示してみたのですが(50行目)、割と初心者殺しの観がある零環*1が見つかったのを見て、
「確かにAlloyで予めモデリングしておけばバグ発見に役立ちそうだなあ」と思いました。

そして、我々の例について位数8以下の環について例を探させたところ、次のものを得ました。
f:id:sle:20170219150720p:plain
元は8個で、Elements(番号)という形で出てくるので、ここではそれらをa_0,\dots,a_7と書くことにします。
出力によると1=a_3であり、0=a_7です。
そして、イデアル
{\frak a} = \{a_4,a_5,a_6,a_7\}{\frak p}_1 = \{a_6, a_7\}{\frak p}_2 = \{a_5, a_7\}{\frak p}_3 = \{a_4, a_7\}
でした。これを見ながら、これがどのような環かを考えてみます。

まず、8つの元の環なので、有限生成アーベル群の分類定理から、加法については{\mathbb Z}/8{\mathbb Z}{\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}({\mathbb Z}/2{\mathbb Z})^3のいずれかであることが分かります。
イデアル{\frak p}_1,{\frak p}_2,{\frak p}_3を見ると、2倍にすると0になる異なる元が3つあることになるので、とりあえず{\mathbb Z}/8{\mathbb Z}ではなさそうです。
2倍したときの性質は気になるので、さらにa_0,a_1,a_2,a_3の様子を加法の表(画像参照)で調べると、
a_0+a_0 = a_1 + a_1 = a_2 + a_2 = a_3 + a_3 = a_4となることがわかります。2倍して非零な同じものa_4になる異なる元が4つあるので、({\mathbb Z}/2{\mathbb Z})^3でもなさそうです。よって、この環の和についての構造は{\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}だということが分かります。
この環のなかで2倍された元でかつ非零な元というのは(2,0)しか有り得ないので、a_4=(2,0)が分かります。
さらに、a_0+a_0 = a_1 + a_1 = a_2 + a_2 = a_3 + a_3 = a_4ということを考えてみると、
a_0,a_1,a_2,a_3はそれぞれ(1,0),(3,0),(1,1),(3,1)のどれかであることがわかります。a_5,a_6は2倍すると0になる元でかつa_4=(2,0)ではないので、(2,1),(0,1)のいずれかであることがわかります。

積については何も見ていないのですが、(1,1)が多分乗法についての単位元だろうという気がするのでそれで辻褄が合うかを見てみます。
つまり、この環は{\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}に要素毎の加法と乗法を入れたもので、0=(0,0)であり、1=(1,1)であるものであり、
{\frak a}=\{(2,0),(2,1),(0,1),(0,0)\}{\frak p}_1=\{(0,0),(2,0)\}{\frak p}_2=\{(0,0),(2,1)\}{\frak p}_3=\{(0,0),(0,1)\}であるということになります。考えてみると、これで確かに辻褄があっていて、無事に反例が見つかり、その構造がわかりました。めでたしめでたし。

*1:元が1つで、その元が0でもあり1でもある環。この上では(かの有名な)0=1が成立する。

Alloyを使って有限群を調べてみる

Alloyはモノを抽象的に記述したり、それらの関係を数学で言うところの「関係」でもって記述する言語です。
さらに、そこで記された制約を満足する例を見つけたり、制約に対する反例を見つけたりするための解析器がついてます。
プログラムの仕様をこれで記述して、それに対して見落しがないかを探すのに便利みたいです。
公式サイトhttp://alloy.mit.edu/alloy/の記述を引用すると、

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.

ということになります。

以前http://ashiato45.hatenablog.jp/entry/2017/02/08/220148で、環に対する反例を見つけるのにAlloyを使おうと思ってこの本

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

で勉強していたのですが、ざっくり読んだのでid:qnighyさんが以前群でやっていたのを思い出しつつAlloyで群の性質を調べてみました。

できたコードはhttps://gist.github.com/ashiato45/b46837f5ff1237fa9c12e64ddaf4711eにあります。

sig Element{}

one sig Group{
	elements: set Element,
	unit: one elements,
	mult: elements -> elements -> one elements,
	inv: elements -> one elements
}

fact NoRedundantElements{
	all e: Element | e in Group.elements
}

まず元としてElementを宣言しておきます。これで、何らかの集合Elementが定義されます*1

それで、群を定義します。群は要素を持ち、うち丁度1つが単位元で、2つの元に対して丁度1つ元を定めるmultがあり、1つの元に対してその逆元を求めるinvがあるということを記述します。いま1つの群についてのみ考えたいので、「one sig Group」とすることでGroupは群を丁度1つだけ含む集合ということにします*2。NoRedundantElementsというfactで、このモデルにあらわれる要素というのはすべて群で使うものとします。この制約がないと、特に意味のない元が例に現れてしまって邪魔です。

fact UnitLaw1{
	all a: Group.elements | Group.mult [a] [Group.unit] = a
}

fact UnitLaw2{
	all a: Group.elements |
	Group.mult [Group.unit] [a] = a
}

fact AssociativeLaw{
	all a: Group.elements | all b: Group.elements | all c:Group.elements |
	Group.mult [Group.mult [a] [b]] [c] = Group.mult [a] [Group.mult [b] [c]]
}

fact InvLaw1{
	all a: Group.elements | Group.mult [Group.inv[a]] [a] = Group.unit
}

assert InvLaw2 {
	all a: Group.elements | Group.mult [a] [Group.inv[a]] = Group.unit
}

check InvLaw2

さらに、群の制約を書き足します。単位元の制約、結合則はいいのですが、逆元について制約は、「任意の元aについて、aのinvは左からかけると単位元になる」ということしか言っていません。InvLaw2は同じことを右からで言っているのですが、こちらは制約ではなくただの成り立ってほしいと思っている命題です。ここで、最後の行でこの命題が成り立つかを検査します。結果、Alloyの検査器は「多分正しい」と教えてくれます。「多分」というのはAlloyは有限個の範囲でしか検査せず、デフォルトだとすべての集合が3つ以下しか元を持たないという制約のもとで(上手に)総当たりします*3。これで、「多分正しいだろう」と人間も予想できるので証明してみます。示すことは、「任意の元bについて、ここで定義した意味でのbのinvは右からかけると単位元になる」ということ。bのinvのことを、b^{-1}と書くことにし、単位元はeで書きます。

aをいま考えている群の元とする。InvLaw1から、a^{-1}\cdot a = eとなる。同様に、(a^{-1})^{-1}\cdot a^{-1} = eとなる。よって、結合則より
a=e\cdot a = (a^{-1})^{-1}\cdot a^{-1}\cdot a = (a^{-1})^{-1}となる。よって、任意のaについてa=(a^{-1})^{-1}が成立する。

bを群の元とする。先のことから、b=(b^{-1})^{-1}となり、b\cdot b^{-1} = (b^{-1})^{-1}\cdot b^{-1} = eとなる。証明おわり。

ということでこのcheckはコメントアウトして先に進む。

次に、

run {}

で、ここまでの制約をみたすような例を表示してみます。Executeを実行して、Showをクリックすると訳のわからん図が出てきます。ここで、図のなかにGroupが出てきてるのが邪魔なので、表示画面の「Theme」をクリックして、出てくる「sig Group」を選択し、「Project over this sig」をonにして「Close」すると
f:id:sle:20170218231435p:plain
こんな感じで群が出てきます。Element1に「unit」と書いてあるので、これが単位元だとわかります。この群はもちろんZ/2Zで演算を和としたものです。
さらに、Nextをクリックすると他の例を探してくれます。いくらか押すと、位数3の群も出てきます。
若干演算がよく分からないので、「Evaluator」をクリックします。ここでは、対話型で出てきた例を調べることができます。
f:id:sle:20170218231842p:plain
ここで、「Group.mult」と叩くと演算multがどうなっているかが見えます。

もう満足したので、このrunはコメントアウトして先に進みます。

assert Commutativity{
	all a: Group.elements | all b: Group.elements | Group.mult [a] [b] = Group.mult [b] [a]
}

check Commutativity for 5

このassertは群が可換であることを意味します。そして、checkでこれが本当に成立するかどうかを確かめます。「for 5」がついていて、位数5以内でこれを確かめます。Executeを押すと「多分正しい」と出てきます。これで、この命題は多分正しそうだということになり、「全ての群は可換である」という気がしてくるのですが*4、念の為もうちょっと大きく、

check Commutativity for 6

f:id:sle:20170218233114p:plain
と変えて実行すると、「反例が見つかりました」と出てきます。すごい。

これで満足したのでcheckはコメントアウトして先に進みます。
今回私が本当に調べたかったのは、

Gを群とし、AをGの正規部分群、BはAの正規部分群とする。このとき、BはGの正規部分群か?

です。これは割と落とし穴でちょっと考えるぐらいだと分かりません。このためには、

pred subgroup (g: set Element, h: set Element){
	(all a: g | a in h) and
	(Group.unit in g) and
	(all a, b: g | Group.mult [a] [b] in g) and
	(all a: g | Group.inv[a] in g)
}

pred regularSubgroup(n: set Element, g: set Element){
	subgroup [n, g] and
	(all n0: n, g0: g | Group.mult [Group.mult [g0] [n0]] [Group.inv[g0]] in n)
}

pred main(n1: set Element, n2: set Element){
	let g = Group.elements |
	regularSubgroup [n1, g] and
	(some g0: g | (not g0 in n1)) and
	regularSubgroup [n2, n1] and
	(some n10: n1 | (not n10 in n2)) and
	(not regularSubgroup [n2, g])
}

と書きます。subgroupは要素の集合2つをとる述語で、その範囲で演算が閉じているかを確かめます。
regularSubgroupも要素の集合2つをとって、正規部分群になっているかを調べます。
mainが調べたいことで、特に意味はないのですが真の正規部分群になっているという条件もついてます。これで

run main for 7

とすると「多分正しい」となります。さらに、「for 8」としてみると、今度は反例を見つけてくれます。
f:id:sle:20170218233114p:plain
めでたしめでたし。

*1:実際どういう集合かというのは制約を見つつAlloyが探してくれるわけなので、「この集合は何?」というのを記述する必要はありません。

*2:普通の言語に慣れているとこれらは関数に見えるのですが、実際は数学で言うところの関係、つまり直積集合の部分集合になっています。ドットで普通のオブジェクト指向言語のように要素へのアクセスをしているように見えるのですが、実際は関係の推移になっています。これで望みのものが書けてしまうというのは結構面白いので是非やってみてください。

*3:ちなみに手元のマシンでデフォルト設定で探索したところ、位数15では反例を見つけられませんでしたが、20だとエラーになりました。

*4:しません

Atiyah-MacDonaldのProposition 1.11について(prime avoidance lemma, 2/13追記)

Atiyah-MacDonaldの「可換代数入門」のProposition 1.11では、

環Aとそのイデアル\frak aと素イデアル\frak p_1,\dots,\frak p_nについて、
\frak a \subset \bigcup_{i=1}^n \frak p_iとなっているとする。
このとき、あるiに対して\frak a \subset \frak p_iとなる。

ということが書いてある。この素イデアルの条件を外すと不味いのかなと思って、
n=2で反例を探していたのだがずっと見つからなかった。
しかし、今日n=2だと素イデアルの条件なしでも同様のことが言えてしまうと気づいたので書いておく。

示すことは、

環Aとそのイデアル\frak a,\frak b,\frak cについて、\frak a\subset \frak b \cup \frak cが成り立っているとする。
このとき、\frak a\subset \frak b\frak a\subset \frak cかのどちらかが成り立つ。

である。背理法で示す。仮に、
(1)\frak a\subset \frak b\cup \frak c、(2)\frak a \not\subset \frak b、(3)\frak a\not\subset \frak cのすべてが成立していたとする。
仮に、\frak b\subset \frak cだとすると、\frak b\cup \frak c = \frak cとなって(1)に反するので、(4)\frak b\not\subset \frak cである。
同様に、(5)\frak c\not\subset \frak bも成り立つ。(2)、(3)、(4)、(5)より、x \in (\frak b\setminus \frak c)\cap \frak a
y\in (\frak c\setminus \frak b)\cap \frak aが成り立つようなxとyが存在する*1x,y\in \frak aなので、(1)よりx+y\in \frak a\subset \frak b\cup \frak cとなる。
よって、x+y\in \frak bx+y\in \frak cかのどちらかは成立する。
前者が成立するとする。y=(x+y)-xだが、xは定義から、x+yは仮定より\frak bの元なので、y\frak bの元である。
これはyの定義に反し、矛盾である。後者が成立すると仮定すると同様にx\in \frak cが導かれ、矛盾する。
よって、どちらにしても矛盾する。証明おわり。

というわけで少なくともn≧3で探さないと意味がないっぽい。Alloyで探してみようと思う。

2/13追記

id:qnighyさんがn=3で例を見つけてくれました。


2次の項全部で割ってるので有限の環になってます。これならAlloyでも見つけられそう(勉強中)。
加群ぽく考えるのが大事みたいです。

あと、タイトルのprime avoidanceの説明をしてなかったのですが、このAtiyah-MacDonaldのProposition 1.11には
prime avoidanceという名前がついているようで、こんな記事https://en.wikipedia.org/wiki/Prime_avoidance_lemmaがあります。

*1:2/13修正

公式のPythonとAnacondaを共存させる(備忘録)

おもに備忘録。すでにPython3が入っていたのですが、科学計算用のライブラリのインストールがうまく行かなくて結局Anacondaを入れることにしました。そうすると、どちらのPythonにパスを通すかというのが問題になりますが、切り替えられるようにバッチを書くことにしました。そのとき、batファイルの書き方が奇っ怪で腹が立ったのでこれを機にPowerShellを使ってみることにしました。等号が-eqだったりするのが奇妙ですがはるかに良い。


gist63a91d89b1679e6e7cb91c3da8e7a76c

これを適当なパスの通った場所に置いておいて、PowerShellから「setpythonpath anaconda」とか叩けばOK。Pathのほうは、デフォルトとして使いたいほうだけパスを通しておく。

はじめはPythonPathという環境変数を作って、そこにPythonのパスを書き、Pathのほうには「%PythonPath%」と書いておけば、PythonPathを書き換えるだけで切り替えができるだろうと思っていたのですが、どこかの時点でPathのなかの%PythonPath%が展開されてしまうようで、PythonPathを書き換えても意味がありませんでした。

プログラミングコンテストチャレンジブックの分割数について

「分割数」でぐぐると同様の記事がいろいろ出てくるのだけれど、やっぱりよく分からなかったので考えたらようやっと納得がいった。なので、その記録をしておく。

まず、なんだか分からなかった原因は、「jのi分割数」というのは「jを1以上の自然数i個の和でかきあらわしたときの(順序を無視した)書き表しかたの個数」であるはずなのに、0の和も考えているようにも読めて何を考えているのだかよく分からなくなるところにあったと思う。そういうわけで、式と向き合っていたところ意図がわかった。

「jのi分割」は「jを1以上の自然数i個の和でかきあらわしたときの(順序を無視した)書き表しかた」で、これらのなす集合である「jのi分割のなす集合」を考える。
この集合を、「jのi分割のなす集合のうち、2以上のみを(1個以上)使うもの」と「jのi分割のなす集合のうち、1を(1個以上)使うもの」の2つに分ける。
すると、この2つの部分集合は交わりがなく、しかもこの2つの集合の結びは「jのi分割のなす集合」となるので、「jのi分割数」であるdp[i][j]を求めるには、この2つの部分集合それぞれの元の個数を数えればよい。

まず、「jのi分割のなす集合のうち、2以上のみを(1個以上)使うもの」の個数を考える。実は、「jのi分割のなす集合のうち、2以上のみを(1個以上)使うもの」と「(j-i)のi分割のなす集合」との間には同型対応が作れる(つまり、余りもダブりもなく、2つの集合から1つずつ選んできたペアを作ることができる)。具体的にどうするかというと、「jのi分割のなす集合のうち、2以上のみを(1個以上)使うもの」の元「2をa_2個、3をa_3個、…」に対して*1「1をa_2個、2をa_3個、…」と割り当てる。いま、i分割を考えていることから、a_2+a_3+\dots = iが成り立っており、この対応は確かにi分割をi分割に写している。さらに、jの分割を考えていることから\sum_{i\ge 2} i a_i = jとなっており、よって \sum_{i\ge 2} (i-1)a_{i}= \sum_{i\ge 2} i a_i - \sum_{i\ge 2} a_i = j - iとなる。よって、確かにjの分割を(j-i)の分割に写している。以上のことより、この対応は確かに「jのi分割のなす集合のうち、2以上のみを(1個以上)使うもの」から「(j-i)のi分割のなす集合」への写像になっている。逆の対応は明らかなので省略し、それが全単射になっていることも省略する*2。よって、「jのi分割のなす集合のうち、2以上のみを(1個以上)使うもの」の個数はdp[i][j-i]である。

次に、「jのi分割のなす集合のうち、1を(1個以上)使うもの」の個数を考える。「jのi分割のなす集合のうち、1を(1個以上)使うもの」は、その使っている1を取り除いて考えれば「jの(i-1)分割」になり、逆の対応もつけることができて同型であることがわかる。よって、「jのi分割のなす集合のうち、1を(1個以上)使うもの」の個数は「jの(i-1)分割」の個数であり、これはdp[i-1][j]である。

以上で、dp[i][j] = dp[i][j-i] + dp[i-1][j]である。

集合の分け方が一番のミソでした。

*1:「2以上のみを~」という定義から、「1を0個」使っているということに注意。つまり、「1をa_1個~」と書く必要はない。

*2:だんだん飽きてきた

米田の補題のしょうもない使用例

マクレーンを読んでて米田の補題を示したはいいが何やってるか全然わからないし、議論する階層も深すぎて何を扱ってるのかもよくわからなかったのでしょうもない
例を作った。式は
 y\colon \bf{Nat}(D(r,-),K) \simeq Krだが、右の Krから何か元をとってきてそこからどんな自然変換ができるかを見てみることにした。

それぞれの登場人物は、以下のようにする。

  •  D: モノイドの圏。 D=\bf{Mon}
  • 関手 K:  \bf{Mon}から\bf{Set}への忘却関手
  •  r: 「 \{a,b,A,B\}という4文字のアルファベットを並べた文字列」というモノイド

そして、 Krの元として文字列「 AabB」をとり、これが y^{-1}でどんな自然変換を生むかを見る。

「AabB」を使って、モノイド dを固定したときに自然変換 \alpha_dを作りたい、つまり
モノイド準同型 f\in D(r,d) \alpha_d Kdのどこに写るかを定めたい。
そのためには以下の図式を使うのだった。

f:id:sle:20151130011539p:plain

ここで、この図式の左側はモノイドの圏の図式で、右側が集合の圏の図式なことに注意する。
ここで、右の四角の左上に恒等写像 1_rを流せば、図式の可換性より
 \alpha_d(f) = (\alpha_d \circ (f\circ ?) )(1_d) = ( (Kf)\circ (\alpha_r) )(1_d) = (Kf)(\alpha_r 1_d)
となるが、この \alpha_r 1_d \in Krを今は文字列「 AabB」と定めるというのが y^{-1}
の定義だった。つまり、
 (Kf)(\alpha_r 1_d) = (Kf)("AabB")であり、
 \alpha_d(f) = (Kf)("AabB")ということになる。

具体的にこの自然性を使ってみる。
いま、「 \{a,b\}という2文字のアルファベットを並べた文字列」というモノイド (\{a,b\}, \cdot)を考える。
また、先のモノイド r (\{a,b,A,B\}, \cdot)と書くことにする。
さらに、モノイド準同型 {\bf{count}} \colon (\{a,b\}, \cdot) \to (N, +)を文字数を数えるモノイド準同型とする。
ただし、 Nは0以上の自然数。このとき、自然性より次の図式が得られる。

f:id:sle:20151130013459p:plain

ここで、この図式の左側はモノイドの圏の図式で、右側が集合の圏の図式なことに注意する。
ここで、図式の左上に、大文字を小文字に、小文字をそのままにするモノイド準同型
 {\bf {lower}} \in {\bf {Mon}}( (\{a,b,A,B\}, \cdot),(\{a,b\}, \cdot) )を入れてみる。すると、
↓→というたどりかたでは、
 
\begin{align}
(\alpha_{(N,+)}\circ ({\bf count} \circ ?) )({\bf lower}) &= \alpha_{(N,+)}( {\bf count} \circ {\bf lower}) \\
&= ({\bf count} \circ {\bf lower})("AabB")\\
&= {\bf count}("aabb")\\
&= 4.
\end{align}
一方、→↓というたどりかたでは、
 
\begin{align}
( (K{\bf count}) \circ \alpha_{(\{a,b\},\cdot)} )({\bf lower})
&=
K{\bf count}({\bf lower}("AabB") )\\
&=
K{\bf count}("aabb")\\
&=
4.
\end{align}

となり、確かに一致する。↓→での "aabb"はモノイド (\{a,b\}, \cdot)の元であり、
→↓での "aabb"は集合 \{a,bからなる文字列\}の元であることに注意する。

つまるところ、「準同型を忘却させて関数を作り、そこに『AabB』をわたす」という操作は自然である」ということになった。

忘却関手を使うとこのへんがごちゃごちゃになるしもうちょっと込み入った関手を使えばよかったのかなあ。