Skip to content

Commit

Permalink
path chains
Browse files Browse the repository at this point in the history
  • Loading branch information
@zstone1
zstone1 committed Sep 15, 2022
1 parent 29b1f5f commit 47fa00d
Showing 1 changed file with 47 additions and 81 deletions.
128 changes: 47 additions & 81 deletions theories/homotopy.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ 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}.

Notation "{ 'path' R , B }" := (@Path.type R _ B) : form_scope.
Notation "[ 'path' 'of' f ]" := ([the (@Path.type _ _ _) of f]) : form_scope.
Notation "[ 'path' 'of' f ]" := ([the (@Path.type _ _ _) of (f: _ -> _)]) : form_scope.

HB.mixin Record IsClosed {R : realType} {T : topologicalType}
(f : R -> T) := { endpointsE : f 0 = f 1 }.
Expand All @@ -47,7 +47,7 @@ HB.structure Definition Loop {R : realType} {T : topologicalType}
(B : set T):= { f of @Path R _ B f & @IsClosed R T f}.

Notation "{ 'loop' R , B }" := (@Loop.type R _ B) : form_scope.
Notation "[ 'loop' 'of' f ]" := ([the (@Loop.type _ _ _) of f]) : form_scope.
Notation "[ 'loop' 'of' f ]" := ([the (@Loop.type _ _ _) of (f : _ -> _)]) : form_scope.

HB.mixin Record IsBetween {R : realType} {T : topologicalType}
(init final : T) (f : R -> T) :=
Expand All @@ -62,14 +62,14 @@ HB.structure Definition PathBetween {R : realType} {T : topologicalType}
{ f of @Path R T B f & @IsBetween R T init final f}.

Notation "{ 'path' R , B 'from' t1 'to' t2 }" := (@PathBetween.type R _ t1 t2 B) : form_scope.
Notation "[ 'path' 'from' t1 'to' t2 'of' f ]" := ([the (@PathBetween.type _ _ t1 t2 _) of f]) : form_scope.
Notation "[ 'path' 'from' t1 'to' t2 'of' f ]" := ([the (@PathBetween.type _ _ t1 t2 _) of (f : _ -> _)]) : form_scope.

HB.structure Definition LoopAt {R : realType} {T : topologicalType}
(init : T) (B : set T) :=
{ f of @Loop R T B f & @IsBetween R T init init f}.

Notation "{ 'loop' R , B `on` t }" := (@LoopAt.type R _ t B) : form_scope.
Notation "[ 'loop' 'at' t 'of' f ]" := ([the (@LoopAt.type _ _ t _) of f]) : form_scope.
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}.
Expand All @@ -83,7 +83,7 @@ Proof. by []. Qed.
HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun.

