日々の流転

λ. 大分三日目

10:00〜20:30の勤務は結構長い。 労働っぽい事はまだ何もしていないが、疲れた。 明日・明後日は休みなのでゆっくりしたい。

昨日、Air-Edgeだと Google Maps が結構重いと書いたが、これはFirefoxの場合でIEだと平気だった。Firefoxだとラスタ画像を使うのに対して、IEだとベクトル画像(VML?)を使ってるのか。

shelarcyさんの「Haskellで学ぶ並列プログラミング(その1)」とsoutaroさんの「それPraggerでできるよ! - Ruby版Plagger登場」を読んだ。

そういえば、浮世ではGaucheNightや第7回仮想化実装技術勉強会が行われている頃か。羨ましいものだ。

アイぶんぶん広場

λ. Chapter 9 の練習問題2

D を spectral locale とすると、

1. Dのスコット開フィルタはKΩDのフィルタに対応し、
2. Dの点はKΩDの素フィルタに対応する。

証明

P = KΩD とおくと ΩD=Idl(P) となるので、練習問題1 の対応を利用する。

Idl(P)のスコット開集合Fと、Pのupper-closedな部分集合Gが対応しているとする。 1を示すためには、FがフィルタであることとGがフィルタであることが同値であることを示せばよい。

• Fがフィルタだとする。 T⊆Gが有限集合ならば S={↓y | y∈T}⊆F も有限集合であり、Fはフィルタなので ⋀S∈F 。↓⋀T=⋀S∈F=ψ(G) より ∃x∈G. ↓x≦↓⋀T で ∃x∈G. x≦⋀T 。Gはupper-closedなので ⋀T∈G 。よってGはフィルタ。
• Gがフィルタだとする。 S⊆Fが有限集合ならば、T={c | ↓c∈S}⊆G も有限集合であり、Gはフィルタなので ⋀T∈G 。⋀T∈G=φ(F) より ↓⋀T∈F で、 ↓⋀T=⋀Sなので ⋀S∈F 。よってFはフィルタ。

2を示すのは簡単。 pt D ≅ Frames(Idl(P), 2) ≅ DistributiveLattices(P, |2|) なので、分配束の準同型射 P→2 について考えればよい。

• 分配束の準同型射 f: P→2 の true-kernel F={x∈P | f(x)=true} が素フィルタに対応することを示す。束の準同型であることから、有限集合 S⊆P について f(⋁S)=⋁{f(x) | x∈S} 。各x∈Sについてf(x)=falseであれば、f(⋁S)=falseなので、Fは素。
• 逆に素フィルタFが与えられたとき、f(x) = if x∈F then true else false が分配束の準同型になっていることを示す。S⊆Pを有限集合として:
  • Fは素フィルタなので f(⋁S)=true ならば ∃x∈S. f(x)=true 。
  • フィルタはupper-closedなので、∃x∈S. f(x)=true ならば f(⋁S)=true 。
  • フィルタはfinite-meetについて閉じているので、∀x∈S. f(x)=true ならば f(⋀S)=true
  • フィルタはupper-closedなので、f(⋀S)=true ならば ∀x∈S. f(x)=true