andrejbauer · November 28, 2023 19:40 · Jun 4, 2014 · Jun 4, 2014 · Jun 4, 2014 · Jun 3, 2014
diff --git a/topology.v b/topology.v
@@ -23,6 +23,10 @@ Definition subset {A : Type} (u v : P A) :=
 
 Notation "u <= v" := (subset u v).
 
+(* Disjointness. *)
+Definition disjoint {A : Type} (u v : P A) :=
+  forall x, ~ (u x /\ v x).
+
 (* We are going to write a lot of statements of the form
    [forall x : A, U x -> P] and we'd like to write
    them in a less verbose manner. We introduce a notation
@@ -33,12 +37,6 @@ Notation "'all' x : U , P" := (forall x, U x -> P) (at level 20, x at level 99).
 (* Similarly for existence. *)
 Notation "'some' x : U , P" := (exists x, U x /\ P) (at level 20, x at level 99).
 
-(* We will assume extensionality of subsets. *)
-Axiom ext : forall (A : Type) (u v : P A),
-   u <= v -> v <= u -> u = v.                  
-
-Hint Resolve ext : core.
-
 (* Arbitrary unions and binary intersections *)
 
 Definition union {A : Type} (S : P (P A)) :=
@@ -56,13 +54,6 @@ Definition empty {A : Type} := { x : A | False }.
 
 Definition full {A : Type} := { x : A | True }.
 
-(* Some basic lemmas. *)
-
-Lemma full_inter {A : Type} (u : P A) : full * u = u.
-Proof.
-  apply ext ; firstorder.
-Qed.
-
 (* A topology in a type [A] is a structure which consists
    of a family of subsets (called the opens), satisfying
    the usual axioms. In Coq this amounts to the following
@@ -97,7 +88,7 @@ Definition hausdorff {A : Type} (T : topology A) :=
   forall x y : A,
   x <> y ->
     some u : T, some v : T,
-      (u x /\ v y /\ u * v = empty).
+      (u x /\ v y /\ disjoint u v).
 
 (* A discrete space is Hausdorff. *)
 Lemma discrete_hausdorff {A : Type} : hausdorff (discrete A).
@@ -106,11 +97,9 @@ Proof.
   exists { z : A | x = z } ; split ; [exact I | idtac].
   exists { z : A | y = z } ; split ; [exact I | idtac].
   repeat split ; auto.
-  apply ext.
-  - intros z [? ?].
-    absurd (x = y) ; auto.
-    transitivity z ; auto.
-  - firstorder.
+  intros z [? ?].
+  absurd (x = y) ; auto.
+  transitivity z ; auto.
 Qed.
 
 (* Every Hausdorff space is T1. *)
@@ -121,9 +110,7 @@ Proof.
   destruct (H x y N) as [u [? [v [? [? [? G]]]]]].
   exists u ; repeat split ; auto.
   intro.
-  absurd (empty y) ; auto.
-  rewrite <- G.
-  split ; auto.
+  absurd (u y /\ v y) ; auto.
 Qed.
 
 (* Indiscrete topology. A classical mathematician will be tempted to use
@@ -136,11 +123,13 @@ Proof.
   exists { u : P A | forall x : A, u x -> (forall y : A, u y) } ; firstorder.
 Defined.
 
-(* Let us prove that the indiscrete topology is the least one. *)
+(* Let us prove that the indiscrete topology is the least one.
+   We seem to need extensionality for propositions. *)
 Lemma indiscrete_least (A : Type) (T : topology A) :
-  all u : indiscrete A, T u.
+  (forall (X : Type) (s t : P X), s <= t -> t <= s -> s = t) ->
+  indiscrete A <= T.
 Proof.
-  intros u H.
+  intros ext u H.
   (* Idea: if u is in the indiscrete topology then it is the union of all
      T-opens v which it meets. *)
   assert (G : (u = union { v : P A | T v /\ some x : v, u x })).

diff --git a/topology.v b/topology.v
@@ -15,6 +15,8 @@ Definition P (A : Type) := A -> Prop.
    sums, so this is not a problem. *)
 Notation "{ x : A | P }" := (fun x : A => P).
 
+Definition singleton {A : Type} (x : A) := { y : A | x = y }.
+
 (* Definition and notation for subset relation. *)
 Definition subset {A : Type} (u v : P A) :=
   forall x : A, u x -> v x.
@@ -147,3 +149,124 @@ Proof.
     + intros x [v [[? [y [? ?]]] ?]] ; now apply (H y).
   - rewrite G ; apply union_open ; firstorder.
 Qed.
+
+(* Particular point topology, see
+   http://en.wikipedia.org/wiki/Particular_point_topology, but of course
+   without unecessary excluded middle.
+*)
+Definition particular {A : Type} (x : A) : topology A.
+Proof.
+  exists { u : P A | (exists y, u y) -> u x } ; firstorder.
+Qed.
+
+(* The topology generated by a family B of subsets that are
+   closed under finite intersections. *)
+Definition base {A : Type} (B : P (P A)) : 
+  B full -> (all u : B, all v : B, B (u * v)) -> topology A.
+Proof.
+  intros H G.
+  exists { u : P A | forall x, u x <-> some v : B, (v x /\ v <= u) }.
+  - firstorder.
+  - firstorder.
+  - intros u Hu v Hv x.
+    split.
+    + intros [Gu Gv].
+      destruct (proj1 (Hu x) Gu) as [u' [? [? ?]]].
+      destruct (proj1 (Hv x) Gv) as [v' [? [? ?]]].
+      exists (u' * v') ; firstorder.
+    + intros [w [? [? ?]]].
+      split ; now apply H2.
+  - intros S K x.
+    split.
+    + intros [u [H1 H2]].
+      destruct (K u H1 x) as [L1 _].
+      destruct (L1 H2) as [v ?].
+      exists v ; firstorder.
+    + firstorder.
+Defined.
+
+Require Import List.
+
+(* The intersection of a finite list of subsets. *)
+Definition inters {A : Type} (us : list (P A)) : P A :=
+  {x : A | Forall (fun u =>  u x) us }.
+
+(* The closure of a family of sets by finite intersections. *)
+Definition inter_close {A : Type} (S : P (P A)) :=
+  { v : P A | some us : Forall S , (forall x, v x <-> inters us x) }.
+
+Lemma Forall_app {A : Type} (l1 l2 : list A) (P : A -> Prop) :
+  Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).
+Proof.
+  induction l1 ; simpl ; auto.
+  intros H G.
+  constructor.
+  - apply (Forall_inv H).
+  - apply IHl1 ; auto.
+    inversion H ; assumption.
+Qed.
+
+Lemma Forall_app1 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
+  Forall P (l1 ++ l2) -> Forall P l1.
+Proof.
+  induction l1 ; simpl ; auto.
+  intro H.
+  inversion H ; auto.
+Qed.
+
+Lemma Forall_app2 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
+  Forall P (l1 ++ l2) -> Forall P l2.
+Proof.
+  induction l1 ; simpl ; auto.
+  intro H.
+  inversion H ; auto.
+Qed.
+
+(* The topology generated by a subbase S. *)
+Definition subbase {A : Type} (S : P (P A)) : topology A.
+Proof.
+  apply (base (inter_close S)).
+  - exists nil ; firstorder using Forall_nil.
+  - intros u [us [Hu Gu]] v [vs [Hv Gv]].
+    exists (us ++ vs).
+    split ; [ (now apply Forall_app) | idtac ].
+    split.
+    + intros [? ?].
+      apply Forall_app ; firstorder.
+    + intro K ; split.
+      * apply Gu.
+        apply (Forall_app1 _ _ _ K).
+      * apply Gv.
+        apply (Forall_app2 _ _ _ K).
+Defined.
+
+(* A subbasic set is open. *)
+Lemma subbase_open {A : Type} (S : P (P A)) (u : P A) :
+  S u -> (subbase S) u.
+Proof.
+  intros H x.
+  split.
+  - intro G.
+    exists u ; split ; [ idtac | firstorder ].
+    exists (u :: nil).
+    split ; [now constructor | idtac].
+    intro y ; split.
+    + intro ; now constructor.
+    + intro K.
+      inversion K ; auto.
+  - firstorder.
+Qed.
+
+(* The cofinite topology on A. *)
+Definition cofinite (A : Type) : topology A :=
+  subbase { u : P A | exists x, forall y, (u y <-> y <> x) }.
+
+(* The cofinite topology is T1. *)
+Lemma cofinite_T1 (A : Type) : T1 (cofinite A).
+Proof.
+  intros x y N.
+  exists { z : A | z <> y }.
+  split ; auto.
+  apply subbase_open.
+  exists y ; firstorder.
+Qed.
diff --git a/topology.v b/topology.v
@@ -122,4 +122,28 @@ Proof.
   absurd (empty y) ; auto.
   rewrite <- G.
   split ; auto.
-Qed.
+Qed.
+
+(* Indiscrete topology. A classical mathematician will be tempted to use
+   disjunction: a set is open if it is either empty or the whole set. But
+   that relies on excluded middle and generally causes trouble. Here is
+   a better definition: a set is open iff as soon as it contains an element,
+   it is the whole set. *)
+Definition indiscrete (A : Type) : topology A.
+Proof.
+  exists { u : P A | forall x : A, u x -> (forall y : A, u y) } ; firstorder.
+Defined.
+
+(* Let us prove that the indiscrete topology is the least one. *)
+Lemma indiscrete_least (A : Type) (T : topology A) :
+  all u : indiscrete A, T u.
+Proof.
+  intros u H.
+  (* Idea: if u is in the indiscrete topology then it is the union of all
+     T-opens v which it meets. *)
+  assert (G : (u = union { v : P A | T v /\ some x : v, u x })).
+  - apply ext.
+    + intros x ?. exists full ; firstorder using full_open.
+    + intros x [v [[? [y [? ?]]] ?]] ; now apply (H y).
+  - rewrite G ; apply union_open ; firstorder.
+Qed.
diff --git a/topology.v b/topology.v
@@ -0,0 +1,125 @@
+(* How do to topology in Coq if you are secretly an HOL fan.
+   We will not use type classes or canonical structures because they
+   count as "advanced" technology. But we will use notations.
+ *)
+
+(* We think of subsets as propositional functions.
+   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
+   [U x] means "[x] is an element of [U]".
+*)
+Definition P (A : Type) := A -> Prop.
+
+(* A subset is in general defined as [fun x : A => ...]. We introduce
+   a more familiar subset notation. NB: We are overriding Coq's standard
+   notation for dependent sums. Luckily, we are not going to use dependent
+   sums, so this is not a problem. *)
+Notation "{ x : A | P }" := (fun x : A => P).
+
+(* Definition and notation for subset relation. *)
+Definition subset {A : Type} (u v : P A) :=
+  forall x : A, u x -> v x.
+
+Notation "u <= v" := (subset u v).
+
+(* We are going to write a lot of statements of the form
+   [forall x : A, U x -> P] and we'd like to write
+   them in a less verbose manner. We introduce a notation
+   that lets us write [all x : U, P] -- Coq will figure
+   out what [A] is. *)
+Notation "'all' x : U , P" := (forall x, U x -> P) (at level 20, x at level 99).
+
+(* Similarly for existence. *)
+Notation "'some' x : U , P" := (exists x, U x /\ P) (at level 20, x at level 99).
+
+(* We will assume extensionality of subsets. *)
+Axiom ext : forall (A : Type) (u v : P A),
+   u <= v -> v <= u -> u = v.                  
+
+Hint Resolve ext : core.
+
+(* Arbitrary unions and binary intersections *)
+
+Definition union {A : Type} (S : P (P A)) :=
+  { x : A | some U : S , U x }.
+
+Definition inter {A : Type} (u v : P A) :=
+  { x : A | u x /\ v x }.
+
+(* Infix notation for intersections. *)
+Notation "u * v" := (inter u v).
+
+(* The empty and the full set. *)
+
+Definition empty {A : Type} := { x : A | False }.
+
+Definition full {A : Type} := { x : A | True }.
+
+(* Some basic lemmas. *)
+
+Lemma full_inter {A : Type} (u : P A) : full * u = u.
+Proof.
+  apply ext ; firstorder.
+Qed.
+
+(* A topology in a type [A] is a structure which consists
+   of a family of subsets (called the opens), satisfying
+   the usual axioms. In Coq this amounts to the following
+   definition. The mysterious [:>] means "automatically
+   coerce from the topology structure to its opens". This
+   is useful as it lets us write [U : T] instead of
+   [U : opens T].
+*)
+
+Structure topology (A : Type) := {
+  open :> P A -> Prop ;
+  empty_open : open empty ;
+  full_open : open full ;
+  inter_open : all u : open, all v : open, open (u * v) ;
+  union_open : forall S, S <= open -> open (union S)
+}.
+
+(* The discrete topology on a type. *)
+Definition discrete (A : Type) : topology A.
+Proof.
+  exists full ; firstorder.
+Defined.
+
+(* The definition of a T_1 space. *)
+Definition T1 {A : Type} (T : topology A) :=
+  forall x y : A,
+    x <> y ->
+      some u : T, (u x /\ ~ (u y)).
+
+(* The definition of Hausdorff space. *)
+Definition hausdorff {A : Type} (T : topology A) :=
+  forall x y : A,
+  x <> y ->
+    some u : T, some v : T,
+      (u x /\ v y /\ u * v = empty).
+
+(* A discrete space is Hausdorff. *)
+Lemma discrete_hausdorff {A : Type} : hausdorff (discrete A).
+Proof.
+  intros x y N.
+  exists { z : A | x = z } ; split ; [exact I | idtac].
+  exists { z : A | y = z } ; split ; [exact I | idtac].
+  repeat split ; auto.
+  apply ext.
+  - intros z [? ?].
+    absurd (x = y) ; auto.
+    transitivity z ; auto.
+  - firstorder.
+Qed.
+
+(* Every Hausdorff space is T1. *)
+Lemma hausdorff_is_T1 {A : Type} (T : topology A) :
+  hausdorff T -> T1 T.
+Proof.
+  intros H x y N.
+  destruct (H x y N) as [u [? [v [? [? [? G]]]]]].
+  exists u ; repeat split ; auto.
+  intro.
+  absurd (empty y) ; auto.
+  rewrite <- G.
+  split ; auto.
+Qed.
No results found