Homotopy between functions #
In this file, we define a homotopy between two functions f₀
and f₁
. First we define
ContinuousMap.Homotopy
between the two functions, with no restrictions on the intermediate
maps. Then, as in the formalisation in HOL-Analysis, we define
ContinuousMap.HomotopyWith f₀ f₁ P
, for homotopies between f₀
and f₁
, where the
intermediate maps satisfy the predicate P
. Finally, we define
ContinuousMap.HomotopyRel f₀ f₁ S
, for homotopies between f₀
and f₁
which are fixed
on S
.
Definitions #
ContinuousMap.Homotopy f₀ f₁
is the type of homotopies betweenf₀
andf₁
.ContinuousMap.HomotopyWith f₀ f₁ P
is the type of homotopies betweenf₀
andf₁
, where the intermediate maps satisfy the predicateP
.ContinuousMap.HomotopyRel f₀ f₁ S
is the type of homotopies betweenf₀
andf₁
which are fixed onS
.
For each of the above, we have
refl f
, which is the constant homotopy fromf
tof
.symm F
, which reverses the homotopyF
. For example, ifF : ContinuousMap.Homotopy f₀ f₁
, thenF.symm : ContinuousMap.Homotopy f₁ f₀
.trans F G
, which concatenates the homotopiesF
andG
. For example, ifF : ContinuousMap.Homotopy f₀ f₁
andG : ContinuousMap.Homotopy f₁ f₂
, thenF.trans G : ContinuousMap.Homotopy f₀ f₂
.
We also define the relations
ContinuousMap.Homotopic f₀ f₁
is defined to beNonempty (ContinuousMap.Homotopy f₀ f₁)
ContinuousMap.HomotopicWith f₀ f₁ P
is defined to beNonempty (ContinuousMap.HomotopyWith f₀ f₁ P)
ContinuousMap.HomotopicRel f₀ f₁ P
is defined to beNonempty (ContinuousMap.HomotopyRel f₀ f₁ P)
and for ContinuousMap.homotopic
and ContinuousMap.homotopic_rel
, we also define the
setoid
and quotient
in C(X, Y)
by these relations.
References #
- toFun : ↑unitInterval × X → Y
- continuous_toFun : Continuous s.toFun
- map_zero_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (0, x) = ↑f₀ x
value of the homotopy at 0
- map_one_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (1, x) = ↑f₁ x
value of the homotopy at 1
ContinuousMap.Homotopy f₀ f₁
is the type of homotopies from f₀
to f₁
.
When possible, instead of parametrizing results over (f : Homotopy f₀ f₁)
,
you should parametrize over {F : Type*} [HomotopyLike F f₀ f₁] (f : F)
.
When you extend this structure, make sure to extend ContinuousMap.HomotopyLike
.
Instances For
- coe : F → ↑unitInterval × X → Y
- coe_injective' : Function.Injective FunLike.coe
- map_continuous : ∀ (f : F), Continuous ↑f
- map_zero_left : ∀ (f : F) (x : X), ↑f (0, x) = ↑f₀ x
value of the homotopy at 0
- map_one_left : ∀ (f : F) (x : X), ↑f (1, x) = ↑f₁ x
value of the homotopy at 1
ContinuousMap.HomotopyLike F f₀ f₁
states that F
is a type of homotopies between f₀
and
f₁
.
You should extend this class when you extend ContinuousMap.Homotopy
.
Instances
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Instances For
Deprecated. Use map_continuous
instead.
Currying a homotopy to a continuous function from I
to C(X, Y)
.
Instances For
Continuously extending a curried homotopy to a function from ℝ
to C(X, Y)
.
Instances For
Given a continuous function f
, we can define a Homotopy f f
by F (t, x) = f x
Instances For
Given a Homotopy f₀ f₁
, we can define a Homotopy f₁ f₀
by reversing the homotopy.
Instances For
Given Homotopy f₀ f₁
and Homotopy f₁ f₂
, we can define a Homotopy f₀ f₂
by putting the first
homotopy on [0, 1/2]
and the second on [1/2, 1]
.
Instances For
Casting a Homotopy f₀ f₁
to a Homotopy g₀ g₁
where f₀ = g₀
and f₁ = g₁
.
Instances For
Composition of a Homotopy g₀ g₁
and f : C(X, Y)
as a homotopy between g₀.comp f
and
g₁.comp f
.
Instances For
If we have a Homotopy f₀ f₁
and a Homotopy g₀ g₁
, then we can compose them and get a
Homotopy (g₀.comp f₀) (g₁.comp f₁)
.
Instances For
Let F
be a homotopy between f₀ : C(X, Y)
and f₁ : C(X, Y)
. Let G
be a homotopy between
g₀ : C(X, Z)
and g₁ : C(X, Z)
. Then F.prodMk G
is the homotopy between f₀.prodMk g₀
and
f₁.prodMk g₁
that sends p
to (F p, G p)
.
Instances For
Let F
be a homotopy between f₀ : C(X, Y)
and f₁ : C(X, Y)
. Let G
be a homotopy between
g₀ : C(Z, Z')
and g₁ : C(Z, Z')
. Then F.prodMap G
is the homotopy between f₀.prodMap g₀
and
f₁.prodMap g₁
that sends (t, x, z)
to (F (t, x), G (t, z))
.
Instances For
Given a family of homotopies F i
between f₀ i : C(X, Y i)
and f₁ i : C(X, Y i)
, returns a
homotopy between ContinuousMap.pi f₀
and ContinuousMap.pi f₁
.
Instances For
Given a family of homotopies F i
between f₀ i : C(X i, Y i)
and f₁ i : C(X i, Y i)
,
returns a homotopy between ContinuousMap.piMap f₀
and ContinuousMap.piMap f₁
.
Instances For
Given continuous maps f₀
and f₁
, we say f₀
and f₁
are homotopic if there exists a
Homotopy f₀ f₁
.
Instances For
If each f₀ i : C(X, Y i)
is homotopic to f₁ i : C(X, Y i)
, then ContinuousMap.pi f₀
is
homotopic to ContinuousMap.pi f₁
.
If each f₀ i : C(X, Y i)
is homotopic to f₁ i : C(X, Y i)
, then ContinuousMap.pi f₀
is
homotopic to ContinuousMap.pi f₁
.
- toFun : ↑unitInterval × X → Y
- continuous_toFun : Continuous s.toFun
- map_zero_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (0, x) = ↑f₀ x
- map_one_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (1, x) = ↑f₁ x
- prop' : ∀ (t : ↑unitInterval), P (ContinuousMap.mk fun x => ContinuousMap.toFun s.toContinuousMap (t, x))
the intermediate maps of the homotopy satisfy the property
The type of homotopies between f₀ f₁ : C(X, Y)
, where the intermediate maps satisfy the predicate
P : C(X, Y) → Prop
Instances For
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Instances For
Given a continuous function f
, and a proof h : P f
, we can define a HomotopyWith f f P
by
F (t, x) = f x
Instances For
Given a HomotopyWith f₀ f₁ P
, we can define a HomotopyWith f₁ f₀ P
by reversing the homotopy.
Instances For
Given HomotopyWith f₀ f₁ P
and HomotopyWith f₁ f₂ P
, we can define a HomotopyWith f₀ f₂ P
by putting the first homotopy on [0, 1/2]
and the second on [1/2, 1]
.
Instances For
Casting a HomotopyWith f₀ f₁ P
to a HomotopyWith g₀ g₁ P
where f₀ = g₀
and f₁ = g₁
.
Instances For
Given continuous maps f₀
and f₁
, we say f₀
and f₁
are homotopic with respect to the
predicate P
if there exists a HomotopyWith f₀ f₁ P
.
Instances For
A HomotopyRel f₀ f₁ S
is a homotopy between f₀
and f₁
which is fixed on the points in S
.
Instances For
Given a map f : C(X, Y)
and a set S
, we can define a HomotopyRel f f S
by setting
F (t, x) = f x
for all t
. This is defined using HomotopyWith.refl
, but with the proof
filled in.
Instances For
Given a HomotopyRel f₀ f₁ S
, we can define a HomotopyRel f₁ f₀ S
by reversing the homotopy.
Instances For
Given HomotopyRel f₀ f₁ S
and HomotopyRel f₁ f₂ S
, we can define a HomotopyRel f₀ f₂ S
by putting the first homotopy on [0, 1/2]
and the second on [1/2, 1]
.
Instances For
Casting a HomotopyRel f₀ f₁ S
to a HomotopyRel g₀ g₁ S
where f₀ = g₀
and f₁ = g₁
.
Instances For
Given continuous maps f₀
and f₁
, we say f₀
and f₁
are homotopic relative to a set S
if
there exists a HomotopyRel f₀ f₁ S
.
Instances For
If two maps are homotopic relative to a set, then they are homotopic.