Skip to content

Commit

Permalink
more homotopy stuff
Browse files Browse the repository at this point in the history
  • Loading branch information
@zstone1
zstone1 committed Sep 15, 2022
1 parent e18544c commit 29b1f5f
Showing 1 changed file with 253 additions and 59 deletions.
312 changes: 253 additions & 59 deletions theories/homotopy.v
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,18 @@
(* 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.
Require Import boolp reals ereal mathcomp_extra classical_sets signed functions.
Require Import topology normedtype landau set_interval.
Require Import realfun .
Require Import mathcomp_extra boolp reals ereal set_interval classical_sets.
Require Import signed functions topology normedtype landau sequences derive.
From HB Require Import structures.

Add Search Blacklist "__canonical__".
Add Search Blacklist "__functions_".
Add Search Blacklist "_factory_".
Add Search Blacklist "_mixin_".

(******************************************************************************)
(* Definitions and lemmas homotopies *)
(* Definitions and lemmas for homotopy theory *)
(* *)
(* *)
(******************************************************************************)
Expand All @@ -24,109 +26,301 @@ Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.


HB.mixin Record IsPath {R : realType} {T : topologicalType} (f : R -> T):=
HB.mixin Record IsPath {R : realType} {T : topologicalType} (f : R -> T) :=
{ path_continuous : {within `[0,1], continuous 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 & IsFun _ _ `[0,1]%classic B f }.
(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.

HB.instance Definition _ {R : realType} {T : topologicalType}
(B : set T) (f : {path R, B}) := Fun.on f.
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 }.

HB.mixin Record CrossingFree {R : realType} {T : topologicalType}
(f : R -> T) := { inj_interior : set_inj `[0,1[ f /\ set_inj `]0,1] f }.
HB.structure Definition JustClosed {R : realType} {T : topologicalType}
:= {f of IsClosed R T f}.

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 _ _ B) : form_scope.
Notation "{ 'loop' R , B }" := (@Loop.type R _ B) : 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) :=
{ init_point : f 0 = init; final_point : f 1 = final; }.
HB.structure Definition JustBetween {R : realType} {T : topologicalType}
(init final : T) :=
{ f of @IsBetween R T init final f }.


HB.structure Definition PathBetween {R : realType} {T : topologicalType}
(init final : T) (B : set T) :=
{ 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.

HB.structure Definition JordanCurve {R : realType} {T : topologicalType}
(B : set T):= { f of @Loop R T B f & @CrossingFree R T f }.
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 "{ 'jordan curve on' B }" := (@JordanCurve.type _ _ B) : form_scope.
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.

Section Paths.
Context {R : realType} {T : topologicalType}.
Section ConstantPath.
Context {R : realType} {T : topologicalType} (x : T).
Context (B : set T) (x : T).
Hypothesis Bx : B x.
Let f : R -> T := fun=> x.

Local Lemma cst_fun : set_fun `[0,1]%classic [set x] f.
Local Lemma cst_fun : set_fun `[0,1]%classic B f.
Proof. by []. Qed.
HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun.

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

Local Lemma cst_closed : f 0 = f 1.
Proof. by []. Qed.
HB.instance Definition _ := @IsClosed.Build R T f cst_closed.
HB.instance Definition _ := @IsClosed.Build R T f (erefl _).
HB.instance Definition _ := @IsBetween.Build R T x x f (erefl _) (erefl _).

Definition constant_path := [the (@Loop.type R T [set x]) of f].
Definition constant_path := [loop at x of f].
End ConstantPath.

Section PathShift.
Context {R : realType} {T : topologicalType} (B : set T) (f : {path R, B}).

Lemma shift_path (shift : {fun `[(0:R),1]%classic >-> `[(0:R),1]%classic}) :
Lemma shift_path (B : set T) (f : {path R, B}) (shift : {fun `[(0:R),1]%classic >-> `[(0:R),1]%classic}) :
(continuous (shift : subspace `[0,1] -> subspace `[0,1])) ->
IsPath _ _ (f \o shift).
{within `[0,1], continuous (f \o shift)}.
Proof.
move=> cts; split=> x.
apply: (@continuous_comp (subspace_topologicalType `[0,1])
(subspace_topologicalType `[0,1]) _).
move=> cts x.
apply: (@continuous_comp
(subspace_topologicalType `[0,1]) (subspace_topologicalType `[0,1]) _).
exact: cts.
exact: path_continuous.
Qed.

End PathShift.
Let flip_f (x : subspace `[(0:R),1]) : subspace `[0,1] := `1- x.

Lemma subspace_continuous_restricted {T : topologicalType} (A : set T)
(f : {fun A >-> A}) :
continuous (f : T -> T) -> continuous (f : subspace A -> subspace A).
Lemma path_rev_funS : @set_fun _ _ `[0,1]%classic `[0,1]%classic flip_f.
Proof.
move=> /continuousP ctsf; apply/continuousP=> U /open_subspaceP [V].
case=> ofV VAUA; apply/open_subspaceP; exists (f@^-1` V); split.
exact: ctsf.
rewrite eqEsubset; split=> x [] ? ?; split=> //; have: A (f x) by exact: funS.
by move=> afx; have: (V `&` A) (f x) by []; rewrite VAUA=> [[]].
by move=> afx; have: (U `&` A) (f x) by []; rewrite -VAUA=> [[]].
rewrite ?set_itvcc => x /= /andP [] xnng xle1; apply/andP.
split; [exact: onem_ge0| exact: onem_le1].
Qed.

HB.instance Definition _ :=
@IsFun.Build R R (`[0,1]%classic) (`[0,1]%classic) (flip_f) path_rev_funS.

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=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
exact: opp_continuous.
*)
Admitted.

Section ReversePath.
Context {R : realType} {T : topologicalType}.
Variables (B : set T) (f : {path R, B}).

Definition flip_path := [fun of f] \o [fun of flip_f].

Definition path_rev (x : subspace `[(0:R),1]) : subspace `[0,1] := `1- x.
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).

