Module mathcomp.analysis.homotopy_theory.continuous_path

From HB Require Import structures.
From mathcomp Require Import all_ssreflect_compat generic_quotient all_algebra.
From mathcomp Require Import finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop reals topology wedge_sigT.

# Paths Paths from biPointed spaces. ``` mk_path ctsf f0 f1 == constructs a value in `pathType x y` given proofs that the endpoints of `f` are `x` and `y` reparameterize f phi == the path `f` with a different parameterization chain_path f g == the path which follows f, then follows g Only makes sense when `f one = g zero`. The domain is the wedge of domains of `f` and `g`. ``` The type `{path i from x to y in T}` is the continuous functions on the bipointed space i that go from x to y staying in T. It is endowed with - Topology via the compact-open topology

Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Reserved Notation "{ 'path' i 'from' x 'to' y }" (
  at level 0, i at level 69, x at level 69, y at level 69,
  only parsing,
  format "{ 'path' i 'from' x 'to' y }").
Reserved Notation "{ 'path' i 'from' x 'to' y 'in' T }" (
  at level 0, i at level 69, x at level 69, y at level 69, T at level 69,
  format "{ 'path' i 'from' x 'to' y 'in' T }").

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope quotient_scope.

. {T : topologicalType} (x y : T)
    (f : i -> T) & isContinuous i T f := {
  path_zero : f zero = x;
  path_one : f one = y;
}.

()
. {T : topologicalType}
  (x y : T) := { of isPath i T x y f & isContinuous i T f}.

Notation := (pathType i x y) : type_scope.
Notation :=
  (@pathType i T x y) : type_scope.

.
  {T : topologicalType} (x y : T) := gen_eqMixin {path i from x to y}.
.
  {T : topologicalType} (x y : T) := gen_choiceMixin {path i from x to y}.
.
    {T : topologicalType} (x y : T) :=
  Topological.copy {path i from x to y}
    (@initial_topology {path i from x to y} {compact-open, i -> T} id).

Section path_eq.
Context { : topologicalType} { : bpTopologicalType} ( : T).

Lemma ( : {path i from x to y}) : a = b <-> a =1 b.

Proof.

split=> [->//|].
move: a b => [/= f [[+ +]]] [/= g [[+ +]]] fgE.
move/funext : fgE => -> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _).
rewrite (Prop_irrelevance a1 a2) (Prop_irrelevance b1 b2).
by rewrite (Prop_irrelevance c1 c2).
Qed.

End path_eq.

Section cst_path.
Context { : topologicalType} { : bpTopologicalType} (: T).

..Build i T x x (cst x) erefl erefl.
End cst_path.

Section path_domain_path.
Context { : bpTopologicalType}.
..Build i i zero one idfun erefl erefl.
End path_domain_path.

Section path_compose.
Context { : topologicalType} (: bpTopologicalType) ( : T).
Context ( : continuousType T U) ( : {path i from x to y}).

Local Lemma : (f \o p) zero = f x.

Proof.

by rewrite /= !path_zero. Qed.

Local Lemma : (f \o p) one = f y.

Proof.

by rewrite /= !path_one. Qed.

..Build i U (f x) (f y) (f \o p)
fp_zero fp_one.

End path_compose.

Section path_reparameterize.
Context { : topologicalType} ( : bpTopologicalType) ( : T).
Context ( : {path i from x to y}) ( : {path j from zero to one in i}).

Definition := f \o phi.

Local Lemma : reparameterize zero = x.

Proof.

by rewrite /reparameterize /= ?path_zero. Qed.

Local Lemma : reparameterize one = y.

Proof.

by rewrite /reparameterize /= ?path_one. Qed.

Local Lemma : continuous reparameterize.

Proof.

by move=> ?; apply: continuous_comp; apply: cts_fun. Qed.

..Build _ _ reparameterize fphi_cts.

..Build j T x y reparameterize
  fphi_zero fphi_one.

End path_reparameterize.

Section mk_path.
Context { : bpTopologicalType} { : topologicalType}.
Context { : T} ( : i -> T) ( : continuous f).
Context ( : f zero = x) ( : f one = y).

Definition : i -> T := let _ := (ctsf, f0, f1) in f.

..Build i T mk_path ctsf.
..Build i T x y mk_path f0 f1.
End mk_path.

Definition { : bpTopologicalType} { : topologicalType}
    ( : i -> T) ( : j -> T) : bpwedge i j -> T :=
  wedge_fun (fun => if return (if b then i else j) -> T then f else g).

Lemma { : bpTopologicalType} { : topologicalType}
    ( : i -> T) ( : j -> T) :
  continuous f ->
  continuous g ->
  f one = g zero ->
  continuous (chain_path f g).

Proof.

by move=> cf cg fgE; apply: wedge_fun_continuous => // [[]|[] []]. Qed.

Section chain_path.
Context { : topologicalType} { : bpTopologicalType} ( : T).
Context ( : {path i from x to y}) ( : {path j from y to z}).

Local Lemma : chain_path p q zero = x.

Proof.

rewrite /chain_path /= wedge_lift_funE ?path_one ?path_zero //.
by case => //= [][] //=; rewrite ?path_one ?path_zero.
Qed.

Local Lemma : chain_path p q one = z.

Proof.

rewrite /chain_path /= wedge_lift_funE ?path_zero ?path_one //.
by case => //= [][] //=; rewrite ?path_one ?path_zero.
Qed.

Local Lemma : continuous (chain_path p q).

Proof.

apply: chain_path_cts_point; [exact: cts_fun..|].
by rewrite path_zero path_one.
Qed.

.  .Build _ T (chain_path p q)
  chain_path_cts.
.  .Build _ T x z (chain_path p q)
  chain_path_zero chain_path_one.

End chain_path.

Files

Module mathcomp.analysis.homotopy_theory.continuous_path