Zorn の補題

Generic Filter は書けたんですが、どうも、Filter から Ultra Filterを作るのには、Zornの補題がいるらしく。

Filterってのは、Pの部分集合をいくつか集めたものなんですが、それの極大集合をとる必要があるわけね。

Zron の補題は、学部の頃、読んだんですがさっぱりわからず。その頃は選択公理無視派だったので、それですましてしまったらしい。

で、定義から見直す羽目になってるわけですが、

　　半順序な集合Aで、すべての空でない全順序部分集合L⊆Aの上界sup(L)∈Aがあれば極大元xが存在する。

で、さっぱりわからない。そもそも、x<0 とか極大元ないじゃん。と思ったんですが、

　　いや、それは x<0 という全順序部分集合に上界がないからだ

とわかった瞬間にばっちり見えました。集合ってのは順序数なんだが、それは一次元的な構造を持っていて、

　　上界がないのは極限順序数の直下にある無限鎖だけ

つまり Zorn の補題の仮定「全順序部分集合L⊆Aの上界がある」は、それを禁止しているだけなのね。

いや学部時代の自分に教えてやりたいです。実際の証明は、そこそこめんどい(まだAgdaで書けてない)。

そもそも書いてない本が多い。シンガーソープと公理的集合論にはなくて、岩波現代数学概説Iと「選択公理と数学」には長いのがある。

新井先生の数学基礎論のはなんかかっこいい証明なんですが全然読めなかったんだが、わかったら読めた。そんなもんです。

nlab の証明も結構長くてあれなんですが、もしかすると、もう少し簡単に書けるかも。

チコノフの定理が極大Filterの存在なので、

　　もしかして、Zornの補題の直積がチコノフの定理なんじゃないか?

と思ったら、そういうものらしい。プロシンでは「今年はチコノフやるかも」とか言ってたんですがなんとなくできそう。

https://ncatlab.org/nlab/show/Zorn%27s+lemma