From afaeabd6daa9c305e28dc43884d38dd5af84fcb8 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 20 Nov 2024 21:53:59 -0500 Subject: [PATCH] rough but current path concat --- theories/homotopy_theory/path.v | 265 +++++++++++++++++++++++++- theories/homotopy_theory/wedge_sigT.v | 2 +- 2 files changed, 265 insertions(+), 2 deletions(-) diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v index e11e80938..7d622f96b 100644 --- a/theories/homotopy_theory/path.v +++ b/theories/homotopy_theory/path.v @@ -3,7 +3,8 @@ 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. +From mathcomp Require Import function_spaces separation_axioms. +From mathcomp Require Import wedge_sigT. (**md**************************************************************************) (* # Paths *) @@ -179,3 +180,265 @@ HB.instance Definition _ := @isPath.Build _ T x z (chain_path p q) chain_path_zero chain_path_one. End chain_path. + +(* Such a structure is very much like [a,b] in that + one can split it in half like `[0,1] \/ [0,1] ~ [0,2] ~ [0,1] +*) +HB.mixin Record isSelfSplit (X : Type) of BiPointedTopological X := { + to_wedge : {path X from zero to one in bpwedge X X }; + to_wedge_bij : bijective to_wedge; + to_wedge_cts : continuous to_wedge; + to_wedge_open : forall A, open A -> open (to_wedge @` A); +}. + +#[short(type="selfSplitType")] +HB.structure Definition SelfSplit := { + X of BiPointedTopological X & isSelfSplit X +}. + +Section path_concat. +Context {T : topologicalType} {i : selfSplitType} (x y z: T). +Context (p : {path i from x to y}) (q : {path i from y to z}). + +Definition path_concat : {path i from x to z} := + reparameterize (chain_path p q) (to_wedge). + +End path_concat. + +Section self_wedge_path. +Context {i : selfSplitType}. + +Definition from_wedge_sub : bpwedge i i -> i := + ((bijection_of_bijective (@to_wedge_bij i))^-1)%FUN. + +Local Lemma from_wedge_zero : from_wedge_sub zero = zero. +Proof. +move/bij_inj : (@to_wedge_bij i); apply. +rewrite /from_wedge_sub /=. +have /= -> := (@invK _ _ _ _ (bijection_of_bijective (@to_wedge_bij i))). + by rewrite path_zero. +by apply/mem_set. +Qed. + +Local Lemma from_wedge_one : from_wedge_sub one = one. +Proof. +move/bij_inj : (@to_wedge_bij i); apply. +rewrite /from_wedge_sub /=. +have /= -> := (@invK _ _ _ _ (bijection_of_bijective (@to_wedge_bij i))). + by rewrite path_one. +exact/mem_set. +Qed. + +Local Lemma from_wedge_cts : continuous from_wedge_sub. +Proof. +apply/continuousP => A /to_wedge_open. +congr(_ _); rewrite eqEsubset; split => //. + move=> ? /= [z Az <-]; rewrite /from_wedge_sub. + by rewrite funK => //; apply/mem_set. +move=> z /=; exists (from_wedge_sub z) => //. +rewrite /from_wedge_sub. +have /= -> // := (@invK _ _ _ _ (bijection_of_bijective (@to_wedge_bij i))). +exact/mem_set. +Qed. + +HB.instance Definition _ := isContinuous.Build _ _ from_wedge_sub from_wedge_cts. + +HB.instance Definition _ := isPath.Build (bpwedge i i) i zero one from_wedge_sub + from_wedge_zero from_wedge_one. +End self_wedge_path. + +HB.lock Definition from_wedge {i : selfSplitType} : + {path (bpwedge i i) from zero to one in i} := + [the pathType _ _ _ of from_wedge_sub]. + +Lemma from_wedgeK {i : selfSplitType} : cancel from_wedge (@to_wedge i). +Proof. +move=> z; rewrite unlock /= /from_wedge_sub. +have /= -> // := (@invK _ _ _ _ (bijection_of_bijective (@to_wedge_bij i))). +exact/mem_set. +Qed. + +Lemma to_wedgeK {i : selfSplitType}: cancel (@to_wedge i) from_wedge. +Proof. +by move=> z; rewrite unlock /= /from_wedge_sub funK //; exact/mem_set. +Qed. + +Section path_join_assoc. +Context (i : selfSplitType). + +Let i_i := @bpwedge i i. +Local Open Scope quotient_scope. +Notation "f '<>' g" := (@path_concat _ i _ _ _ f g). + +Lemma conact_cstr {T : topologicalType} (x y : T) (f : {path i from x to y}) : + exists (p : {path i from zero to one}), f \o p = (f <> cst y). +Proof. +exists (idfun <> cst one). +rewrite compA wedge_fun_comp /path_concat. +congr( _ \o to_wedge); congr(wedge_fun _). +apply: functional_extensionality_dep; case => //=. +by apply/funext => ? /=; rewrite /cst path_one. +Qed. + +Lemma conact_cstl {T : topologicalType} (x y : T) (f : {path i from x to y}) : + exists (p : {path i from zero to one}), f \o p = (cst x <> f). +Proof. +exists (cst zero <> idfun). +rewrite compA wedge_fun_comp /path_concat. +congr( _ \o to_wedge); congr(wedge_fun _). +apply: functional_extensionality_dep; case => //=. +by apply/funext => ? /=; rewrite /cst path_zero. +Qed. + +Let ii_i := (bpwedge i_i i). +Let i_ii := (bpwedge i i_i). +Check @mk_path. +Let wedgel_i_i : {path i from zero to _ in i_i} := + @mk_path _ _ zero _ + [the continuousType _ _ of @wedge_lift _ _ _ true] + cts_fun + erefl (bpwedgeE i i). + Check wedgel_i_i. +Let wedger_i_i : {path i from _ to one in i_i} := + @mk_path _ _ _ one + [the continuousType _ _ of @wedge_lift _ _ _ false] + cts_fun + erefl erefl. + +Let splitl_left : {path i_i from zero to _ in ii_i} := + (@mk_path _ _ zero _ + [the continuousType _ _ of @wedge_lift _ _ _ true] + cts_fun + erefl (@bpwedgeE _ _)). +Let splitl_right : {path i from _ to one in ii_i} := + @mk_path _ _ _ one + [the continuousType _ _ of @wedge_lift _ _ _ false] + cts_fun + erefl erefl. +Let splitl : {path i from (@zero ii_i) to one} := + (reparameterize splitl_left to_wedge) <> splitl_right. + +Let splitr_right : {path i_i from _ to one in i_ii} := + @mk_path _ _ _ one + [the continuousType _ _ of @wedge_lift _ _ _ false] + cts_fun + erefl erefl. +Let splitr_left : {path i from zero to _ in i_ii} := + @mk_path _ _ zero _ + [the continuousType _ _ of @wedge_lift _ _ _ true] + cts_fun + erefl (bpwedgeE _ _). + +Let unsplitr : {path i_ii from zero to one in i} := + reparameterize + from_wedge + (chain_path wedgel_i_i (reparameterize wedger_i_i from_wedge)). + +Let associ : continuousType ii_i i_ii := + chain_path + (chain_path + (splitr_left) + (splitr_right \o wedgel_i_i)) + (splitr_right \o wedger_i_i). + +Section assoc. +Context {T : topologicalType} {p1 p2 p3 p4: T}. +Context (f : {path i from p1 to p2}). +Context (g : {path i from p2 to p3}). +Context (h : {path i from p3 to p4}). + +Local Lemma assoc0 : associ zero = zero. +Proof. +rewrite /associ /= /chain_path/mk_path /= ?wedge_lift_funE //. + by case; case; rewrite //= ?bpwedgeE. +case; case; rewrite //= ?bpwedgeE //= ?wedge_lift_funE /= ?bpwedgeE //=. + by case; case; rewrite //= ?bpwedgeE. +by case; case; rewrite //= ?bpwedgeE. +Qed. + +Local Lemma assoc1 : associ one = one. +Proof. +rewrite /associ /= /chain_path/mk_path /= ?wedge_lift_funE //. +case; case; rewrite //= ?bpwedgeE //= ?wedge_lift_funE /= ?bpwedgeE //=. + by case; case; rewrite //= ?bpwedgeE. +by case; case; rewrite //= ?bpwedgeE. +Qed. + +(* not really non-forgetful, but we can make it local anyway so it's fine*) +#[local, non_forgetful_inheritance] +HB.instance Definition _ := isPath.Build ii_i _ _ _ associ + assoc0 assoc1. + +Local Lemma concat_assocl : + (f <> (g <> h)) \o (unsplitr \o associ \o splitl) = + ((f <> g) <> h). +Proof. +Ltac wedge_simpl := repeat ( + rewrite ?(wedge_lift_funE, path_one, path_zero, bpwedgeE, reprK) //=; + (try (case;case))). +apply/funext => z; rewrite /= /reparameterize /=/associ/chain_path. +rewrite -[to_wedge z](@reprK _ i_i). +case E : (repr (to_wedge z)) => [b x] /=. +wedge_simpl; rewrite /= ?from_wedgeK ?to_wedgeK. +case: b x E => x E /=; wedge_simpl; first last. + by rewrite from_wedgeK; wedge_simpl. +rewrite -[to_wedge x](@reprK _ i_i); case: (repr (to_wedge x)) => [b2 y] /=. +case: b2 y => y; wedge_simpl; rewrite from_wedgeK. +wedge_simpl. +Qed. + +Lemma concat_assoc: + exists p : {path i from zero to one}, + (f <> (g <> h)) \o p = ((f <> g) <> h). +Proof. +exists (reparameterize unsplitr (reparameterize associ splitl)). +by rewrite concat_assocl. +Qed. + +End assoc. +End path_join_assoc. + +HB.mixin Record isPathDomain {d} (i : Type) of + OrderTopological d i & SelfSplit i := { + (* this makes the path_between relation symmetric*) + flip : {path i from (@one i) to (@zero i)}; + flipK : involutive flip; + (* this lets us curry for paths between paths*) + domain_locally_compact : locally_compact [set: i]; + (* this gives us starting/ending points for constructing homotopies*) + zero_bot : forall (y : i), (@Order.le d i zero y); + one_top : forall (y : i), (@Order.le d i y one); +}. + +#[short(type="pathDomainType")] +HB.structure Definition PathDomain {d} := + { i of @OrderTopological d i & SelfSplit i & isPathDomain d i}. + +Lemma path_domain_set1 {d} {i : pathDomainType d} (x : i) : + closed [set x]. +Proof. +exact/accessible_closed_set1/hausdorff_accessible/order_hausdorff. +Qed. + +#[global] Hint Resolve path_domain_set1 : core. + +Section path_flip. +Context {d} {T : topologicalType} (i : pathDomainType d) (x y : T). +Context (f : {path i from x to y}). + +Definition path_flip := f \o flip. + +Local Lemma fflip_zero : path_flip zero = y. +Proof. by rewrite /path_flip /= path_zero path_one. Qed. + +Local Lemma fflip_one : path_flip one = x. +Proof. by rewrite /path_flip /= path_one path_zero. Qed. + +Local Lemma fflip_cts : continuous path_flip. +Proof. by move=> ?; apply: continuous_comp; apply: cts_fun. Qed. + +HB.instance Definition _ := isContinuous.Build _ _ path_flip fflip_cts. + +HB.instance Definition _ := isPath.Build i T y x path_flip + fflip_zero fflip_one. +End path_flip. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 86822e545..a2916f221 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -401,7 +401,7 @@ Proof. by apply/eqP => /eqmodP/predU1P[//|/andP[/= + _]]; exact/negP/zero_one_neq. Qed. -Local Lemma bpwedgeE : @bpwedge_lift true one = @bpwedge_lift false zero . +Lemma bpwedgeE : @bpwedge_lift true one = @bpwedge_lift false zero . Proof. by apply/eqmodP/orP; rewrite !eqxx; right. Qed. HB.instance Definition _ := @isBiPointed.Build