path connected is an equivalence relation

theories/homotopy.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
-From mathcomp Require Import interval rat.
+From mathcomp Require Import interval rat generic_quotient.
 Require Import realfun .
 Require Import mathcomp_extra boolp reals ereal set_interval classical_sets.
 Require Import signed functions topology normedtype landau sequences derive.
@@ -72,9 +72,9 @@ Notation "{ 'loop' R , B 'at' t }" := (@LoopAt.type R _ t B) : form_scope.
 Notation "[ 'loop' 'at' t 'of' f ]" := ([the (@LoopAt.type _ _ t _) of (f : _ -> _)]) : form_scope.
 
 Section Paths.
-Context {R : realType} {T : topologicalType}.
+Context {R : realType} {T : topologicalType} (B : set T).
 Section ConstantPath.
-Context (B : set T) (x : T).
+Context (x : T).
 Hypothesis Bx : B x.
 Let f : R -> T := fun=> x.
 
@@ -92,7 +92,7 @@ HB.instance Definition _ := @IsBetween.Build R T x x f (erefl _) (erefl _).
 Definition constant_path := [loop at x of f].
 End ConstantPath.
 
-Lemma shift_path (B : set T) (f : {path R, B}) (shift : {fun `[(0:R),1]%classic >-> `[(0:R),1]%classic}) : 
+Lemma shift_path (f : {path R, B}) (shift : {fun `[(0:R),1]%classic >-> `[(0:R),1]%classic}) : 
  (continuous (shift : subspace `[0,1] -> subspace `[0,1])) ->
  {within `[0,1], continuous (f \o shift)}.
 Proof.
@@ -123,15 +123,15 @@ exact: opp_continuous.
 Qed.
 
 Section ReversePath.
-Variables (B : set T) (f : {path R, B}).
+Variables (f : {path R, B}).
 
 Definition flip_path := [fun of f] \o [fun of flip_f].
 
 Lemma flip_path_funS : @set_fun R T `[0,1]%classic B flip_path.
 Proof. by []. Qed.
 
 HB.instance Definition _ := 
-  @IsPath.Build R T flip_path (@shift_path B f [fun of flip_f] rev_cts).
+  @IsPath.Build R T flip_path (@shift_path f [fun of flip_f] rev_cts).
 
 HB.instance Definition _ := 
   @IsFun.Build R T `[0,1]%classic B flip_path flip_path_funS.
@@ -141,7 +141,7 @@ Definition reverse_path := [path of flip_path].
 End ReversePath.
 
 Section RevLoop.
-Context {t1 t2 : T} {B : set T} (f : {loop R, B}).
+Context {t1 t2 : T} (f : {loop R, B}).
 Lemma rev_loop : @IsClosed R T (reverse_path f). 
 Proof.
 by split; rewrite /= /flip_path /= /flip_f onem0 onem1 -endpointsE.
@@ -151,7 +151,7 @@ HB.instance Definition _ := rev_loop.
 End RevLoop.
 
 Section RevPathBetween.
-Context {t1 t2 : T} {B : set T} (f : {path R, B from t1 to t2}).
+Context {t1 t2 : T} (f : {path R, B from t1 to t2}).
 Lemma rev_pathbetween : @IsBetween R T t2 t1 (reverse_path f). 
 Proof. 
 split; rewrite /= /flip_path /= /flip_f ?onem1 ?onem0.
@@ -164,7 +164,7 @@ HB.instance Definition _ := @rev_pathbetween.
 End RevPathBetween.
 
 Section ReverseLoopAtBetween.
-Context {B : set T} (t : T) (f : {loop R, B at t}).
+Context (t : T) (f : {loop R, B at t}).
 
 Lemma rev_loop_at : @IsBetween R T t t (reverse_path f). 
 Proof. apply: rev_pathbetween. Qed. 
@@ -178,11 +178,11 @@ Definition foo := [path from t to t of (reverse_path f)].
 *)
 
 Section ChainPath.
-Context (B : set T) (x1 x2 x3 : T) (f : {path R, B from x1 to x2}).
+Context (x1 x2 x3 : T) (f : {path R, B from x1 to x2}).
 Context (g : {path R, B from x2 to x3}).
 Let shift1 : R -> R := (fun r => r*2).
 Let shift2 : R -> R := (fun r => r*2 - 1).
-Definition chain := patch (g \o shift2) (`[0,1/2]%classic) (f \o shift1).
+Definition ftheng := patch (g \o shift2) (`[0,1/2]%classic) (f \o shift1).
 
 Local Lemma shift1fun : 
   @set_fun R R `[0,1/2]%classic `[0,1]%classic shift1.
@@ -194,7 +194,7 @@ Qed.
 
 HB.instance Definition _ := IsFun.Build _ _ _ _ _ shift1fun.
 
-Lemma h_cts1 : {within `[0,1/2], continuous chain}.
+Lemma h_cts1 : {within `[0,1/2], continuous ftheng}.
 apply: (@subspace_eq_continuous _ _ _ (f \o shift1)). 
   move=> q1 q2; apply: sym_equal; move: q1 q2.
   apply patchT.
@@ -217,10 +217,10 @@ Qed.
 
 HB.instance Definition _ := IsFun.Build _ _ _ _ _ shift2fun.
 
-Lemma h_cts2 : {within `[1/2,1], continuous chain}.
+Lemma h_cts2 : {within `[1/2,1], continuous ftheng}.
 pose h2 := patch (g \o shift2) (`[0,1/2[%classic) (f \o shift1).
-apply: (@subspace_eq_continuous _ _ _ h2 chain).
-  move=> q /set_mem; rewrite set_itvcc /chain/h2 => /= /andP [? ?].
+apply: (@subspace_eq_continuous _ _ _ h2 ftheng).
+  move=> q /set_mem; rewrite set_itvcc /ftheng/h2 => /= /andP [? ?].
   rewrite /patch/= set_itvcc set_itvco ; do 2 case: ifP => //=.
     move=> /negP /= P /set_mem/andP [] ? ?; contradict P.
     by apply: mem_set; apply/andP; split => //; exact: ltW.
@@ -245,7 +245,7 @@ apply (@continuousD R R R) => //; last exact: cst_continuous.
 apply (@continuousM R) => //; last exact: cst_continuous.
 Qed.
 
-Lemma h_cts : {within `[0,1], continuous chain}.
+Lemma h_cts : {within `[0,1], continuous ftheng}.
 Proof.
 have : (`[0,1/2]%classic `|` `[1/2,1]%classic = `[(0:R),1]%classic).
   rewrite ?set_itvcc eqEsubset; (split => r /=; first case) => /andP [lb ub].
@@ -260,33 +260,74 @@ move=> <-; apply: pasting; (try exact: interval_closed).
 exact: h_cts2.
 Qed.
 
-Lemma h_fun : set_fun `[0,1]%classic B chain.
+Lemma h_fun : set_fun `[0,1]%classic B ftheng.
 Proof.
 move=> r; rewrite set_itvcc => /andP [] ? ?.
-rewrite /chain/patch; case: ifP; rewrite set_itvcc. 
+rewrite /ftheng/patch; case: ifP; rewrite set_itvcc. 
   rewrite (_ : f \o shift1 = [fun of f] \o [fun of shift1]) //.
   by move=> /set_mem/andP [? ?]; apply: funS; apply/andP; split.
 rewrite (_ : g \o shift2 = [fun of g] \o [fun of shift2]) // => /negP P.
 apply: funS; apply/andP; split => //; move: P; apply: contra_notP => /=.
 by move=> /negP; rewrite -ltNge => /ltW ?; apply/mem_set/andP; split.
 Qed.
 
-Lemma chain_init : chain 0 = x1.
+Lemma chain_init : ftheng 0 = x1.
 Proof. 
-rewrite /chain patchT /shift1 /= ?(@mul0r R) ?init_point //.
+rewrite /ftheng patchT /shift1 /= ?(@mul0r R) ?init_point //.
 rewrite mem_set //= bound_itvE; apply: divr_ge0 => //.
 Qed.
 
-Lemma chain_final : chain 1 = x3.
+Lemma chain_final : ftheng 1 = x3.
 Proof. 
-rewrite /chain patchC /shift2 /= mul1r. 
+rewrite /ftheng patchC /shift2 /= mul1r. 
   by rewrite (_ : 2 = 1+1) // addrK final_point //. 
 rewrite setCitv /= in_setU; apply/orP; right => /=.
 by rewrite set_itv_o_infty mem_set //= invr_cp1 // ?unitfE // ltr_addr.
 Qed.
 
-HB.instance Definition _ :=  @IsBetween.Build R T x1 x3 chain chain_init chain_final.
-HB.instance Definition _ := @IsPath.Build R T chain h_cts.
-HB.instance Definition _ := @IsFun.Build _ _ _ B chain h_fun.
+HB.instance Definition _ :=  @IsBetween.Build R T x1 x3 ftheng chain_init chain_final.
+HB.instance Definition _ := @IsPath.Build R T ftheng h_cts.
+HB.instance Definition _ := @IsFun.Build _ _ _ B ftheng h_fun.
+
+Definition chain := [path from x1 to x3 of ftheng].
 
 End ChainPath.
+
+Section ChainLoop.
+
+Context (t : T) (f g : {loop R, B at t}).
+
+Lemma chain_loop_at : @IsBetween R T t t (chain f g). 
+Proof. split; [exact: init_point | exact: final_point ]. Qed.
+
+HB.instance Definition _ := chain_loop_at.
+
+End ChainLoop.
+
+Section path_components.
+
+Definition same_path_component (t u : {x : T | B x}) := 
+  `[<exists (p : {path R, B from (projT1 t) to (projT1 u)}), True>].
+
+Lemma reflexive_path_comp : reflexive same_path_component.
+Proof.
+by case=> t Bt; apply/asboolP; exists (constant_path Bt).
+Qed.
+
+Lemma symmetric_path_comp : symmetric same_path_component.
+Proof.
+move=> x y. apply/asbool_equiv_eq; split; case=> f _. 
+  by exists [path from (projT1 y) to (projT1 x) of (reverse_path f)].
+by exists [path from (projT1 x) to (projT1 y) of (reverse_path f)].
+Qed.
+
+Lemma transitive_path_comp : transitive same_path_component.
+Proof.
+move=> ? ? ? /asboolP [f _] /asboolP [g _]; apply/asboolP. 
+by exists (chain f g).
+Qed.
+
+Definition path_components_rel := EquivRel same_path_component 
+  reflexive_path_comp symmetric_path_comp transitive_path_comp.
+
+End path_components.