トポロジー

なんとなく来年はチコノフの定理やろうと思っていたのだが少し書いてみました。

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

これは filter に似てるな。

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

実際、コンパクトが超フィルターが集積点を持つことに対応するらしい。量は多いけどできそうな感じ。

別に集合でやらなくても良くて束上でやるとか自然数上でやるとかでも。ただ集合論も基数できてないし、トポスもやってないし。

群論も正規部分群とかやってないんだよな。いろいろ老後の楽しみがたまっていく感じ。