From 20cd6f5a69a191a340832deacb453d3327db0263 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 25 Sep 2022 00:51:51 -0400 Subject: [PATCH] getting there on paths --- theories/homotopy.v | 194 +++++++++++++++++++++++++++++++++++++++----- 1 file changed, 175 insertions(+), 19 deletions(-) diff --git a/theories/homotopy.v b/theories/homotopy.v index 1e8c84133..21297f815 100644 --- a/theories/homotopy.v +++ b/theories/homotopy.v @@ -28,7 +28,6 @@ Local Open Scope ring_scope. HB.mixin Record IsParametrization {R : realType} (f : R -> R) := { - parametrize_monotone : {in `[0, 1] &, {homo f : x y / x <= y}}; parametrize_cts : {within `[0,1], continuous f}; parametrize_init : f 0 = 0; parametrize_final : f 1 = 1; @@ -47,16 +46,22 @@ Notation "[ 'parametrization' 'of' f ]" := Section Parametrizations. Context {R : realType}. -Section Identity. -Local Lemma id_parametrize_monotone : - {in `[0, 1] &, {homo (@idfun R) : x y / x <= y}}. -Proof. by []. Qed. +Lemma parametrize_monotone (f : {parametrization R}) : + {in `[0,1] &, {mono f : x y / x <= y}}. +Proof. +apply: itv_continuous_inj_le. +- exists 0; exists 1; rewrite ?bound_itvE ?parametrize_init. + by rewrite ?parametrize_final; split. +- apply: parametrize_cts. +- by move: (@inj _ _ _ f); rewrite mem_setE. +Qed. +Section Identity. Local Lemma id_parametrize_cts : {within `[0,1], continuous (@idfun R)}. Proof. exact: continuous_subspaceT. Qed. HB.instance Definition _ := @IsParametrization.Build - _ _ (id_parametrize_monotone) id_parametrize_cts erefl erefl. + _ _ id_parametrize_cts erefl erefl. Definition id_parametrization := [parametrization of (@idfun R)]. End Identity. @@ -66,14 +71,6 @@ Variables (f g : {parametrization R}). Let h := (f \o g) : R -> R. HB.instance Definition _ := SplitInjFun.on h. -Local Lemma h_monotone : {in `[0, 1] &, {homo h : x y / x <= y}}. -Proof. -move=> x y ? ? ?; apply: parametrize_monotone. -- exact: (@funS _ _ _ _ g) => /=. -- exact: (@funS _ _ _ _ g) => /=. -- exact: parametrize_monotone. -Qed. - Local Lemma h_continuous : {within `[0, 1], continuous h}. Proof. move=> x; apply: (@continuous_comp @@ -89,7 +86,7 @@ Local Lemma h_final : h 1 = 1. Proof. by rewrite /h /= parametrize_final parametrize_final. Qed. HB.instance Definition _ := @IsParametrization.Build - _ _ (h_monotone) h_continuous h_init h_final. + _ _ h_continuous h_init h_final. Definition comp_parametrization := [parametrization of h]. End Composition. @@ -100,11 +97,170 @@ Variables (f : {parametrization R}). Let g := (f^-1). -HB.mixin Record IsPath {R : realType} {T : topologicalType} (f : R -> T) := - { path_continuous : {within `[0,1], continuous f} }. +Local Lemma g_continuous : {within `[0,1], continuous g}. +Proof. +rewrite -(@parametrize_init _ f) -(@parametrize_final _ f). +apply: segment_can_le_continuous => //; first exact: parametrize_cts. +by move=> ? ?; apply/funK/mem_set. +Qed. + +Local Lemma g_init : g 0 = 0. +Proof. +rewrite -[x in g x](@parametrize_init _ f) [g (f _)]funK //. +by rewrite mem_setE /= bound_itvE. +Qed. + +Local Lemma g_final : g 1 = 1. +Proof. +rewrite -[x in g x](@parametrize_final _ f) [g (f _)]funK //. +by rewrite mem_setE /= bound_itvE. +Qed. + +Local Lemma g_cancel : {in `[0,1]%classic, cancel g f}. +Proof. +rewrite mem_setE /= -(@parametrize_init _ f) -(@parametrize_final _ f). +apply: segment_continuous_le_can_sym => //; first exact: parametrize_cts. +by move=> ? ?; apply/funK/mem_set. +Qed. + +Local Lemma g_fun : set_fun `[0,1]%classic `[0,1]%classic g. +Proof. +have gle : {in `[0,1] &, {mono g : x y / x <= y}}. + apply: itv_continuous_inj_le. + - by exists 0; exists 1; rewrite ?bound_itvE ?g_init ?g_final; split. + - apply: g_continuous. + - by apply: can_in_inj => p q; exact/g_cancel/mem_set. +move=> z; rewrite /= ?in_itv /= => /[dup] ? /andP [] ? ?. +by rewrite -g_init -g_final; apply/andP; split; rewrite gle // ?bound_itvE. +Qed. + +HB.instance Definition _ := Can.Build _ _ _ g g_cancel. +HB.instance Definition _ := IsFun.Build _ _ _ _ _ g_fun. +HB.instance Definition _ := SplitInjFun.on g. + +HB.instance Definition _ := @IsParametrization.Build + _ _ g_continuous g_init g_final. + +Definition inv_parametrization := [parametrization of g]. + +Lemma inv_parametrization_can_r : {in `[0,1], cancel f inv_parametrization}. +Proof. +move=> z zI /=; rewrite (@segment_continuous_can_sym _ 0 1) //. +- exact: parametrize_cts. +- move=> w wI; move: (@funK _ _ _ inv_parametrization w). + by rewrite mem_setE invV => /(_ wI). +- by rewrite g_init g_final /minr /maxr ltr01. +Qed. + +Lemma inv_parametrization_can_l: {in `[0,1], cancel inv_parametrization f}. +Proof. by move=> z zI; apply: funK; rewrite mem_setE. Qed. + +End Inverses. +End Parametrizations. + +HB.mixin Record IsContinuous {T U : topologicalType} (f : T -> U) := + { continuous_fun : continuous f }. + +HB.structure Definition JustContinuous {T U : topologicalType} + := {f of @IsContinuous T U f}. + +HB.structure Definition ContinuousFun {T U : topologicalType} + (A : set T) (B : set U) := + {f of + @IsContinuous (subspace_topologicalType A) U f & + @Fun (subspace_topologicalType A) U A B f + }. + +Notation "{ 'continuous' A >-> B }" := + (@ContinuousFun.type _ _ A B) : form_scope. +Notation "[ 'continuous' 'of' f ]" := + ([the (@ContinuousFun.type _ _ _ _) of (f: _ -> _)]) : form_scope. + +Section Reparametrization. +Open Scope quotient_scope. +Context {R : realType} {T : topologicalType} (B : set T). + +Definition reparametrize (f g : {classic {continuous `[0,1] >-> B}}) : bool := + `[]. + +Lemma reflexive_reparametrize : reflexive reparametrize. +Proof. by move=> f; apply/asboolP; exists id_parametrization. Qed. + +Lemma symmetric_reparametrize : symmetric reparametrize. +Proof. +by move=> f g; apply/asbool_equiv_eq; split=> [][] gamma fgamg; + exists (inv_parametrization gamma) => z zI; + rewrite /comp -fgamg /comp ?inv_parametrization_can_l //; + apply: (@funS _ _ _ _ (inv_parametrization gamma)). +Qed. + +Lemma transitive_reparametrize : transitive reparametrize. +Proof. +move=> f g h /asboolP [p pfg] /asboolP [q qgh]; apply/asboolP. +exists (comp_parametrization p q) => z zI /=. +by rewrite -qgh //= -pfg //; exact: (@funS _ _ _ _ q). +Qed. + +Definition equiv_rel_reparametrize := EquivRel reparametrize + reflexive_reparametrize symmetric_reparametrize transitive_reparametrize. + +Definition Path := {eq_quot equiv_rel_reparametrize}. + +Definition path_init := lift_fun1 Path (fun f => f 0). + +Lemma path_init_mono : {mono \pi_Path : f / f 0 >-> path_init f}. +Proof. +move=> f; unlock path_init. +have : ((repr (\pi_(Path) f)) = f %[mod Path]) by rewrite reprK. +move=> /eqquotP /asboolP [] gamma /(_ 0). +by rewrite bound_itvE /= parametrize_init; exact. +Qed. + +Canonical pi_path_init_mono := PiMono1 path_init_mono. + +Definition path_final := lift_fun1 Path (fun f => f 1). + +Lemma path_final_mono : {mono \pi_Path : f / f 1 >-> path_final f}. +Proof. +move=> f; unlock path_final. +have : ((repr (\pi_(Path) f)) = f %[mod Path]) by rewrite reprK. +move=> /eqquotP /asboolP [] gamma /(_ 1). +by rewrite bound_itvE /= parametrize_final; exact. +Qed. + +Canonical pi_path_final_mono := PiMono1 path_final_mono. + +Definition path_image := lift_fun1 Path (fun f => f @` `[0,1] ). + +Lemma path_image_mono : {mono \pi_Path : f / f @` `[0,1] >-> path_image f}. +Proof. +move=> f; unlock path_image; rewrite eqEsubset; split => z /= [w wI] <-. + have /eqquotP/asboolP [gamma fg]: f = repr (\pi_(Path) f) %[mod Path]. + by rewrite reprK. + by (exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma). +have /eqquotP/asboolP [gamma fg]: repr (\pi_(Path) f) = f %[mod Path]. + by rewrite reprK. +(exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma). +Qed. + +Canonical pi_path_image_mono := PiMono1 path_image_mono. + +Section ConstantPath. +Context (x : T). +Hypothesis Bx : B x. +Let f : (subspace `[(0:R),1]) -> T := fun=> x. + +Local Lemma cst_fun : set_fun `[0,1]%classic B f. +Proof. by []. Qed. +HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun. + +Local Lemma cst_continuous : continuous f. +Proof. by apply: continuous_subspaceT => ? ?; exact: cst_continuous. Qed. + +HB.instance Definition _ := @IsContinuous.Build _ _ _ cst_continuous. + +Definition cst_path : Path := \pi [continuous of f]. -HB.structure Definition JustPath {R : realType} {T : topologicalType} - := {f of @IsPath R T f}. HB.structure Definition Path {R : realType} {T : topologicalType} (B : set T) := {f of @IsPath R T f & @Fun R T `[0,1]%classic B f}.