積位相

結局、トポロジーに手をつけてるんだけど、チコノフやるなら、積位相書かないと。

record Topology　( L : HOD ) : Set (suc n) where
　 field
　　　 OS　　: HOD
　　　 OS⊆PL :　OS ⊆ Power L
　　　 o∩ : { p q : HOD } → OS ∋ p →　OS ∋ q　　　→ OS ∋ (p ∩ q)
　　　 o∪ : { P : HOD }　→　P ⊂ OS　　　　　　　　→ OS ∋ Union P

これの直積だろって思ったんだが、直積の方を見たら、Zornの補題やりまくったせいで、だいぶ見通しが良くなってて、
劇的に簡単に。ところが...

　　積位相って単なる開集合の直積じゃない

え。まぁ、それでも位相空間にはなるらしいんだが。最弱じゃないとかあるらしい。

まぁ、PとQの直積空間をP方向Q方向に短冊みたいに、Pの開集合とQ全体の直積みたいにすれば良いらしい。

のだが、いざ Topology 書いてみるとぜんぜんできない。で、諦めて、少しぐぐって定義をみたら、

　　準開基から生成する

とかある。しかも証明は「明らか」。くそ〜　準開基自体は、集合の可算回の∩ってだけなので瞬殺だったんですが、
開基の生成が意味不明。Union (Power P)かと思ったら、OS ∋ Union P が、まったく出てこない。P ⊂ OS でなくて、P ⊆ OS
でやってたとかもあったんですが(それだと絶対できない)。

しかたないので、教科書に戻って開基からの生成を見直すと、

　　OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P →　x ∈ b ⊂ U }

とある。これが、どうして生成になってるのかわからなかったんですが、Uのすべての点に対して、Uの中にある
(b ⊆ U でもよい) 準開基を使うわけね。

結局、こうらしい。

record Base (L P : HOD) (u x : Ordinal) : Set n where
　 field
　　　 b　 : Ordinal
　　　 u⊂L : * u ⊆ L
　　　 sb　: Subbase P b
　　　 b⊆u : * b ⊆ * u
　　　 bx　: odef (* b) x

SO : (L P : HOD) → HOD
SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = ? ; <odmax = ? }

record IsSubBase (L P : HOD) : Set (suc n) where
　 field
　　　 P⊆PL　: P ⊆ Power L

これで、あら不思議、準開基から位相を生成できた。

　　GeneratedTopogy : (L P : HOD) → IsSubBase L P　→ Topology L

いや、簡単とはいえないけど。P ⊆ Power L だけから、Topology L 作れるとか、すごすぎないですか。

積位相も以下の準開基から簡単に生成できました。

record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
　 field
　　　 p q : Ordinal
　　　 op : odef (OS TP) p
　　　 prod : x ≡ & (ZFP (* p) Q )

record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
　 field
　　　 p q　: Ordinal
　　　 oq : odef (OS TQ) q
　　　 prod : x ≡ & (ZFP P (* q ))

base : {P Q : HOD} → Topology P → Topology Q → HOD
base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }

生成は一発

_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
_Top⊗_ {P} {Q} TP TQ =　GeneratedTopogy (ZFP P Q) (base TP TQ) ?

https://github.com/shinji-kono/zf-in-agda/blob/master/src/Topology.agda