From 71b1296fa6bc2c46fce5cc4759e401d9c4d60999 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Wed, 20 Nov 2024 21:14:54 -0500 Subject: [PATCH] bipointed and paths (#1400) * bipointed and paths --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 7 + _CoqProject | 1 + classical/classical_sets.v | 10 + theories/Make | 1 + theories/homotopy_theory/homotopy.v | 1 + theories/homotopy_theory/path.v | 181 ++++++++++++++++++ theories/homotopy_theory/wedge_sigT.v | 31 +++ theories/topology_theory/topology_structure.v | 4 + 8 files changed, 236 insertions(+) create mode 100644 theories/homotopy_theory/path.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 38ae969fb..5b707c91f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -112,6 +112,13 @@ - in `boolp.v`: + lemmas `existT_inj1`, `surjective_existT` +- in file `homotopy_theory/path.v`, + + new definitions `reparameterize`, `mk_path`, and `chain_path`. + + new lemmas `path_eqP`, and `chain_path_cts_point`. +- in file `homotopy_theory/wedge_sigT.v`, + + new definition `bpwedge_shared_pt`. + + new notations `bpwedge`, and `bpwedge_lift`. + ### Changed - in file `normedtype.v`, diff --git a/_CoqProject b/_CoqProject index ed73bd01a..882574185 100644 --- a/_CoqProject +++ b/_CoqProject @@ -63,6 +63,7 @@ theories/topology_theory/sigT_topology.v theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v +theories/homotopy_theory/path.v theories/separation_axioms.v theories/function_spaces.v diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 8c5acd53b..b773f279d 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2485,6 +2485,16 @@ Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed. End PointedTheory. +HB.mixin Record isBiPointed (X : Type) of Equality X := { + zero : X; + one : X; + zero_one_neq : zero != one; +}. + +#[short(type="biPointedType")] +HB.structure Definition BiPointed := + { X of Choice X & isBiPointed X }. + Variant squashed T : Prop := squash (x : T). Arguments squash {T} x. Notation "$| T |" := (squashed T) : form_scope. diff --git a/theories/Make b/theories/Make index eaefdc810..d82042d37 100644 --- a/theories/Make +++ b/theories/Make @@ -31,6 +31,7 @@ topology_theory/sigT_topology.v homotopy_theory/homotopy.v homotopy_theory/wedge_sigT.v +homotopy_theory/path.v separation_axioms.v function_spaces.v diff --git a/theories/homotopy_theory/homotopy.v b/theories/homotopy_theory/homotopy.v index 33e29737b..d424c7b38 100644 --- a/theories/homotopy_theory/homotopy.v +++ b/theories/homotopy_theory/homotopy.v @@ -1,2 +1,3 @@ (* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Export wedge_sigT. +From mathcomp Require Export path. diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v new file mode 100644 index 000000000..e11e80938 --- /dev/null +++ b/theories/homotopy_theory/path.v @@ -0,0 +1,181 @@ +(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import function_spaces wedge_sigT. + +(**md**************************************************************************) +(* # Paths *) +(* Paths from biPointed spaces. *) +(* *) +(* ``` *) +(* mk_path ctsf f0 f1 == constructs a value in `pathType x y` given proofs *) +(* that the endpoints of `f` are `x` and `y` *) +(* reparameterize f phi == the path `f` with a different parameterization *) +(* chain_path f g == the path which follows f, then follows g *) +(* Only makes sense when `f one = g zero`. The *) +(* domain is the wedge of domains of `f` and `g`. *) +(* ``` *) +(* The type `{path i from x to y in T}` is the continuous functions on the *) +(* bipointed space i that go from x to y staying in T. It is endowed with *) +(* - Topology via the compact-open topology *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Reserved Notation "{ 'path' i 'from' x 'to' y }" ( + at level 0, i at level 69, x at level 69, y at level 69, + only parsing, + format "{ 'path' i 'from' x 'to' y }"). +Reserved Notation "{ 'path' i 'from' x 'to' y 'in' T }" ( + at level 0, i at level 69, x at level 69, y at level 69, T at level 69, + format "{ 'path' i 'from' x 'to' y 'in' T }"). + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +HB.mixin Record isPath {i : bpTopologicalType} {T : topologicalType} (x y : T) + (f : i -> T) of isContinuous i T f := { + path_zero : f zero = x; + path_one : f one = y; +}. + +#[short(type="pathType")] +HB.structure Definition Path {i : bpTopologicalType} {T : topologicalType} + (x y : T) := {f of isPath i T x y f & isContinuous i T f}. + +Notation "{ 'path' i 'from' x 'to' y }" := (pathType i x y) : type_scope. +Notation "{ 'path' i 'from' x 'to' y 'in' T }" := + (@pathType i T x y) : type_scope. + +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := gen_eqMixin {path i from x to y}. +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := gen_choiceMixin {path i from x to y}. +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := + Topological.copy {path i from x to y} + (@weak_topology {path i from x to y} {compact-open, i -> T} id). + +Section path_eq. +Context {T : topologicalType} {i : bpTopologicalType} (x y : T). + +Lemma path_eqP (a b : {path i from x to y}) : a = b <-> a =1 b. +Proof. +split=> [->//|]. +move: a b => [/= f [[+ +]]] [/= g [[+ +]]] fgE. +move/funext : fgE => -> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _). +rewrite (Prop_irrelevance a1 a2) (Prop_irrelevance b1 b2). +by rewrite (Prop_irrelevance c1 c2). +Qed. + +End path_eq. + +Section cst_path. +Context {T : topologicalType} {i : bpTopologicalType} (x: T). + +HB.instance Definition _ := @isPath.Build i T x x (cst x) erefl erefl. +End cst_path. + +Section path_domain_path. +Context {i : bpTopologicalType}. +HB.instance Definition _ := @isPath.Build i i zero one idfun erefl erefl. +End path_domain_path. + +Section path_compose. +Context {T U : topologicalType} (i: bpTopologicalType) (x y : T). +Context (f : continuousType T U) (p : {path i from x to y}). + +Local Lemma fp_zero : (f \o p) zero = f x. +Proof. by rewrite /= !path_zero. Qed. + +Local Lemma fp_one : (f \o p) one = f y. +Proof. by rewrite /= !path_one. Qed. + +HB.instance Definition _ := isPath.Build i U (f x) (f y) (f \o p) + fp_zero fp_one. + +End path_compose. + +Section path_reparameterize. +Context {T : topologicalType} (i j: bpTopologicalType) (x y : T). +Context (f : {path i from x to y}) (phi : {path j from zero to one in i}). + +(* we use reparameterize, as opposed to just `\o` because we can simplify the + endpoints. So we don't end up with `f \o p : {path j from f zero to f one}` + but rather `{path j from zero to one}` +*) +Definition reparameterize := f \o phi. + +Local Lemma fphi_zero : reparameterize zero = x. +Proof. by rewrite /reparameterize /= ?path_zero. Qed. + +Local Lemma fphi_one : reparameterize one = y. +Proof. by rewrite /reparameterize /= ?path_one. Qed. + +Local Lemma fphi_cts : continuous reparameterize. +Proof. by move=> ?; apply: continuous_comp; apply: cts_fun. Qed. + +HB.instance Definition _ := isContinuous.Build _ _ reparameterize fphi_cts. + +HB.instance Definition _ := isPath.Build j T x y reparameterize + fphi_zero fphi_one. + +End path_reparameterize. + +Section mk_path. +Context {i : bpTopologicalType} {T : topologicalType}. +Context {x y : T} (f : i -> T) (ctsf : continuous f). +Context (f0 : f zero = x) (f1 : f one = y). + +Definition mk_path : i -> T := let _ := (ctsf, f0, f1) in f. + +HB.instance Definition _ := isContinuous.Build i T mk_path ctsf. +HB.instance Definition _ := @isPath.Build i T x y mk_path f0 f1. +End mk_path. + +Definition chain_path {i j : bpTopologicalType} {T : topologicalType} + (f : i -> T) (g : j -> T) : bpwedge i j -> T := + wedge_fun (fun b => if b return (if b then i else j) -> T then f else g). + +Lemma chain_path_cts_point {i j : bpTopologicalType} {T : topologicalType} + (f : i -> T) (g : j -> T) : + continuous f -> + continuous g -> + f one = g zero -> + continuous (chain_path f g). +Proof. by move=> cf cg fgE; apply: wedge_fun_continuous => // [[]|[] []]. Qed. + +Section chain_path. +Context {T : topologicalType} {i j : bpTopologicalType} (x y z: T). +Context (p : {path i from x to y}) (q : {path j from y to z}). + +Local Lemma chain_path_zero : chain_path p q zero = x. +Proof. +rewrite /chain_path /= wedge_lift_funE ?path_one ?path_zero //. +by case => //= [][] //=; rewrite ?path_one ?path_zero. +Qed. + +Local Lemma chain_path_one : chain_path p q one = z. +Proof. +rewrite /chain_path /= wedge_lift_funE ?path_zero ?path_one //. +by case => //= [][] //=; rewrite ?path_one ?path_zero. +Qed. + +Local Lemma chain_path_cts : continuous (chain_path p q). +Proof. +apply: chain_path_cts_point; [exact: cts_fun..|]. +by rewrite path_zero path_one. +Qed. + +HB.instance Definition _ := @isContinuous.Build _ T (chain_path p q) + chain_path_cts. +HB.instance Definition _ := @isPath.Build _ T x z (chain_path p q) + chain_path_zero chain_path_one. + +End chain_path. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index d39fddba0..86822e545 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -24,6 +24,10 @@ From mathcomp Require Import separation_axioms function_spaces. (* wedge_prod == the mapping from the wedge as a quotient of sums to *) (* the wedge as a subspace of the product topology. *) (* It's an embedding when the index is finite. *) +(* bpwedge_shared_pt b == the shared point in the bpwedge. Either zero or one *) +(* depending on `b`. *) +(* bpwedge == wedge of two bipointed spaces gluing zero to one *) +(* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) (* ``` *) (* *) (* The type `wedge p0` is endowed with the structures of: *) @@ -35,6 +39,10 @@ From mathcomp Require Import separation_axioms function_spaces. (* - quotient *) (* - pointed *) (* *) +(* The type `bpwedge` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* - bipointed *) (******************************************************************************) Set Implicit Arguments. @@ -379,3 +387,26 @@ HB.instance Definition _ := Quotient.on pwedge. HB.instance Definition _ := isPointed.Build pwedge pwedge_point. End pwedge. + +Section bpwedge. +Context (X Y : bpTopologicalType). + +Definition bpwedge_shared_pt b := + if b return (if b then X else Y) then @one X else @zero Y. +Local Notation bpwedge := (@wedge bool _ bpwedge_shared_pt). +Local Notation bpwedge_lift := (@wedge_lift bool _ bpwedge_shared_pt). + +Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one. +Proof. +by apply/eqP => /eqmodP/predU1P[//|/andP[/= + _]]; exact/negP/zero_one_neq. +Qed. + +Local Lemma bpwedgeE : @bpwedge_lift true one = @bpwedge_lift false zero . +Proof. by apply/eqmodP/orP; rewrite !eqxx; right. Qed. + +HB.instance Definition _ := @isBiPointed.Build + bpwedge (@bpwedge_lift true zero) (@bpwedge_lift false one) wedge_neq. +End bpwedge. + +Notation bpwedge X Y := (@wedge bool _ (bpwedge_shared_pt X Y)). +Notation bpwedge_lift X Y := (@wedge_lift bool _ (bpwedge_shared_pt X Y)). diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 5e78bde1c..8eaf56dbb 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -105,6 +105,10 @@ HB.structure Definition Topological := HB.structure Definition PointedTopological := {T of PointedNbhs T & Nbhs_isTopological T}. +#[short(type="bpTopologicalType")] +HB.structure Definition BiPointedTopological := + { X of BiPointed X & Topological X }. + Section Topological1. Context {T : topologicalType}.