Module mathcomp.analysis.homotopy_theory.continuous_path
From HB Require Import structures.From mathcomp Require Import boot order generic_quotient algebra finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import 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
Unset 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.
HBSource code.mixinSource code RecordSource code isPathSource code {iSource code :Source code bpTopologicalType}Source code {T : topologicalType} (x y : T)
(f : i -> T) & isContinuous i T f := {
path_zero : f zero = x;
path_one : f one = y;
}.
#[shortSource code(type=Source code"pathType"Source code)]Source code
HBSource code.structureSource code DefinitionSource code PathSource code {iSource code :Source code bpTopologicalType}Source code {T : topologicalType}
(x y : T) := {fSource code of isPath i T x y f & isContinuous i T f}.
Notation "{ 'path' i 'from' x 'to' y }"Source code := (pathType i x y) : type_scope.
Notation "{ 'path' i 'from' x 'to' y 'in' T }"Source code :=
(@pathType i T x y) : type_scope.
HBSource code.instanceSource code DefinitionSource code _Source code {iSource code :Source code bpTopologicalType}Source code
{T : topologicalType} (x y : T) := gen_eqMixin {path i from x to y}.
HBSource code.instanceSource code DefinitionSource code _Source code {iSource code :Source code bpTopologicalType}Source code
{T : topologicalType} (x y : T) := gen_choiceMixin {path i from x to y}.
HBSource code.instanceSource code DefinitionSource code _Source code {iSource code :Source code bpTopologicalType}Source code
{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 {TSource code : topologicalType} {iSource code : bpTopologicalType} (xSource code ySource code : T).
Lemma path_eqPSource code (aSource code bSource code : {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.
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 {TSource code : topologicalType} {iSource code : bpTopologicalType} (xSource code: T).
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @isPathSource code.Build i T x x (cst x) erefl erefl.
End cst_path.
Section path_domain_path.
Context {iSource code : bpTopologicalType}.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @isPathSource code.Build i i zero one idfun erefl erefl.
End path_domain_path.
Section path_compose.
Context {TSource code USource code : topologicalType} (iSource code: bpTopologicalType) (xSource code ySource code : T).
Context (fSource code : continuousType T U) (pSource code : {path i from x to y}).
Local Lemma fp_zeroSource code : (f \o p) zero = f x.
Proof.
Local Lemma fp_oneSource code : (f \o p) one = f y.
Proof.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isPathSource code.Build i U (f x) (f y) (f \o p)
fp_zero fp_one.
End path_compose.
Section path_reparameterize.
Context {TSource code : topologicalType} (iSource code jSource code: bpTopologicalType) (xSource code ySource code : T).
Context (fSource code : {path i from x to y}) (phiSource code : {path j from zero to one in i}).
Definition reparameterize
Source code := f \o phi.
Let fphi_zeroSource code : reparameterize zero = x.
Proof.
Let fphi_oneSource code : reparameterize one = y.
Proof.
Let fphi_ctsSource code : continuous reparameterize.
Proof.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isContinuousSource code.Build _ _ reparameterize fphi_cts.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isPathSource code.Build j T x y reparameterize
fphi_zero fphi_one.
End path_reparameterize.
Section mk_path.
Context {iSource code : bpTopologicalType} {TSource code : topologicalType}.
Context {xSource code ySource code : T} (fSource code : i -> T) (ctsfSource code : continuous f).
Context (f0Source code : f zero = x) (f1Source code : f one = y).
Definition mk_path
Source code : i -> T := let _ := (ctsf, f0, f1) in f.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isContinuousSource code.Build i T mk_path ctsf.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @isPathSource code.Build i T x y mk_path f0 f1.
End mk_path.
Definition chain_path
Source code {iSource code jSource code : bpTopologicalType} {TSource code : topologicalType}
(fSource code : i -> T) (gSource code : j -> T) : bpwedge i j -> T :=
wedge_fun (fun bSource code => if bSource code return (if b then i else j) -> T then f else g).
Lemma chain_path_cts_pointSource code {iSource code jSource code : bpTopologicalType} {TSource code : topologicalType}
(fSource code : i -> T) (gSource code : j -> T) :
continuous f ->
continuous g ->
f one = g zero ->
continuous (chain_path f g).
Proof.
Section chain_path.
Context {TSource code : topologicalType} {iSource code jSource code : bpTopologicalType} (xSource code ySource code zSource code: T).
Context (pSource code : {path i from x to y}) (qSource code : {path j from y to z}).
Let chain_path_zeroSource code : 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.
by case => //= [][] //=; rewrite ?path_one ?path_zero.
Qed.
Let chain_path_oneSource code : 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.
by case => //= [][] //=; rewrite ?path_one ?path_zero.
Qed.
Let chain_path_ctsSource code : continuous (chain_path p q).
Proof.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @isContinuousSource code.Build _ T (chain_path p q)
chain_path_cts.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @isPathSource code.Build _ T x z (chain_path p q)
chain_path_zero chain_path_one.
End chain_path.