チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

Coq で位相空間

前々回の記事「Coq でモジュラー束」で「群 G の部分群を述語 G -> Prop で表す」という方針を採用したところ、割と上手くいくということがわかりました。今回は他の題材として、「連結集合の連続写像による像は連結」であることを、同じ方針により証明してみます。大学の学部で習う定番問題ですね。証明付きの完全なコードは https://gist.github.com/4466805 です。

とりあえず概念を準備しよう

位相空間

「X の部分集合」の型をいちいち X -> Prop の形で書くと冗長になるため、シノニムを付けておきます。

Definition Subset (X : Set) : Type := X -> Prop.

また、開集合系の公理を記述するために必要な、X 自身、空集合、共通部分、和集合をそれぞれ定義しておきましょう。ここで、(X の) 空集合として

Definition empty (X : Set) : Subset X := fun (x : X) => x <> x.

としました。任意の x : X に対して ~ x <> x が成立することは、等号の反射性 eq_refl を用いて容易に示すことができます。また、開集合系の公理として「任意個の開集合の和集合」を表現する必要があるため、任意の添字付けに対する共通部分 bigcap と和集合 bigcup を先に定義しておき、2 個の場合 intsec と union はその特殊な場合として表しています。bigcap は今回は使い途がありませんでしたが。

以上を踏まえて、X が 位相 Open を備えた位相空間であることを、次のように表しました。

Class TopSpace (X : Set) (Open : Subset X -> Prop) := {
    TS_whole :
        Open (whole X);
    TS_empty :
        Open (empty X);
    TS_intsec :
        forall U1 U2 : Subset X,
        Open U1 -> Open U2 ->
        Open (intsec U1 U2);
    TS_union :
        forall (I : Set) (index : I -> Subset X),
        (forall i : I, Open (index i)) ->
        Open (bigcup I index)
}.
連続写像

逆像 preimage を用いて連続写像の定義を書きます。「任意の開集合の逆像が開なら連続」というやつですね。特に問題はなく、至って教科書通り。

Definition preimage {X Y : Set}
                    (f : X -> Y) (V : Subset Y) : Subset X :=
    fun (x : X) => V (f x).

Class Continuous (X : Set) (XOpen : Subset X -> Prop)
                 (Y : Set) (YOpen : Subset Y -> Prop)
                 (f : X -> Y) := {
    Conti_TopSpace_l :>
        TopSpace X XOpen;
    Conti_TopSpace_r :>
        TopSpace Y YOpen;
    Conti_preim :
        forall V : Subset Y,
        YOpen V -> XOpen (preimage f V)
}.
連結集合

さて、今回の主題である連結集合の定義です。

Class Connected (X : Set) (Open : Subset X -> Prop)
                (S : Subset X) := {
    Conn_TopSpace :>
        TopSpace X Open;
    Conn_insep :
        forall U1 U2 : Subset X,
        Open U1 -> Open U2 -> incl S (union U1 U2) ->
        (exists x1 : X, (intsec S U1) x1) ->
        (exists x2 : X, (intsec S U2) x2) ->
        exists x : X, intsec S (intsec U1 U2) x
}.

定義を書く上で、部分集合への所属を Prop で表現している関係上、否定 ~ の出現は避けたいところです。通常、連結空間の定義としては「S がふたつの (S の) 開集合の非交和として表せない」という言い回しが採用されることが多いですが、これを「S がふたつの開集合 U1 と U2 の和として表されればそれは非交和ではない」と表現することにして、さらに「共通部分が空でない」ことを「実際に元が存在する」として否定表現を回避してあります。

それから証明しよう

さて、本題の証明に入りましょう。(X, XOpen) と (Y, YOpen) を位相空間、f : X -> Y を連続写像とし、X の連結部分集合 U の像 f(U) の連結性を示します。

Variables X Y : Set.
Variable XOpen : Subset X -> Prop.
Variable YOpen : Subset Y -> Prop.
Hypothesis X_TopSpace : TopSpace X XOpen.
Hypothesis Y_TopSpace : TopSpace Y YOpen.
Variable f : X -> Y.
Hypothesis f_Continuous : Continuous X XOpen Y YOpen f.
Variable U : Subset X.
Hypothesis U_Connected : Connected X XOpen U.

Instance image_Connected : Connected Y YOpen (image f U).

ちなみに証明の中身は、次のような感じ。なんと言うか、特にひねったところもないスタンダードな証明です。

  1. V1 と V2 を、f(U) を覆う Y の開集合とする。
  2. U の連結性から、U と f^{-1} (V1) と f^{-1} (V2) の共通部分は空でなく、ここから元 x が取れる。実際、
    • f の連続性より f^{-1} (V1) と f^{-1} (V2) は開。
    • f(U) が V1 と V2 の和集合に含まれることから、U は f^{-1} (V1) と f^{-1} (V2) の和集合に含まれる。
    • f(U) と V1、V2 それぞれとの共通部分が空でないため、 U と f^{-1} (V1)、f^{-1} (V2) それぞれの共通部分も空でない。
  3. f(x) は f(U) と V1 と V2 の共通部分に属する。よってこの共通部分は空でない。

その他補足

今回の題材、本当は「コンパクト集合の連続写像による像はコンパクト」を証明しようかと思ったのですが、残念ながら上記の定式化では有限交叉性が上手く表現できません。FSet モジュール辺りが有望でしょうか。いずれこちらのネタもやってみたいものですが、それはまた別の話。