(*|
位相空間
========

位相空間を定義する。
|*)

Require Import category.
Require Import classical_logic.
Require Import logic.
Require Import power.
Require Import function.

Set Implicit Arguments.

(*|
定義
----
|*)

(*|
型 `A` 上の位相構造を以下のように定義する。
|*)

Record is_topology
  (A : Type)
  (is_open  : power A -> Prop)
  : Prop :=
  make_is_topology {
    top_open : is_open whole_set;

    bin_inter_open {U V} :
      is_open U ->
      is_open V ->
      is_open (U ∩ V);

    union_open {X : power (power A)} :
      (forall U, U ∈ X -> is_open U) ->
      is_open (⋃ X);
  }.

Record topology (A : Type) : Type :=
  make_topology {
    is_open : power A -> Prop;
    is_open_is_topology :> is_topology is_open;
  }.

(*|
位相構造は、``A`` の元の集合がどのようなときに開集合であるかを ``is_open`` という述語によって指定する。``A`` の元全体の集合は開集合である。開集合は2項の共通集合と、一般の合併によって閉じている。

位相空間とは、型とその上の位相の組である。
|*)

Record topological_space : Type :=
  make_topological_space {
    A :> Type;
    topology_on_A :> topology A;
  }.

(*|
閉集合を定義する。
|*)

Definition is_closed
  (X : topological_space)
  (S : power X)
  : Prop
  := X.(is_open) (complement S).

Lemma empty_open
  (X : topological_space)
  : X.(is_open) empty_set.
Proof.
  rewrite<- union_of_empty_set.
  apply X.(union_open).
  intros.
  unfold mem, empty_set in H.
  contradiction.
Qed.

(*|
例
--
|*)

(*|
どんな型も、その上に離散位相を考えることができる。
|*)

Definition discrete_topology (A : Type) : topology A.
Proof.
  exists (fun S => True).
  constructor.
  -
    simpl.
    trivial.
  -
    simpl.
    trivial.
  -
    simpl.
    trivial.
Defined.

(*|
どんな型も、その上に密着位相を考えることができる。
|*)

Lemma indiscrete_topology_is_topology
  (A : Type)
  : is_topology (fun S : power A => S = empty_set \/ S = whole_set).
Proof.
  constructor.

(*|
まず ``whole_set`` が開集合であることを示す。
|*)

  -
    right.
    reflexivity.

(*|
次に2項の共通集合で閉じていることを示す。
|*)

  -
    intros.
    destruct H.
    +
      left.
      subst U.
      apply bin_inter_empty_set_left.
    +
      destruct H0.
      *
        left.
        subst V.
        apply bin_inter_empty_set_right.
      *
        right.
        subst U V.
        apply bin_inter_left_unit.

(*|
最後に任意の合併で閉じていることを示す。
|*)

  -
    intros.
    destruct (exists_or_none (fun U => U ∈ X /\ U = whole_set)).
    +
      right.
      destruct H0 as [U [H1 H2]].
      rewrite H2 in H1.
      apply (union_whole_set H1).
    +
      left.
      apply subset_of_empty_set.
      apply union_least_upper_bound.
      intros.
      specialize (H S H1).
      specialize (H0 S).
      assert (S <> whole_set) by
        exact (uncurry_not H0 H1).
      clear H0 H1.
      apply (disj_delete_right H) in H2.
      rewrite H2.
      apply inclusion_refl.
Qed.

(*|
これで離散位相が実際に位相であることが分かった。
|*)

Definition indiscrete_topology (A : Type) : topology A.
Proof.
  exists (fun S => S = empty_set \/ S = whole_set).
  apply indiscrete_topology_is_topology.
Defined.

Print indiscrete_topology.

(*|
連続写像
--------
|*)

Definition continuous
  {A B}
  (X : topology A)
  (Y : topology B)
  (f : A -> B)
  : Prop :=
  forall U : power B,
    Y.(is_open _) U ->
    X.(is_open _) (preimage f U).

Record continuous_map
  (X Y : topological_space)
  : Type :=
  make_continuous_map {
    f :> X -> Y;
    f_is_continous :> continuous X Y f;
  }.

Lemma identity_continuous
  {A}
  (X : topology A)
  : continuous X X id_function.
Proof.
  unfold continuous.
  intros.
  unfold preimage.
  assumption.
Qed.

Definition identity_continuous_map
  (X : topological_space)
  : continuous_map X X.
Proof.
  exists id_function.
  apply identity_continuous.
Defined.

