From 034310e2e2727844250ce3281c23c7b09bd6cfe4 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 17 Nov 2024 19:56:55 -0500 Subject: [PATCH 1/4] bipointed and paths --- _CoqProject | 1 + classical/classical_sets.v | 10 + theories/Make | 1 + theories/homotopy_theory/homotopy.v | 1 + theories/homotopy_theory/path.v | 177 ++++++++++++++++++ theories/homotopy_theory/wedge_sigT.v | 29 +++ theories/topology_theory/topology_structure.v | 4 + 7 files changed, 223 insertions(+) create mode 100644 theories/homotopy_theory/path.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..6f7a61f5c --- /dev/null +++ b/theories/homotopy_theory/path.v @@ -0,0 +1,177 @@ +(* 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. +From mathcomp Require Import wedge_sigT. + +(**md**************************************************************************) +(* # Paths *) +(* Paths from biPointed spaces. *) +(* *) +(* ``` *) +(* *) +(* {path i from x to y} == The space of paths over the bipointed space `i` *) +(* from x to y through a space T. It is endowed with *) +(* the compact-open topology. *) +(* 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`. *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +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) (at level 0) : 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; first by move => ->. +case: a; case: b => /= f [[+ +]] g [[+ +]] fgE. +rewrite -funeqE in fgE; rewrite fgE. +move=> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _). +have -> : a1 = a2 by exact: Prop_irrelevance. +have -> : b1 = b2 by exact: Prop_irrelevance. +have -> : c1 = c2 by exact: Prop_irrelevance. +done. +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 i) to one}). + +(* 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). + +Local 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. +move=> cf cg fgE; apply: wedge_fun_continuous => //; first by case. +by case; case; rewrite //=. +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. +by apply: wedge_fun_continuous; case; (try now (exact: cts_fun)); + case => //=;rewrite ?path_one ?path_zero //. +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..9081bee48 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -24,6 +24,9 @@ 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 == wedge of two bipointed spaces gluing zero to one *) +(* wedge2p == the shared point in the bpwedge *) +(* bpwedge_lift == wedge_lift specialized to the bipoitned wedge *) (* ``` *) (* *) (* The type `wedge p0` is endowed with the structures of: *) @@ -35,6 +38,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 +386,25 @@ HB.instance Definition _ := Quotient.on pwedge. HB.instance Definition _ := isPointed.Build pwedge pwedge_point. End pwedge. + +Section bpwedge. +Context (X Y : bpTopologicalType). +Definition wedge2p b := if b return (if b then X else Y) then (@one X) else (@zero Y). +Local Notation bpwedge := (@wedge bool _ wedge2p). +Local Notation bpwedge_lift := (@wedge_lift bool _ wedge2p). + +Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one . +Proof. +apply/eqP => R; have /eqmodP/orP[/eqP //|/andP[ /= + _]] := R. +by have := (@zero_one_neq X) => /[swap] ->. +Qed. + +Local Lemma bpwedgeE : @bpwedge_lift true one = @bpwedge_lift false zero . +Proof. by apply/eqmodP/orP; right; apply/andP; split. 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 _ (wedge2p X Y)). +Notation bpwedge_lift X Y := (@wedge_lift bool _ (wedge2p 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}. From 360b92790773ce8e2f41a8f111b1e532ab9d487f Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 18 Nov 2024 16:30:46 -0500 Subject: [PATCH 2/4] notation improvements --- CHANGELOG_UNRELEASED.md | 7 +++++++ theories/homotopy_theory/path.v | 31 +++++++++++++++++++++---------- 2 files changed, 28 insertions(+), 10 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 38ae969fb..7207353e1 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 `wedge2p`. + + new notations `bpwedge`, and `bpwedge_lift`. + ### Changed - in file `normedtype.v`, diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v index 6f7a61f5c..abcd25a4a 100644 --- a/theories/homotopy_theory/path.v +++ b/theories/homotopy_theory/path.v @@ -12,15 +12,16 @@ From mathcomp Require Import wedge_sigT. (* *) (* ``` *) (* *) -(* {path i from x to y} == The space of paths over the bipointed space `i` *) -(* from x to y through a space T. It is endowed with *) -(* the compact-open topology. *) (* 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 *) (* *) (******************************************************************************) @@ -28,6 +29,15 @@ 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. @@ -42,9 +52,10 @@ HB.mixin Record isPath {i : bpTopologicalType} {T: topologicalType} (x y : T) 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) (at level 0) : type_scope. - +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} @@ -99,7 +110,7 @@ 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 i) to one}). +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}` @@ -137,7 +148,7 @@ 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). -Local Lemma chain_path_cts_point {i j : bpTopologicalType} {T : topologicalType} +Lemma chain_path_cts_point {i j : bpTopologicalType} {T : topologicalType} (f : i -> T) (g : j -> T) : continuous f -> continuous g -> @@ -166,8 +177,8 @@ Qed. Local Lemma chain_path_cts : continuous (chain_path p q). Proof. -by apply: wedge_fun_continuous; case; (try now (exact: cts_fun)); - case => //=;rewrite ?path_one ?path_zero //. +apply: chain_path_cts_point; try exact: cts_fun. +by rewrite path_zero path_one. Qed. HB.instance Definition _ := @isContinuous.Build _ T (chain_path p q) From c85fb2105848ebc4b52e712de2150949506753f4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 11:13:05 +0900 Subject: [PATCH 3/4] linting --- theories/homotopy_theory/path.v | 79 ++++++++++++--------------- theories/homotopy_theory/wedge_sigT.v | 17 +++--- 2 files changed, 45 insertions(+), 51 deletions(-) diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v index abcd25a4a..e11e80938 100644 --- a/theories/homotopy_theory/path.v +++ b/theories/homotopy_theory/path.v @@ -3,21 +3,19 @@ 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. -From mathcomp Require Import wedge_sigT. +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`. *) +(* 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`. *) +(* 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 *) @@ -33,53 +31,49 @@ 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, + 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) +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} +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 }" := +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} + +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. +Lemma path_eqP (a b : {path i from x to y}) : a = b <-> a =1 b. Proof. -split; first by move => ->. -case: a; case: b => /= f [[+ +]] g [[+ +]] fgE. -rewrite -funeqE in fgE; rewrite fgE. -move=> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _). -have -> : a1 = a2 by exact: Prop_irrelevance. -have -> : b1 = b2 by exact: Prop_irrelevance. -have -> : c1 = c2 by exact: Prop_irrelevance. -done. +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. @@ -98,10 +92,10 @@ 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. +Proof. by rewrite /= !path_zero. Qed. Local Lemma fp_one : (f \o p) one = f y. -Proof. by rewrite /= ?path_one. Qed. +Proof. by rewrite /= !path_one. Qed. HB.instance Definition _ := isPath.Build i U (f x) (f y) (f \o p) fp_zero fp_one. @@ -112,8 +106,8 @@ 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}` +(* 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. @@ -131,6 +125,7 @@ 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. @@ -138,26 +133,23 @@ 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. +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} +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) : +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. -move=> cf cg fgE; apply: wedge_fun_continuous => //; first by case. -by case; case; rewrite //=. -Qed. +Proof. by move=> cf cg fgE; apply: wedge_fun_continuous => // [[]|[] []]. Qed. Section chain_path. Context {T : topologicalType} {i j : bpTopologicalType} (x y z: T). @@ -177,7 +169,7 @@ Qed. Local Lemma chain_path_cts : continuous (chain_path p q). Proof. -apply: chain_path_cts_point; try exact: cts_fun. +apply: chain_path_cts_point; [exact: cts_fun..|]. by rewrite path_zero path_one. Qed. @@ -185,4 +177,5 @@ 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 9081bee48..8bc9180ab 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -26,7 +26,7 @@ From mathcomp Require Import separation_axioms function_spaces. (* It's an embedding when the index is finite. *) (* bpwedge == wedge of two bipointed spaces gluing zero to one *) (* wedge2p == the shared point in the bpwedge *) -(* bpwedge_lift == wedge_lift specialized to the bipoitned wedge *) +(* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) (* ``` *) (* *) (* The type `wedge p0` is endowed with the structures of: *) @@ -389,20 +389,21 @@ End pwedge. Section bpwedge. Context (X Y : bpTopologicalType). -Definition wedge2p b := if b return (if b then X else Y) then (@one X) else (@zero Y). + +Definition wedge2p b := + if b return (if b then X else Y) then @one X else @zero Y. Local Notation bpwedge := (@wedge bool _ wedge2p). Local Notation bpwedge_lift := (@wedge_lift bool _ wedge2p). - -Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one . + +Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one. Proof. -apply/eqP => R; have /eqmodP/orP[/eqP //|/andP[ /= + _]] := R. -by have := (@zero_one_neq X) => /[swap] ->. +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; right; apply/andP; split. Qed. +Proof. by apply/eqmodP/orP; rewrite !eqxx; right. Qed. -HB.instance Definition _ := @isBiPointed.Build +HB.instance Definition _ := @isBiPointed.Build bpwedge (@bpwedge_lift true zero) (@bpwedge_lift false one) wedge_neq. End bpwedge. From 756ffc984e4eef5c69a85aa54b1f23f118112c17 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 18 Nov 2024 22:09:03 -0500 Subject: [PATCH 4/4] better name for bpwedge point --- CHANGELOG_UNRELEASED.md | 2 +- theories/homotopy_theory/wedge_sigT.v | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7207353e1..5b707c91f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -116,7 +116,7 @@ + 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 `wedge2p`. + + new definition `bpwedge_shared_pt`. + new notations `bpwedge`, and `bpwedge_lift`. ### Changed diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 8bc9180ab..86822e545 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -24,8 +24,9 @@ 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 *) -(* wedge2p == the shared point in the bpwedge *) (* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) (* ``` *) (* *) @@ -390,10 +391,10 @@ End pwedge. Section bpwedge. Context (X Y : bpTopologicalType). -Definition wedge2p b := +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 _ wedge2p). -Local Notation bpwedge_lift := (@wedge_lift bool _ wedge2p). +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. @@ -407,5 +408,5 @@ HB.instance Definition _ := @isBiPointed.Build bpwedge (@bpwedge_lift true zero) (@bpwedge_lift false one) wedge_neq. End bpwedge. -Notation bpwedge X Y := (@wedge bool _ (wedge2p X Y)). -Notation bpwedge_lift X Y := (@wedge_lift bool _ (wedge2p X Y)). +Notation bpwedge X Y := (@wedge bool _ (bpwedge_shared_pt X Y)). +Notation bpwedge_lift X Y := (@wedge_lift bool _ (bpwedge_shared_pt X Y)).