Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
(* 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 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.
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
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).
(* 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 }.
(* 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 /\ disjoint u v).
(* 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.
intros z [? ?].
absurd (x = y) ; auto.
transitivity z ; auto.
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 (u y /\ v y) ; auto.
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.
We seem to need extensionality for propositions. *)
Lemma indiscrete_least (A : Type) (T : topology A) :
(forall (X : Type) (s t : P X), s <= t -> t <= s -> s = t) ->
indiscrete A <= T.
Proof.
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 })).
- 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.
(* 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.
@jeremy-w

This comment has been minimized.

Copy link

commented Jun 6, 2014

Interesting. I'd love to see a version done how you feel one should do it natively in Coq, to learn from by comparison. Or is there some established project that already has that where I should go look at it?

@andrejbauer

This comment has been minimized.

Copy link
Owner Author

commented Jun 15, 2014

Well, if I did it my way, I wouldn't posit that topology is closed under arbitrary unions, nor would I state that opens are subsets of a space. I would axiomatize the Sierpinski space S and then define the topology of a type A to be A -> S, a la synthetic topology.

@DavidMichaelRoberts

This comment has been minimized.

Copy link

commented Oct 16, 2014

Ah, so you mean the topology is the type A -> S, and every type comes with an intrinsic topology, as in http://math.andrej.com/2010/01/06/metric-spaces-in-synthetic-topology-2/

@sligocki

This comment has been minimized.

Copy link

commented Jul 3, 2018

Is it possible to represent Subspaces (Subspace topologies) in this formalization? I guess not because you require that (open (@Full A)), so this won't allow us to consider a topology on a subset of A, is that right?

How about Quotient topologies?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.