Lemma composition_continuous
  {A B C}
  {X : topology A}
  {Y : topology B}
  {Z : topology C}
  {f : A -> B}
  {g : B -> C}
  (g' : continuous Y Z g)
  (f' : continuous X Y f)
  : continuous X Z (compose_functions g f).
Proof.
  unfold continuous.
  intros.
  rewrite preimage_of_composition.
  apply f'.
  apply g'.
  assumption.
Qed.

Definition composition_continuous_map
  {X Y Z : topological_space}
  (g : continuous_map Y Z)
  (f : continuous_map X Y)
  : continuous_map X Z.
Proof.
  exists (compose_functions g f).
  apply (composition_continuous g f).
Defined.

(*|
位相空間の圏
------------
|*)

Definition displayed_category_of_topological_spaces_data
  : displayed_category_data category_of_types_data.
Proof.
  unshelve econstructor.
  -
    exact topology.
  -
    intros A B f X Y.
    exact (continuous X Y f).
  -
    simpl.
    intros.
    apply identity_continuous.
  -
    simpl.
    intros.
    apply (composition_continuous g' f').
Defined.

Print displayed_category_of_topological_spaces_data.

(*|
近傍
----
|*)

Section Neighborhoods.
  Context {X : topological_space}.

  Definition neighborhood
    (x : X)
    (N : power X)
    : Prop :=
    exists U,
    X.(is_open) U /\
    x ∈ U /\
    U ⊆ N.

  Definition open_neighborhood
    (x : X)
    (U : power X)
    : Prop :=
    X.(is_open) U /\
    x ∈ U.

  Lemma open_neighborhood_is_neighborhood
    (x : X)
    (U : power X)
    : open_neighborhood x U -> neighborhood x U.
  Proof.
    intro.
    destruct H.
    exists U.
    repeat split.
    -
      assumption.
    -
      assumption.
    -
      apply inclusion_refl.
  Qed.

  Lemma open_neighborhood_is_open_neighborhood
    (x : X)
    (U : power X) :
    X.(is_open) U ->
    neighborhood x U ->
    open_neighborhood x U.
  Proof.
    intros.
    destruct H0 as [H0 [H1 [H2 H3]]].
    split.
    -
      assumption.
    -
      apply H3.
      assumption.
  Qed.
End Neighborhoods.

(*|
分離公理
--------
|*)

Definition T1_space (X : topological_space)
  : Prop :=
  forall x : X, is_closed X (singleton x).

Definition hausdorff (X : topological_space)
  : Prop :=
  forall x y : X,
  x <> y ->
  exists U V,
  open_neighborhood x U /\
  open_neighborhood y V /\
  disjoint U V.

Lemma T1_space_separated_by_open_neighborhood
  (X : topological_space) :
  T1_space X ->
  (
    forall (x y : X),
    x <> y ->
    exists N,
    open_neighborhood x N /\
    ~ (y ∈ N)
  ).
Proof.
  intros.
  specialize (H y).
  unfold is_closed in H.
  exists (complement (singleton y)).
  split.
  -
    split.
    +
      assumption.
    +
      unfold singleton, complement, mem.
      assumption.
  -
    unfold singleton, complement, mem.
    apply double_negation_introduction.
    reflexivity.
Qed.

(*|
TODO: 以下の証明は明らかに読みにくい：
|*)

Lemma separated_by_neighborhood_T1_space
  (X : topological_space) :
  (
    forall (x y : X),
    x <> y ->
    exists N,
    neighborhood x N /\
    ~ (y ∈ N)
  ) ->
  T1_space X.
Proof.
  intro.
  unfold T1_space.
  unfold is_closed.
  intro x.

  assert (X.(is_open) (⋃ (fun S => X.(is_open) S /\ ~ (x ∈ S)))).

  -
    apply X.(union_open).
    unfold mem.
    intros.
    destruct H0.
    assumption.
  -
    assert (
      complement (singleton x) =
      ⋃ (fun S => X.(is_open) S /\ ~ (x ∈ S))
    ).
    +
      apply inclusion_antisymmetric.
      *
        intros y H1.
        unfold singleton, complement, mem in H1.
        specialize (H y x H1).
        destruct H as [N [H H2]].
        destruct H as [U [H [H3 H4]]].
        exists U.
        repeat split.
        **
           assumption.
        **
           intro.
           apply H2.
           apply H4.
           assumption.
        **
           assumption.
      *
        intros y H1.
        unfold singleton, complement, mem.
        destruct H1 as [U [H1 H2]].
        intro.
        subst y.
        unfold mem in H1.
        destruct H1.
        apply H3.
        assumption.
    +
      rewrite H1.
      apply H0.
Qed.

Lemma hausdorff_is_T1
  (X : topological_space)
  : hausdorff X -> T1_space X.
Proof.
  intro H.
  apply separated_by_neighborhood_T1_space.
  intros.
  specialize (H x y H0).
  destruct H as [U [V [H [H1 H2]]]].
  exists U.
  split.
  -
    apply open_neighborhood_is_neighborhood.
    assumption.
  -
    intro.
    unfold disjoint in H2.
    destruct H.
    destruct H1.
    specialize (H2 y H3 H5).
    assumption.
Qed.