Filter

数学の概念、Ideal の双対だってのを割と最近知ったのは残念。集合論の選択公理連続体仮説が成立しないモデルを作る時に使います。

超実数を定義するのにも使うな。

集合論を手に入れたので楽勝で書けると思ったんですが、

　　本によって書き方が違う

Kunen とか二ヶ所に書いてあって、ちょっと違う。∃を使うか∀を使うかと、集合でやるか順序構造でやるかの違いらしい。

Agda だと ∃ は扱いにくいので、∀ を使う方が良いみたい。ultra filter なら prime filter ってのを証明できたのでそれっぽくできたみたい。

去年の10月に書いたのがだいたい正しかったようだな。本読んでる時には「はいはい」みたいに理解してたが、いざ証明してみると時間がかかる。

だいぶ馬鹿になってるかもね。ZFSet でやらずに OD でやってるが、原理的にはZFでできるはずです。

どこまでやるかは割と謎です。練習な感じ。

　　record Filter　( L : OD　) : Set (suc n) where
　　　 field
　　　　　 filter : OD　
　　　　　 f⊆PL :　filter ⊆ Power L
　　　　　 filter1 : { p q : OD } →　q ⊆ L　→ filter ∋ p →　p ⊆ q　→ filter ∋ q
　　　　　 filter2 : { p q : OD } → filter ∋ p →　filter ∋ q　→ filter ∋ (p ∩ q)

　　record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
　　　 field
　　　　　 proper　: ¬ (filter P ∋ od∅)
　　　　　 prime　 : {p q : OD } →　filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )

　　record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
　　　 field
　　　　　 proper　: ¬ (filter P ∋ od∅)
　　　　　 ultra　 : {p : OD } → p ⊆ L →　( filter P ∋ p ) ∨ (　filter P ∋ ( L ＼ p) )

　　record Ideal　( L : OD　) : Set (suc n) where
　　　 field
　　　　　 ideal : OD　
　　　　　 i⊆PL :　ideal ⊆ Power L
　　　　　 ideal1 : { p q : OD } →　q ⊆ L　→ ideal ∋ p →　q ⊆ p　→ ideal ∋ q
　　　　　 ideal2 : { p q : OD } → ideal ∋ p →　ideal ∋ q　→ ideal ∋ (p ∪ q)