HB.instance Definition _ :=
@IsFun.Build R T `[0,1]%classic B flip_path flip_path_funS.

Lemma path_rev_funS : @set_fun _ _ `[0,1]%classic `[0,1]%classic path_rev.
Definition reverse_path := [path of flip_path].
End ReversePath.

Section RevLoop.
Context {t1 t2 : T} {B : set T} (f : {loop R, B}).
Lemma rev_loop : @IsClosed R T (reverse_path f).
Proof.
rewrite ?set_itvcc => x /= /andP [] xnng xle1; apply/andP.
split; [exact: onem_ge0| exact: onem_le1].
by split; rewrite /= /flip_path /= /flip_f onem0 onem1 -endpointsE.
Qed.

HB.instance Definition _ :=
@IsFun.Build R R (`[0,1]%classic) (`[0,1]%classic) (path_rev) path_rev_funS.
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)].

Section RevPathBetween.
Context {t1 t2 : T} {B : set 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.
by rewrite final_point.
by rewrite init_point.
Qed.
HB.instance Definition _ := @rev_pathbetween.

Definition foo := [path of reverse_path f ].

Lemma rev_cts: continuous path_rev.
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 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 nbhs_subspaceW {T : topologicalType} (A : set T) (B : set T) (x : T) :
nbhs (x : T) B -> nbhs (x : subspace A) B.
Proof.
move=> z; apply: subspace_continuous_restricted; rewrite /= /path_rev.
move=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
exact: opp_continuous.
rewrite ?nbhsE /= => [[]] O [[]] oO Ox oB; exists O; split => //.
by split=> //; exact: open_subspaceW.
Qed.

HB.instance Definition _ (B : set T) (f : {path R, B}) :=
@shift_path R T B f [fun of path_rev] rev_cts.
Section ChainPath.
Context {R : realType} {T : topologicalType} (B : set T).
Variables (f g : {path R, B}).
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.

Lemma rev_loop (B : set T) {f : @Loop.type R T B} :
@IsClosed R T (f \o path_rev).
Proof. by split; rewrite /path_rev /= onem0 onem1 -endpointsE. Qed.
Local Lemma shift1fun :
@set_fun R R `[0,1/2]%classic `[0,1]%classic shift1.
Proof.
move=> r; rewrite /shift1 ?set_itvcc /= =>/andP.
case=> ? rh; apply/andP; split; first exact: mulr_ge0.
by rewrite -ler_pdivl_mulr.
Qed.

HB.instance Definition _ (B : set T) (f : {loop R, B}) := @rev_loop B f.
HB.instance Definition _ := IsFun.Build _ _ _ _ _ shift1fun.

Lemma h_cts1 : {within `[0,1/2], continuous chain}.
apply: (@subspace_eq_continuous _ _ _ (f \o shift1)).
move=> q1 q2; apply: sym_equal; move: q1 q2.
apply patchT.
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.
by move => z; apply: (@continuousM R R _ _ z) => //; exact: cst_continuous.
Qed.

Local Lemma shift2fun :
@set_fun R R `[1/2,1]%classic `[0,1]%classic shift2.
Proof.
move=> r; rewrite /shift2 ?set_itvcc /= =>/andP.
case=> ? rh; apply/andP; split.
by rewrite ler_subr_addl addr0 -ler_pdivr_mulr.
by rewrite ler_subl_addr -ler_pdivl_mulr // divff.
Qed.

HB.instance Definition _ := IsFun.Build _ _ _ _ _ shift2fun.

Lemma h_cts2 : {within `[1/2,1], continuous chain}.
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 [? ?].
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.
move=> P Q; suff -> : q = 1/2.
rewrite /shift2 /shift1 divfK // subrr; exact: f1g0.
case/set_mem/andP: P => qpos qhlf.
move/negP:Q => /=; apply: contra_notP=> qnhlf.
apply/mem_set/andP; split => //.
by move: qhlf; rewrite le_eqVlt=> /orP [] // /eqP.
apply: (@subspace_eq_continuous _ _ _ (g \o shift2)).
rewrite set_itvcc => q /set_mem/andP [halfp ?]; apply/sym_equal/patchC.
rewrite set_itvco; apply/mem_set => /andP [?].
by apply/negP; rewrite -leNgt.
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.
move => z /=; rewrite /shift2.
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}.
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].
- apply/andP; split => //; apply: (ge_trans _ ub) => /=.
by rewrite ler_pdivr_mulr // mul1r -ler_subl_addr subrr.
- by apply/andP; split => //; apply: (ge_trans lb) => /=.
- case/orP: (@real_leVge R r (1/2) (num_real _) (num_real _)) => rh.
by left; apply/andP; split.
by right; apply/andP; split.
move=> <-; apply: pasting; (try exact: interval_closed).
exact: h_cts1.
exact: h_cts2.
Qed.

End ReversePath.
Lemma h_fun : set_fun `[0,1]%classic B chain.
Proof.
move=> r; rewrite set_itvcc => /andP [] ? ?.
rewrite /chain/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.

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.

HB.structure Definition PathHomotopy {R : realType} {T : topologicalType}
(B : set T) := { f of IsPathHomotopy R T f & IsFun _ _ square B f }.

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

0 comments on commit 29b1f5f

Please sign in to comment.