Homotopy between functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we define a homotopy between two functions f₀ and f₁. First we define
continuous_map.homotopy between the two functions, with no restrictions on the intermediate
maps. Then, as in the formalisation in HOL-Analysis, we define
continuous_map.homotopy_with f₀ f₁ P, for homotopies between f₀ and f₁, where the
intermediate maps satisfy the predicate P. Finally, we define
continuous_map.homotopy_rel f₀ f₁ S, for homotopies between f₀ and f₁ which are fixed
on S.
Definitions #
continuous_map.homotopy f₀ f₁is the type of homotopies betweenf₀andf₁.continuous_map.homotopy_with f₀ f₁ Pis the type of homotopies betweenf₀andf₁, where the intermediate maps satisfy the predicateP.continuous_map.homotopy_rel f₀ f₁ Sis the type of homotopies betweenf₀andf₁which are fixed onS.
For each of the above, we have
refl f, which is the constant homotopy fromftof.symm F, which reverses the homotopyF. For example, ifF : continuous_map.homotopy f₀ f₁, thenF.symm : continuous_map.homotopy f₁ f₀.trans F G, which concatenates the homotopiesFandG. For example, ifF : continuous_map.homotopy f₀ f₁andG : continuous_map.homotopy f₁ f₂, thenF.trans G : continuous_map.homotopy f₀ f₂.
We also define the relations
continuous_map.homotopic f₀ f₁is defined to benonempty (continuous_map.homotopy f₀ f₁)continuous_map.homotopic_with f₀ f₁ Pis defined to benonempty (continuous_map.homotopy_with f₀ f₁ P)continuous_map.homotopic_rel f₀ f₁ Pis defined to benonempty (continuous_map.homotopy_rel f₀ f₁ P)
and for continuous_map.homotopic and continuous_map.homotopic_rel, we also define the
setoid and quotient in C(X, Y) by these relations.
References #
structure
continuous_map.homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f₀ f₁ : C(X, Y)) :
Type (max u v)
- to_continuous_map : C(↥unit_interval × X, Y)
- map_zero_left' : ∀ (x : X), self.to_continuous_map.to_fun (0, x) = ⇑f₀ x
- map_one_left' : ∀ (x : X), self.to_continuous_map.to_fun (1, x) = ⇑f₁ x
continuous_map.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*} [homotopy_like F f₀ f₁] (f : F).
When you extend this structure, make sure to extend continuous_map.homotopy_like.
Instances for continuous_map.homotopy
- continuous_map.homotopy.has_sizeof_inst
- continuous_map.homotopy.continuous_map.homotopy_like
- continuous_map.homotopy.has_coe_to_fun
- continuous_map.homotopy.inhabited
@[nolint, instance]
def
continuous_map.homotopy_like.to_continuous_map_class
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(F : Type u_2)
(f₀ f₁ : out_param C(X, Y))
[self : continuous_map.homotopy_like F f₀ f₁] :
continuous_map_class F (↥unit_interval × X) Y
@[class]
structure
continuous_map.homotopy_like
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(F : Type u_2)
(f₀ f₁ : out_param C(X, Y)) :
Type (max u u_2 v)
- coe : F → Π (a : ↥unit_interval × X), (λ (_x : ↥unit_interval × X), Y) a
- coe_injective' : function.injective continuous_map.homotopy_like.coe
- map_continuous : ∀ (f : F), continuous ⇑f
- map_zero_left : ∀ (f : F) (x : X), ⇑f (0, x) = ⇑f₀ x
- map_one_left : ∀ (f : F) (x : X), ⇑f (1, x) = ⇑f₁ x
continuous_map.homotopy_like F f₀ f₁ states that F is a type of homotopies between f₀ and
f₁.
You should extend this class when you extend continuous_map.homotopy.
Instances of this typeclass
Instances of other typeclasses for continuous_map.homotopy_like
- continuous_map.homotopy_like.has_sizeof_inst
@[protected, instance]
def
continuous_map.homotopy.continuous_map.homotopy_like
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)} :
continuous_map.homotopy_like (f₀.homotopy f₁) f₀ f₁
Equations
- continuous_map.homotopy.continuous_map.homotopy_like = {coe := λ (f : f₀.homotopy f₁), f.to_continuous_map.to_fun, coe_injective' := _, map_continuous := _, map_zero_left := _, map_one_left := _}
@[protected, instance]
def
continuous_map.homotopy.has_coe_to_fun
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)} :
has_coe_to_fun (f₀.homotopy f₁) (λ (_x : f₀.homotopy f₁), ↥unit_interval × X → Y)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[ext]
theorem
continuous_map.homotopy.ext
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{F G : f₀.homotopy f₁}
(h : ∀ (x : ↥unit_interval × X), ⇑F x = ⇑G x) :
F = G
def
continuous_map.homotopy.simps.apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
↥unit_interval × X → Y
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
@[protected]
theorem
continuous_map.homotopy.continuous
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
Deprecated. Use map_continuous instead.
@[simp]
theorem
continuous_map.homotopy.apply_zero
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(x : X) :
@[simp]
theorem
continuous_map.homotopy.apply_one
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(x : X) :
@[simp]
theorem
continuous_map.homotopy.coe_to_continuous_map
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
⇑(F.to_continuous_map) = ⇑F
def
continuous_map.homotopy.curry
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
Currying a homotopy to a continuous function fron I to C(X, Y).
Equations
- F.curry = F.to_continuous_map.curry
@[simp]
theorem
continuous_map.homotopy.curry_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(t : ↥unit_interval)
(x : X) :
noncomputable
def
continuous_map.homotopy.extend
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
Continuously extending a curried homotopy to a function from ℝ to C(X, Y).
Equations
- F.extend = continuous_map.Icc_extend continuous_map.homotopy.extend._proof_1 F.curry
@[simp]
theorem
continuous_map.homotopy.extend_apply_coe
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(t : ↥unit_interval)
(x : X) :
@[simp]
theorem
continuous_map.homotopy.extend_apply_of_mem_I
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
{t : ℝ}
(ht : t ∈ unit_interval)
(x : X) :
theorem
continuous_map.homotopy.congr_fun
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{F G : f₀.homotopy f₁}
(h : F = G)
(x : ↥unit_interval × X) :
theorem
continuous_map.homotopy.congr_arg
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
{x y : ↥unit_interval × X}
(h : x = y) :
def
continuous_map.homotopy.refl
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f : C(X, Y)) :
f.homotopy f
Given a continuous function f, we can define a homotopy f f by F (t, x) = f x
Equations
- continuous_map.homotopy.refl f = {to_continuous_map := {to_fun := λ (x : ↥unit_interval × X), ⇑f x.snd, continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}
@[simp]
theorem
continuous_map.homotopy.refl_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f : C(X, Y))
(x : ↥unit_interval × X) :
⇑(continuous_map.homotopy.refl f) x = ⇑f x.snd
@[protected, instance]
def
continuous_map.homotopy.inhabited
{X : Type u}
[topological_space X] :
inhabited ((continuous_map.id X).homotopy (continuous_map.id X))
Equations
def
continuous_map.homotopy.symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
f₁.homotopy f₀
Given a homotopy f₀ f₁, we can define a homotopy f₁ f₀ by reversing the homotopy.
Equations
- F.symm = {to_continuous_map := {to_fun := λ (x : ↥unit_interval × X), ⇑F (unit_interval.symm x.fst, x.snd), continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}
@[simp]
theorem
continuous_map.homotopy.symm_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(x : ↥unit_interval × X) :
@[simp]
theorem
continuous_map.homotopy.symm_symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy f₁) :
noncomputable
def
continuous_map.homotopy.trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ f₂ : C(X, Y)}
(F : f₀.homotopy f₁)
(G : f₁.homotopy f₂) :
f₀.homotopy f₂
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].
theorem
continuous_map.homotopy.trans_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ f₂ : C(X, Y)}
(F : f₀.homotopy f₁)
(G : f₁.homotopy f₂)
(x : ↥unit_interval × X) :
@[simp]
theorem
continuous_map.homotopy.cast_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁)
(ᾰ : ↥unit_interval × X) :
def
continuous_map.homotopy.cast
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy f₁)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁) :
g₀.homotopy g₁
Casting a homotopy f₀ f₁ to a homotopy g₀ g₁ where f₀ = g₀ and f₁ = g₁.
Equations
- F.cast h₀ h₁ = {to_continuous_map := {to_fun := ⇑F, continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}
@[simp]
theorem
continuous_map.homotopy.hcomp_apply
{X : Type u}
{Y : Type v}
{Z : Type w}
[topological_space X]
[topological_space Y]
[topological_space Z]
{f₀ f₁ : C(X, Y)}
{g₀ g₁ : C(Y, Z)}
(F : f₀.homotopy f₁)
(G : g₀.homotopy g₁)
(x : ↥unit_interval × X) :
def
continuous_map.homotopy.hcomp
{X : Type u}
{Y : Type v}
{Z : Type w}
[topological_space X]
[topological_space Y]
[topological_space Z]
{f₀ f₁ : C(X, Y)}
{g₀ g₁ : C(Y, Z)}
(F : f₀.homotopy f₁)
(G : g₀.homotopy g₁) :
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₁).
Equations
- F.hcomp G = {to_continuous_map := {to_fun := λ (x : ↥unit_interval × X), ⇑G (x.fst, ⇑F x), continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}
def
continuous_map.homotopic
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f₀ f₁ : C(X, Y)) :
Prop
Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic if there exists a
homotopy f₀ f₁.
@[refl]
theorem
continuous_map.homotopic.refl
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f : C(X, Y)) :
f.homotopic f
@[symm]
theorem
continuous_map.homotopic.symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
⦃f g : C(X, Y)⦄
(h : f.homotopic g) :
g.homotopic f
@[trans]
theorem
continuous_map.homotopic.trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
⦃f g h : C(X, Y)⦄
(h₀ : f.homotopic g)
(h₁ : g.homotopic h) :
f.homotopic h
theorem
continuous_map.homotopic.hcomp
{X : Type u}
{Y : Type v}
{Z : Type w}
[topological_space X]
[topological_space Y]
[topological_space Z]
{f₀ f₁ : C(X, Y)}
{g₀ g₁ : C(Y, Z)}
(h₀ : f₀.homotopic f₁)
(h₁ : g₀.homotopic g₁) :
theorem
continuous_map.homotopic.equivalence
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y] :
structure
continuous_map.homotopy_with
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f₀ f₁ : C(X, Y))
(P : C(X, Y) → Prop) :
Type (max u v)
- to_homotopy : f₀.homotopy f₁
- prop' : ∀ (t : ↥unit_interval), P {to_fun := λ (x : X), self.to_homotopy.to_continuous_map.to_fun (t, x), continuous_to_fun := _}
The type of homotopies between f₀ f₁ : C(X, Y), where the intermediate maps satisfy the predicate
P : C(X, Y) → Prop
Instances for continuous_map.homotopy_with
- continuous_map.homotopy_with.has_sizeof_inst
- continuous_map.homotopy_with.has_coe_to_fun
- continuous_map.homotopy_with.inhabited
- path.homotopy.has_coe_to_fun
@[protected, instance]
def
continuous_map.homotopy_with.has_coe_to_fun
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop} :
has_coe_to_fun (f₀.homotopy_with f₁ P) (λ (_x : f₀.homotopy_with f₁ P), ↥unit_interval × X → Y)
Equations
- continuous_map.homotopy_with.has_coe_to_fun = {coe := λ (F : f₀.homotopy_with f₁ P), F.to_homotopy.to_continuous_map.to_fun}
theorem
continuous_map.homotopy_with.coe_fn_injective
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop} :
@[ext]
theorem
continuous_map.homotopy_with.ext
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
{F G : f₀.homotopy_with f₁ P}
(h : ∀ (x : ↥unit_interval × X), ⇑F x = ⇑G x) :
F = G
def
continuous_map.homotopy_with.simps.apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P) :
↥unit_interval × X → Y
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
@[protected, continuity]
theorem
continuous_map.homotopy_with.continuous
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P) :
@[simp]
theorem
continuous_map.homotopy_with.apply_zero
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P)
(x : X) :
@[simp]
theorem
continuous_map.homotopy_with.apply_one
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P)
(x : X) :
@[simp]
theorem
continuous_map.homotopy_with.coe_to_continuous_map
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P) :
⇑(F.to_homotopy.to_continuous_map) = ⇑F
@[simp]
theorem
continuous_map.homotopy_with.coe_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P) :
⇑(F.to_homotopy) = ⇑F
theorem
continuous_map.homotopy_with.prop
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P)
(t : ↥unit_interval) :
P (⇑(F.to_homotopy.curry) t)
theorem
continuous_map.homotopy_with.extend_prop
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop}
(F : f₀.homotopy_with f₁ P)
(t : ℝ) :
P (⇑(F.to_homotopy.extend) t)
def
continuous_map.homotopy_with.refl
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
(f : C(X, Y))
(hf : P f) :
f.homotopy_with f P
Given a continuous function f, and a proof h : P f, we can define a homotopy_with f f P by
F (t, x) = f x
Equations
- continuous_map.homotopy_with.refl f hf = {to_homotopy := {to_continuous_map := (continuous_map.homotopy.refl f).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
@[simp]
theorem
continuous_map.homotopy_with.refl_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
(f : C(X, Y))
(hf : P f)
(x : ↥unit_interval × X) :
⇑(continuous_map.homotopy_with.refl f hf) x = ⇑f x.snd
@[simp]
theorem
continuous_map.homotopy_with.refl_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
(f : C(X, Y))
(hf : P f) :
@[protected, instance]
def
continuous_map.homotopy_with.inhabited
{X : Type u}
[topological_space X] :
inhabited ((continuous_map.id X).homotopy_with (continuous_map.id X) (λ (f : C(X, X)), true))
@[simp]
theorem
continuous_map.homotopy_with.symm_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(x : ↥unit_interval × X) :
def
continuous_map.homotopy_with.symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P) :
f₁.homotopy_with f₀ P
Given a homotopy_with f₀ f₁ P, we can define a homotopy_with f₁ f₀ P by reversing the homotopy.
Equations
- F.symm = {to_homotopy := {to_continuous_map := F.to_homotopy.symm.to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
@[simp]
theorem
continuous_map.homotopy_with.symm_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P) :
F.symm.to_homotopy = F.to_homotopy.symm
@[simp]
theorem
continuous_map.homotopy_with.symm_symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P) :
noncomputable
def
continuous_map.homotopy_with.trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ f₂ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(G : f₁.homotopy_with f₂ P) :
f₀.homotopy_with f₂ P
Given homotopy_with f₀ f₁ P and homotopy_with f₁ f₂ P, we can define a homotopy_with f₀ f₂ P
by putting the first homotopy on [0, 1/2] and the second on [1/2, 1].
Equations
- F.trans G = {to_homotopy := {to_continuous_map := (F.to_homotopy.trans G.to_homotopy).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
theorem
continuous_map.homotopy_with.trans_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ f₂ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(G : f₁.homotopy_with f₂ P)
(x : ↥unit_interval × X) :
theorem
continuous_map.homotopy_with.symm_trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ f₂ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(G : f₁.homotopy_with f₂ P) :
def
continuous_map.homotopy_with.cast
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁) :
g₀.homotopy_with g₁ P
Casting a homotopy_with f₀ f₁ P to a homotopy_with g₀ g₁ P where f₀ = g₀ and f₁ = g₁.
Equations
- F.cast h₀ h₁ = {to_homotopy := {to_continuous_map := (F.to_homotopy.cast h₀ h₁).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
@[simp]
theorem
continuous_map.homotopy_with.cast_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁) :
(F.cast h₀ h₁).to_homotopy = F.to_homotopy.cast h₀ h₁
@[simp]
theorem
continuous_map.homotopy_with.cast_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy_with f₁ P)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁)
(ᾰ : ↥unit_interval × X) :
def
continuous_map.homotopic_with
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f₀ f₁ : C(X, Y))
(P : C(X, Y) → Prop) :
Prop
Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic with respect to the
predicate P if there exists a homotopy_with f₀ f₁ P.
Equations
- f₀.homotopic_with f₁ P = nonempty (f₀.homotopy_with f₁ P)
@[refl]
theorem
continuous_map.homotopic_with.refl
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
(f : C(X, Y))
(hf : P f) :
f.homotopic_with f P
@[symm]
theorem
continuous_map.homotopic_with.symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
⦃f g : C(X, Y)⦄
(h : f.homotopic_with g P) :
g.homotopic_with f P
@[trans]
theorem
continuous_map.homotopic_with.trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{P : C(X, Y) → Prop}
⦃f g h : C(X, Y)⦄
(h₀ : f.homotopic_with g P)
(h₁ : g.homotopic_with h P) :
f.homotopic_with h P
@[reducible]
def
continuous_map.homotopy_rel
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f₀ f₁ : C(X, Y))
(S : set X) :
Type (max u v)
A homotopy_rel f₀ f₁ S is a homotopy between f₀ and f₁ which is fixed on the points in S.
theorem
continuous_map.homotopy_rel.eq_fst
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
(t : ↥unit_interval)
{x : X}
(hx : x ∈ S) :
theorem
continuous_map.homotopy_rel.eq_snd
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
(t : ↥unit_interval)
{x : X}
(hx : x ∈ S) :
theorem
continuous_map.homotopy_rel.fst_eq_snd
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
{x : X}
(hx : x ∈ S) :
@[simp]
theorem
continuous_map.homotopy_rel.refl_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f : C(X, Y))
(S : set X) :
@[simp]
theorem
continuous_map.homotopy_rel.refl_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f : C(X, Y))
(S : set X)
(x : ↥unit_interval × X) :
⇑(continuous_map.homotopy_rel.refl f S) x = ⇑f x.snd
def
continuous_map.homotopy_rel.refl
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f : C(X, Y))
(S : set X) :
f.homotopy_rel f S
Given a map f : C(X, Y) and a set S, we can define a homotopy_rel f f S by setting
F (t, x) = f x for all t. This is defined using homotopy_with.refl, but with the proof
filled in.
Equations
@[simp]
theorem
continuous_map.homotopy_rel.symm_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
(x : ↥unit_interval × X) :
def
continuous_map.homotopy_rel.symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S) :
f₁.homotopy_rel f₀ S
Given a homotopy_rel f₀ f₁ S, we can define a homotopy_rel f₁ f₀ S by reversing the homotopy.
Equations
- F.symm = {to_homotopy := (continuous_map.homotopy_with.symm F).to_homotopy, prop' := _}
@[simp]
theorem
continuous_map.homotopy_rel.symm_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S) :
@[simp]
theorem
continuous_map.homotopy_rel.symm_symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S) :
noncomputable
def
continuous_map.homotopy_rel.trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ f₂ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
(G : f₁.homotopy_rel f₂ S) :
f₀.homotopy_rel f₂ S
Given homotopy_rel f₀ f₁ S and homotopy_rel f₁ f₂ S, we can define a homotopy_rel f₀ f₂ S
by putting the first homotopy on [0, 1/2] and the second on [1/2, 1].
Equations
- F.trans G = {to_homotopy := {to_continuous_map := (F.to_homotopy.trans G.to_homotopy).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
theorem
continuous_map.homotopy_rel.trans_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ f₂ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
(G : f₁.homotopy_rel f₂ S)
(x : ↥unit_interval × X) :
theorem
continuous_map.homotopy_rel.symm_trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{f₀ f₁ f₂ : C(X, Y)}
{S : set X}
(F : f₀.homotopy_rel f₁ S)
(G : f₁.homotopy_rel f₂ S) :
def
continuous_map.homotopy_rel.cast
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X}
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy_rel f₁ S)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁) :
g₀.homotopy_rel g₁ S
Casting a homotopy_rel f₀ f₁ S to a homotopy_rel g₀ g₁ S where f₀ = g₀ and f₁ = g₁.
Equations
- F.cast h₀ h₁ = {to_homotopy := {to_continuous_map := (F.to_homotopy.cast h₀ h₁).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
@[simp]
theorem
continuous_map.homotopy_rel.cast_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X}
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy_rel f₁ S)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁)
(ᾰ : ↥unit_interval × X) :
@[simp]
theorem
continuous_map.homotopy_rel.cast_to_homotopy
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X}
{f₀ f₁ g₀ g₁ : C(X, Y)}
(F : f₀.homotopy_rel f₁ S)
(h₀ : f₀ = g₀)
(h₁ : f₁ = g₁) :
(F.cast h₀ h₁).to_homotopy = F.to_homotopy.cast h₀ h₁
def
continuous_map.homotopic_rel
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
(f₀ f₁ : C(X, Y))
(S : set X) :
Prop
Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic relative to a set S if
there exists a homotopy_rel f₀ f₁ S.
Equations
- f₀.homotopic_rel f₁ S = nonempty (f₀.homotopy_rel f₁ S)
@[refl]
theorem
continuous_map.homotopic_rel.refl
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X}
(f : C(X, Y)) :
f.homotopic_rel f S
@[symm]
theorem
continuous_map.homotopic_rel.symm
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X}
⦃f g : C(X, Y)⦄
(h : f.homotopic_rel g S) :
g.homotopic_rel f S
@[trans]
theorem
continuous_map.homotopic_rel.trans
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X}
⦃f g h : C(X, Y)⦄
(h₀ : f.homotopic_rel g S)
(h₁ : g.homotopic_rel h S) :
f.homotopic_rel h S
theorem
continuous_map.homotopic_rel.equivalence
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{S : set X} :
equivalence (λ (f g : C(X, Y)), f.homotopic_rel g S)