Local Lemma cst_path : {within `[0,1], continuous f}.
Proof. by apply: subspace_restrict_domain => ? ?; exact: cst_continuous. Qed.
Proof. by apply: continuous_subspaceT => ? ?; exact: cst_continuous. Qed.
HB.instance Definition _ := @IsPath.Build R T f cst_path.

HB.instance Definition _ := @IsClosed.Build R T f (erefl _).
Expand Down Expand Up @@ -116,13 +116,11 @@ HB.instance Definition _ :=

Lemma rev_cts: continuous flip_f.
Proof.
(* need to merge 739 for this*)
(*move=> z; apply: subspace_continuous_restricted; rewrite /= /flip_f.
move=> ?; apply: subspace_restrict_domain.
move=> z; apply: subspaceT_continuous; rewrite /= /flip_f.
move=> ?; apply: continuous_subspaceT.
move=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
exact: opp_continuous.
*)
Admitted.
Qed.

Section ReversePath.
Variables (B : set T) (f : {path R, B}).
Expand All @@ -138,6 +136,7 @@ HB.instance Definition _ :=
HB.instance Definition _ :=
@IsFun.Build R T `[0,1]%classic B flip_path flip_path_funS.


Definition reverse_path := [path of flip_path].
End ReversePath.

Expand All @@ -149,9 +148,7 @@ by split; rewrite /= /flip_path /= /flip_f onem0 onem1 -endpointsE.
Qed.

HB.instance Definition _ := rev_loop.

Definition foo := [the (@Path.type R T B) of (reverse_path f)].
Definition bar := [the (@JustClosed.type R T) of (reverse_path f)].
End RevLoop.

Section RevPathBetween.
Context {t1 t2 : T} {B : set T} (f : {path R, B from t1 to t2}).
Expand All @@ -161,40 +158,31 @@ split; rewrite /= /flip_path /= /flip_f ?onem1 ?onem0.
by rewrite final_point.
by rewrite init_point.
Qed.

HB.instance Definition _ := @rev_pathbetween.

Definition foo := [path of reverse_path f ].
End RevPathBetween.

Lemma rev_loopAt {t1 : T} {B : set T} (f : {path R, B from t1 to t2}) :
@IsBetween R T t2 t1 (reverse_path f).
Proof.
split; rewrite /= /flip_path /= /flip_f ?onem1 ?onem0.
by rewrite final_point.
by rewrite init_point.
Qed.
HB.instance Definition _ t1 t2 B f := @rev_pathbetween t1 t2 B f.
Section ReverseLoopAtBetween.
Context {B : set T} (t : T) (f : {loop R, B at t}).

Section ReversePathBetween
Context {B : set T} (f : {loop R, B}).
Lemma rev_loop : @IsClosed R T (reverse_path f).
Proof.
by split; rewrite /reverse_path //= /flip_path /= onem0 onem1 -endpointsE.
Qed.
Lemma rev_loop_at : @IsBetween R T t t (reverse_path f).
Proof. apply: rev_pathbetween. Qed.

Lemma nbhs_subspaceW {T : topologicalType} (A : set T) (B : set T) (x : T) :
nbhs (x : T) B -> nbhs (x : subspace A) B.
Proof.
rewrite ?nbhsE /= => [[]] O [[]] oO Ox oB; exists O; split => //.
by split=> //; exact: open_subspaceW.
Qed.
HB.instance Definition _ := @rev_loop_at.
End ReverseLoopAtBetween.

(*
Why doesn't this work?
Definition foo := [path from t to t of (reverse_path f)].
*)

Section ChainPath.
Context {R : realType} {T : topologicalType} (B : set T).
Variables (f g : {path R, B}).
Context (B : set T) (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).
Hypothesis f1g0 : g 0 = f 1.

Local Lemma shift1fun :
@set_fun R R `[0,1/2]%classic `[0,1]%classic shift1.
Expand All @@ -214,7 +202,7 @@ move=> x; apply: (@continuous_comp
[topologicalType of (subspace `[0,1/2])]
[topologicalType of (subspace `[0,1])]
T _ _ x); last exact: path_continuous.
apply: subspace_restrict_range; apply: subspace_restrict_domain.
apply: subspaceT_continuous; apply: continuous_subspaceT.
by move => z; apply: (@continuousM R R _ _ z) => //; exact: cst_continuous.
Qed.

Expand All @@ -237,7 +225,8 @@ apply: (@subspace_eq_continuous _ _ _ h2 chain).
move=> /negP /= P /set_mem/andP [] ? ?; contradict P.
by apply: mem_set; apply/andP; split => //; exact: ltW.
move=> P Q; suff -> : q = 1/2.
rewrite /shift2 /shift1 divfK // subrr; exact: f1g0.
by rewrite /shift2 /shift1 divfK // subrr final_point init_point.

case/set_mem/andP: P => qpos qhlf.
move/negP:Q => /=; apply: contra_notP=> qnhlf.
apply/mem_set/andP; split => //.
Expand All @@ -250,7 +239,7 @@ move=> x; apply: (@continuous_comp
[topologicalType of (subspace `[1/2, 1])]
[topologicalType of (subspace `[0,1])]
T _ _ x); last exact: path_continuous.
apply: subspace_restrict_range; apply: subspace_restrict_domain.
apply: subspaceT_continuous; apply: continuous_subspaceT.
move => z /=; rewrite /shift2.
apply (@continuousD R R R) => //; last exact: cst_continuous.
apply (@continuousM R) => //; last exact: cst_continuous.
Expand Down Expand Up @@ -282,45 +271,22 @@ apply: funS; apply/andP; split => //; move: P; apply: contra_notP => /=.
by move=> /negP; rewrite -ltNge => /ltW ?; apply/mem_set/andP; split.
Qed.

HB.instance Definition p1 := @IsPath.Build R T chain h_cts.
HB.instance Definition p2 := @IsFun.Build _ _ _ B chain h_fun.

Definition chain_path := [path of chain].
End ChainPath.

Section ChainLoop.
Context {R : realType} {T : topologicalType} (B : set T).
Variables (f g : {loop R, B}).

Lemma fgpoint : f 1 = g 0.
Proof.
rewrite (@endpointsE _ _ _ f).

Definition chain_loop_aux = chain_path ()

Lemma chain_reverse {R : realType} {T : topologicalType} (B : set T) (f : {path R, B}) :
(chain f (rev_path f)) 0 =
(chain f (f \o path_rev)) 1.

Section HomotopiesAsPaths.
Context {R : realType} {T : uniformType} (B : set T) (x : T).
Hypothesis Bx : B x.

Canonical paths_eqType := EqType {path R, B} gen_eqMixin.
Canonical paths_choiceType := ChoiceType {path R, B} gen_choiceMixin.
Canonical paths_PointedType :=
PointedType {path R, B} (@constant_path R T B x Bx).

Definition include (f : {path R, B}) : {uniform` `[(0:R),1]%classic -> T} := f.

Canonical PathSpace {R : realType} {T : uniformType} (B : set T) :=
weak_topologicalType include.
End HomotopiesAsPaths.
Lemma chain_init : chain 0 = x1.
Proof.
rewrite /chain patchT /shift1 /= ?(@mul0r R) ?init_point //.
rewrite mem_set //= bound_itvE; apply: divr_ge0 => //.
Qed.

HB.structure Definition PathHomotopy {R : realType} {T : topologicalType}
(B : set T) := { f of IsPathHomotopy R T f & IsFun _ _ square B f }.
Lemma chain_final : chain 1 = x3.
Proof.
rewrite /chain 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.

Lemma hpath_path (h : @PathHomotopy.type R T B) :
IsPath R _ (hpath h).
Proof.
split.
End ChainPath.

0 comments on commit 47fa00d

Please sign in to comment.