位相空間論の続き

チコノフ(Compact 空間の直積は積位相に関してCompact)の続き

　Compact ⇔ 有限交叉 ⇔　任意の超フィルターが収束 (A)

で、積空間の任意の超フィルターの射影を取ると収束先が分かるので、収束を示せば良いらしい。

定義が多くてね。このフィルターFの収束ってのが「P∋limitがあって、limitの近傍をFが含む」っていう意味。

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

record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) )
　　(ultra : ultra-filter F ) : Set (suc (suc n)) where
　field
　　limit : Ordinal
　　P∋limit : odef P limit
　　is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v)

いや、今年初めて知りました。学部時代の自分に「読めよ!」って思った。xの近傍の定義が、

　xを含む開集合oがあって、それを含むPの部分集合uの集合

record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where
　field
　　u : Ordinal
　　ou : odef (OS TP) u
　　ux : odef (* u) x
　　v⊆P : * v ⊆ P
　　u⊆v : * u ⊆ * v

いや長いし。位相空間の基底、フィルター基、近傍と似たようなものがたくさん。

収束の定義が間違っていたのが片付いたので、A まで Agda で書き終わりました。Zorn の補題を使うのは

　有限交叉 →　任意の超フィルターが収束

ここだけ。なぜか、呼び出すと agda でのチェックに1分かかる。外すと数秒。Zorn 自体はすぐ終わるようになった。

謎すぎる。普段は外してるんだが、入れる入れないでcheckに差がある。こまったもんだ。

残りはチコノフの定理本体だな。いきなり、フィルターの射影の定義を間違えていたが、割とすぐに片付くんじゃないか?!

Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ　→ Compact (ProductTopology TP TQ)
Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
　 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F)
　　　 → UFLP (ProductTopology TP TQ) F UF
　...

いや、Zorn の補題もそんなこと言ってて9ヶ月もかかったんですけどね。