Instantly share code, notes, and snippets.

# andrejbauer/topology.v

Last active November 28, 2023 19:40
Show Gist options
• Save andrejbauer/d31e9666d5f950dd8ccd to your computer and use it in GitHub Desktop.
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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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 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 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 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 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?