日々の流転

λ. 特急あずさって

トラベルミステリーの中だけの存在じゃなくて、ちゃんと実在したのか(ぉ　今日初めて見た。

λ. Algebraic dcpo + 2/3 SFP + Scott位相 ⇒ Spectral algebraic space

Topology Via Logic の Lemma 9.3.7 に一週間くらい悩んでいたのだが、ようやく理解できた……気がする。

問題

この補題の中身は次のようなもの。

Let P be a poset satisfying the 2/3 SFP property of 9.3.6 (ii). Then Idl(P) with its Scott topology is a spectral algebraic space.

ただ、2/3 SFP property を満たすべきなのは P ではなく Idl(P) ではないかと思う。でないと話が繋がらない。

方針

Proposition 9.2.5 の

A topological space is spectral iff

• it is sober (localic),
• any finite intersection of compact open sets is still compact, and
• the compact open sets form a basis.

を使ってspectralであることを示す。

algebraicであることは普通に示す。

↑↓x はスコット開集合

Proposition 9.1.2 より ↓x は Idl(P) のコンパクトな要素で、 Definition 9.1.1 より ↑↓x はスコット開集合。

↑↓x は compact coprime open

↑↓x ⊆ ⋃S と仮定する。 このとき、↓x ∈ ⋃S なので、ある a∈S が存在して ↓x ∈ a 。 a は upper-closed なので、↑↓x ⊆ a 。

よって、↑↓x は compact coprime open 。

{↑↓x | x∈P} はスコット位相の基底

スコット開集合 a が与えられたとする。

b = ⋃{↑↓x | x∈P, ↑↓x⊆a} とおき a=b を示せば良い。 a⊇b は自明なので、a⊆b だけ示す。

y∈a が与えられたとする。 Idl(P)の代数性より S={↓x | x∈P, ↓x⊑y} とおくと y=⨆^↑S 。 スコット開集合 a は directed-join によって到達不能なので、 ある ↓x∈S が存在して ↓x∈a 。 aはupper-closedなので ↑↓x⊆a であり、bの定義から ↑↓x⊆b 。 一方、↓x⊑y より y∈↑↓x なので y∈b となる。

これでコンパクト開集合が基底になっていることが示せた。

コンパクト開集合は有限個の ↑↓x の和集合

コンパクト開集合 c が与えられたとする。 S={↑↓x | x∈P, ↑↓x⊆c} とおくと、 c=⋃S となる。 Sはcの開被覆なので、cのコンパクト性からSの有限部分集合Tが存在して c⊆⋃T。 c⊇⋃T は明らかなので c=⋃T。

コンパクト開集合が有限個の compact coprime open の和集合で表現できたので、この空間が spectral なら spectral algebraic であることが示せた。

コンパクト開集合の有限個のintersectionはコンパクト

まず、binaryな場合について。 コンパクト開集合 a, b が与えられたとする。 このとき有限集合 S, T が存在して、a = ⋃{↑↓x | x∈S}, b = ⋃{↑↓y | y∈T} であり、分配則から a∩b = ⋃{↑↓x∩↑↓y | (x,y)∈S×T} 。 S×T は有限であり、有限個の和集合ではコンパクト性は保存されるので、↑↓x∩↑↓y がコンパクトであることを示せば十分。

S={↓x, ↓y} に 2/3 SFP property を適用して、その complete set of upper bounds M が得られる。 そして、 w∈↑↓x∩↑↓y ⇔ ↓x⊑w and ↓y⊑w ⇔ ∃↓z∈M. ↓z⊑w ⇔ ∃↓z∈M. w∈↑↓z ⇔ w∈⋃{↑↓z | ↓z∈M} なので、↑↓x∩↑↓y = ⋃{ | ↓z∈M} が言える (2/3 SFP と algebraicity よりwがコンパクトでない場合についても問題ない)。 ↑↓x∩↑↓y は、有限個のコンパクト開集合の和集合として表せたので、コンパクト開集合。

この空間はSober

Idl(P) は preorder ではなく poset なので、この空間は T₀ であり、区別不可能な点は存在しない。 後は、この空間をlocalifyした空間の点に対応する点が、Idl(P)に元から含まれていることを示すだけ。

localifyした空間の点zが与えられているとする。 I={x∈P | z ⊨ ↑↓x} が目的の点であることを示す。 イデアルの条件のうち、lower-closedであることは明らかなので、finite-joinに関して閉じていることを示す。

SをIの有限部分集合とし、M⊆PをSのcomplete set of upper boundsとする。 w∈⋃{↑↓x | x∈S} ⇔ ∀x∈S. ↓x⊑w ⇔ ∃y∈M. ↓y⊑w ⇔ ∃y∈M. w∈↑↓y ⇔ w∈⋃{↑↓y | y∈M} より、⋂{↑↓x | x∈S}=⋃{↑↓y | y∈M} 。 z ⊨ ⋃{↑↓x | x∈S}=⋃{↑↓y | y∈M} より、あるy∈Mが存在して、z ⊨ ↑↓y 。よって、Iの定義より y∈I で、また y∈M はSのupper-boundであった。ゆえに、Iはイデアル。

λ. 無人駅とSuica/Pasmo

某駅にこんなのがあった。 無人駅っぽいところでもSuica/Pasmoを使えることに感動。

湘南モノレールもSuica/Pasmoが使えるようになれば良いのに、と思った。 色々難しそうだが。例えば、この路線の場合、ほとんどの利用者は有人の駅と無人の駅の間の移動だろうけど、モノレールの場合には無人駅の間の移動も結構ありそうだし。