Bernstein の続き

相互に injection (単射)な写像があれば、bijection (双射)があるって奴です。

もちろん Agda でやるわですが、可算版の方が結構手間取った。

　　ℕ ↔　 A　→　B　→　C　↔　 ℕ

でやるんですけどね。Cの中の B を下から数えて番号を付ければ良いだけなんだが、induction するには最大値を見つける必要がある。

　　Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ
　　　　 → (fi : InjectiveF A　B ) → (gi : InjectiveF　B C )
　　　　 → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c ))
　　　　 → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c)　)
　　　　 → Bijection B ℕ

それは n 番のBが欲しければ, A の方で、n 個取って、それに対応するCの番号の最大値m を取る。すると、m以下には n 個以上のBがある。

なので、m から induction で下がっていけばよいってだけですけどね。さらに、

　　bijection を示すには、Bの個数の injection を示す必要がある

これは、数えた個数が同じなら、同じBを指すってやつだが、これがけっこう微妙。ま、面白いとも言うか。

これで、
　 List (Maybe Bool) と　ℕ との bijection

とか、

　 List ℕ と ℕ

とかを(比較的)簡単に示せます。

ゲーデルナンバーみたいなものね。

　＊　＊　＊

　 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b

本家の集合論の方も、いろいろ苦労したが、結局、教科書的な証明が良いらしい。f : A → B , g : B → A で、

　 Injection と Image を定義して、
　 C 0 = A \ Image g　に対して、g (f x) の閉包を定義して、その Union (C n) を取る

すると、C n 上では f と g が　C n と f (C n) のbinjection になり

X \ C n とf (X \ C n)　の bijection には g をその逆写像が bijection になる。

と、そんな感じ。g (f (C n ))が、g (f a) しか含まないってのは当たり前だが、だから、
g は (f (C n ) 上で逆写像があるという論法は、まぁ、面白い。


　＊　＊　＊

で、この可算版と、非可算版が関係あるんじゃないかって話ね。可算モデルを考えれば当然なんだが。

証明的には、可算の方が難易度は高い。 可算側は構成的に bijection が得られるしね。

集合側の Union (C n) を C n を必要な部分だけ計算するとすると可算側の証明に近くなる。