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 between f₀ and f₁.
• ContinuousMap.HomotopyWith f₀ f₁ P is the type of homotopies between f₀ and f₁, where the intermediate maps satisfy the predicate P.
• ContinuousMap.HomotopyRel f₀ f₁ S is the type of homotopies between f₀ and f₁ which are fixed on S.

For each of the above, we have

• refl f, which is the constant homotopy from f to f.
• symm F, which reverses the homotopy F. For example, if F : ContinuousMap.Homotopy f₀ f₁, then F.symm : ContinuousMap.Homotopy f₁ f₀.
• trans F G, which concatenates the homotopies F and G. For example, if F : ContinuousMap.Homotopy f₀ f₁ and G : ContinuousMap.Homotopy f₁ f₂, then F.trans G : ContinuousMap.Homotopy f₀ f₂.

We also define the relations

• ContinuousMap.Homotopic f₀ f₁ is defined to be Nonempty (ContinuousMap.Homotopy f₀ f₁)
• ContinuousMap.HomotopicWith f₀ f₁ P is defined to be Nonempty (ContinuousMap.HomotopyWith f₀ f₁ P)
• ContinuousMap.HomotopicRel f₀ f₁ P is defined to be Nonempty (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

• HOL-Analysis formalisation

structure ContinuousMap.Homotopy {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) extends ContinuousMap : Type (max u v)

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.

• toFun : ↑unitInterval × X → Y
• continuous_toFun : Continuous self.toFun
• map_zero_left : ∀ (x : X), self.toFun (0, x) = f₀ x

  value of the homotopy at 0

• map_one_left : ∀ (x : X), self.toFun (1, x) = f₁ x

  value of the homotopy at 1

class ContinuousMap.HomotopyLike {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [TopologicalSpace X] [TopologicalSpace Y] (F : Type u_5) (f₀ : outParam C(X, Y)) (f₁ : outParam C(X, Y)) [FunLike F (↑unitInterval × X) Y] extends ContinuousMapClass : Prop

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.

• 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

instance ContinuousMap.Homotopy.instFunLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} : FunLike (ContinuousMap.Homotopy f₀ f₁) (↑unitInterval × X) Y

Equations

• ContinuousMap.Homotopy.instFunLike = { coe := fun (f : ContinuousMap.Homotopy f₀ f₁) => f.toFun, coe_injective' := ⋯ }

instance ContinuousMap.Homotopy.instHomotopyLikeHomotopyInstFunLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} : ContinuousMap.HomotopyLike (ContinuousMap.Homotopy f₀ f₁) f₀ f₁

Equations

• ⋯ = ⋯

theorem ContinuousMap.Homotopy.ext {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : ContinuousMap.Homotopy f₀ f₁} {G : ContinuousMap.Homotopy f₀ f₁} (h : ∀ (x : ↑unitInterval × X), F x = G x) : F = G

def ContinuousMap.Homotopy.Simps.apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : ↑unitInterval × 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

• ContinuousMap.Homotopy.Simps.apply F = ⇑F

theorem ContinuousMap.Homotopy.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : Continuous ⇑F

Deprecated. Use map_continuous instead.

@[simp]

theorem ContinuousMap.Homotopy.apply_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (x : X) : F (0, x) = f₀ x

@[simp]

theorem ContinuousMap.Homotopy.apply_one {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (x : X) : F (1, x) = f₁ x

@[simp]

theorem ContinuousMap.Homotopy.coe_toContinuousMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : ⇑F.toContinuousMap = ⇑F

def ContinuousMap.Homotopy.curry {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : C(↑unitInterval, C(X, Y))

Currying a homotopy to a continuous function from I to C(X, Y).

Equations

• ContinuousMap.Homotopy.curry F = ContinuousMap.curry F.toContinuousMap

@[simp]

theorem ContinuousMap.Homotopy.curry_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (t : ↑unitInterval) (x : X) : ((ContinuousMap.Homotopy.curry F) t) x = F (t, x)

def ContinuousMap.Homotopy.extend {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : C(ℝ, C(X, Y))

Continuously extending a curried homotopy to a function from ℝ to C(X, Y).

Equations

• ContinuousMap.Homotopy.extend F = ContinuousMap.IccExtend ContinuousMap.Homotopy.extend.proof_1 (ContinuousMap.Homotopy.curry F)

theorem ContinuousMap.Homotopy.extend_apply_of_le_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) {t : ℝ} (ht : t ≤ 0) (x : X) : ((ContinuousMap.Homotopy.extend F) t) x = f₀ x

theorem ContinuousMap.Homotopy.extend_apply_of_one_le {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) {t : ℝ} (ht : 1 ≤ t) (x : X) : ((ContinuousMap.Homotopy.extend F) t) x = f₁ x

@[simp]

theorem ContinuousMap.Homotopy.extend_apply_coe {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (t : ↑unitInterval) (x : X) : ((ContinuousMap.Homotopy.extend F) ↑t) x = F (t, x)

@[simp]

theorem ContinuousMap.Homotopy.extend_apply_of_mem_I {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) {t : ℝ} (ht : t ∈ unitInterval) (x : X) : ((ContinuousMap.Homotopy.extend F) t) x = F ({ val := t, property := ht }, x)

theorem ContinuousMap.Homotopy.congr_fun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : ContinuousMap.Homotopy f₀ f₁} {G : ContinuousMap.Homotopy f₀ f₁} (h : F = G) (x : ↑unitInterval × X) : F x = G x

theorem ContinuousMap.Homotopy.congr_arg {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) {x : ↑unitInterval × X} {y : ↑unitInterval × X} (h : x = y) : F x = F y

@[simp]

theorem ContinuousMap.Homotopy.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : ↑unitInterval × X) : (ContinuousMap.Homotopy.refl f) x = f x.2

def ContinuousMap.Homotopy.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : ContinuousMap.Homotopy f f

Given a continuous function f, we can define a Homotopy f f by F (t, x) = f x

Equations

• ContinuousMap.Homotopy.refl f = { toContinuousMap := { toFun := fun (x : ↑unitInterval × X) => f x.2, continuous_toFun := ⋯ }, map_zero_left := ⋯, map_one_left := ⋯ }

instance ContinuousMap.Homotopy.instInhabitedHomotopyId {X : Type u} [TopologicalSpace X] : Inhabited (ContinuousMap.Homotopy (ContinuousMap.id X) (ContinuousMap.id X))

Equations

• ContinuousMap.Homotopy.instInhabitedHomotopyId = { default := ContinuousMap.Homotopy.refl (ContinuousMap.id X) }

@[simp]

theorem ContinuousMap.Homotopy.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (x : ↑unitInterval × X) : (ContinuousMap.Homotopy.symm F) x = F (unitInterval.symm x.1, x.2)

def ContinuousMap.Homotopy.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : ContinuousMap.Homotopy f₁ f₀

Given a Homotopy f₀ f₁, we can define a Homotopy f₁ f₀ by reversing the homotopy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousMap.Homotopy.symm_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : ContinuousMap.Homotopy.symm (ContinuousMap.Homotopy.symm F) = F

theorem ContinuousMap.Homotopy.symm_bijective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} : Function.Bijective ContinuousMap.Homotopy.symm

def ContinuousMap.Homotopy.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy f₁ f₂) : ContinuousMap.Homotopy f₀ 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].

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousMap.Homotopy.trans_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy f₁ f₂) (x : ↑unitInterval × X) : (ContinuousMap.Homotopy.trans F G) x = if h : ↑x.1 ≤ 1 / 2 then F ({ val := 2 * ↑x.1, property := ⋯ }, x.2) else G ({ val := 2 * ↑x.1 - 1, property := ⋯ }, x.2)

theorem ContinuousMap.Homotopy.symm_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy f₁ f₂) : ContinuousMap.Homotopy.symm (ContinuousMap.Homotopy.trans F G) = ContinuousMap.Homotopy.trans (ContinuousMap.Homotopy.symm G) (ContinuousMap.Homotopy.symm F)

@[simp]

theorem ContinuousMap.Homotopy.cast_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (ContinuousMap.Homotopy.cast F h₀ h₁) a = F a

def ContinuousMap.Homotopy.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : ContinuousMap.Homotopy g₀ g₁

Casting a Homotopy f₀ f₁ to a Homotopy g₀ g₁ where f₀ = g₀ and f₁ = g₁.

Equations

• ContinuousMap.Homotopy.cast F h₀ h₁ = { toContinuousMap := { toFun := ⇑F, continuous_toFun := ⋯ }, map_zero_left := ⋯, map_one_left := ⋯ }

@[simp]

theorem ContinuousMap.Homotopy.compContinuousMap_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (G : ContinuousMap.Homotopy g₀ g₁) (f : C(X, Y)) : ∀ (a : ↑unitInterval × X), (ContinuousMap.Homotopy.compContinuousMap G f) a = G (a.1, f a.2)

def ContinuousMap.Homotopy.compContinuousMap {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (G : ContinuousMap.Homotopy g₀ g₁) (f : C(X, Y)) : ContinuousMap.Homotopy (ContinuousMap.comp g₀ f) (ContinuousMap.comp g₁ f)

Composition of a Homotopy g₀ g₁ and f : C(X, Y) as a homotopy between g₀.comp f and g₁.comp f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousMap.Homotopy.hcomp_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) (x : ↑unitInterval × X) : (ContinuousMap.Homotopy.hcomp F G) x = G (x.1, F x)

def ContinuousMap.Homotopy.hcomp {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) : ContinuousMap.Homotopy (ContinuousMap.comp g₀ f₀) (ContinuousMap.comp g₁ f₁)

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

• ContinuousMap.Homotopy.hcomp F G = { toContinuousMap := { toFun := fun (x : ↑unitInterval × X) => G (x.1, F x), continuous_toFun := ⋯ }, map_zero_left := ⋯, map_one_left := ⋯ }

def ContinuousMap.Homotopy.prodMk {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Z)} {g₁ : C(X, Z)} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) : ContinuousMap.Homotopy (ContinuousMap.prodMk f₀ g₀) (ContinuousMap.prodMk f₁ g₁)

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).

Equations

• ContinuousMap.Homotopy.prodMk F G = { toContinuousMap := ContinuousMap.prodMk F.toContinuousMap ↑G, map_zero_left := ⋯, map_one_left := ⋯ }

def ContinuousMap.Homotopy.prodMap {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Z, Z')} {g₁ : C(Z, Z')} (F : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) : ContinuousMap.Homotopy (ContinuousMap.prodMap f₀ g₀) (ContinuousMap.prodMap f₁ g₁)

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)).

Equations

• One or more equations did not get rendered due to their size.

def ContinuousMap.Homotopy.pi {X : Type u} {ι : Type u_2} [TopologicalSpace X] {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X, Y i)} {f₁ : (i : ι) → C(X, Y i)} (F : (i : ι) → ContinuousMap.Homotopy (f₀ i) (f₁ i)) : ContinuousMap.Homotopy (ContinuousMap.pi f₀) (ContinuousMap.pi f₁)

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₁.

Equations

• ContinuousMap.Homotopy.pi F = { toContinuousMap := ContinuousMap.pi fun (i : ι) => ↑(F i), map_zero_left := ⋯, map_one_left := ⋯ }

def ContinuousMap.Homotopy.piMap {ι : Type u_2} {X : ι → Type u_3} {Y : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X i, Y i)} {f₁ : (i : ι) → C(X i, Y i)} (F : (i : ι) → ContinuousMap.Homotopy (f₀ i) (f₁ i)) : ContinuousMap.Homotopy (ContinuousMap.piMap f₀) (ContinuousMap.piMap f₁)

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₁.

Equations

• ContinuousMap.Homotopy.piMap F = ContinuousMap.Homotopy.pi fun (i : ι) => ContinuousMap.Homotopy.hcomp (ContinuousMap.Homotopy.refl (ContinuousMap.eval i)) (F i)

def ContinuousMap.Homotopic {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (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₁.

Equations

• ContinuousMap.Homotopic f₀ f₁ = Nonempty (ContinuousMap.Homotopy f₀ f₁)

theorem ContinuousMap.Homotopic.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : ContinuousMap.Homotopic f f

theorem ContinuousMap.Homotopic.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ (h : ContinuousMap.Homotopic f g) : ContinuousMap.Homotopic g f

theorem ContinuousMap.Homotopic.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ ⦃h : C(X, Y)⦄ (h₀ : ContinuousMap.Homotopic f g) (h₁ : ContinuousMap.Homotopic g h) : ContinuousMap.Homotopic f h

theorem ContinuousMap.Homotopic.hcomp {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (h₀ : ContinuousMap.Homotopic f₀ f₁) (h₁ : ContinuousMap.Homotopic g₀ g₁) : ContinuousMap.Homotopic (ContinuousMap.comp g₀ f₀) (ContinuousMap.comp g₁ f₁)

theorem ContinuousMap.Homotopic.equivalence {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Equivalence ContinuousMap.Homotopic

theorem ContinuousMap.Homotopic.prodMk {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Z)} {g₁ : C(X, Z)} : ContinuousMap.Homotopic f₀ f₁ → ContinuousMap.Homotopic g₀ g₁ → ContinuousMap.Homotopic (ContinuousMap.prodMk f₀ g₀) (ContinuousMap.prodMk f₁ g₁)

theorem ContinuousMap.Homotopic.prodMap {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Z, Z')} {g₁ : C(Z, Z')} : ContinuousMap.Homotopic f₀ f₁ → ContinuousMap.Homotopic g₀ g₁ → ContinuousMap.Homotopic (ContinuousMap.prodMap f₀ g₀) (ContinuousMap.prodMap f₁ g₁)

theorem ContinuousMap.Homotopic.pi {X : Type u} {ι : Type u_2} [TopologicalSpace X] {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X, Y i)} {f₁ : (i : ι) → C(X, Y i)} (F : ∀ (i : ι), ContinuousMap.Homotopic (f₀ i) (f₁ i)) : ContinuousMap.Homotopic (ContinuousMap.pi f₀) (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₁.

theorem ContinuousMap.Homotopic.piMap {ι : Type u_2} {X : ι → Type u_3} {Y : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X i, Y i)} {f₁ : (i : ι) → C(X i, Y i)} (F : ∀ (i : ι), ContinuousMap.Homotopic (f₀ i) (f₁ i)) : ContinuousMap.Homotopic (ContinuousMap.piMap f₀) (ContinuousMap.piMap 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₁.

structure ContinuousMap.HomotopyWith {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (P : C(X, Y) → Prop) extends ContinuousMap.Homotopy : Type (max u v)

The type of homotopies between f₀ f₁ : C(X, Y), where the intermediate maps satisfy the predicate P : C(X, Y) → Prop

• toFun : ↑unitInterval × X → Y
• continuous_toFun : Continuous self.toFun
• map_zero_left : ∀ (x : X), self.toFun (0, x) = f₀ x
• map_one_left : ∀ (x : X), self.toFun (1, x) = f₁ x
• prop' : ∀ (t : ↑unitInterval), P { toFun := fun (x : X) => self.toFun (t, x), continuous_toFun := ⋯ }

  the intermediate maps of the homotopy satisfy the property

instance ContinuousMap.HomotopyWith.instFunLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} : FunLike (ContinuousMap.HomotopyWith f₀ f₁ P) (↑unitInterval × X) Y

Equations

• ContinuousMap.HomotopyWith.instFunLike = { coe := fun (F : ContinuousMap.HomotopyWith f₀ f₁ P) => ⇑F.toHomotopy, coe_injective' := ⋯ }

instance ContinuousMap.HomotopyWith.instHomotopyLikeHomotopyWithInstFunLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} : ContinuousMap.HomotopyLike (ContinuousMap.HomotopyWith f₀ f₁ P) f₀ f₁

Equations

• ⋯ = ⋯

theorem ContinuousMap.HomotopyWith.coeFn_injective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} : Function.Injective DFunLike.coe

theorem ContinuousMap.HomotopyWith.ext {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} {F : ContinuousMap.HomotopyWith f₀ f₁ P} {G : ContinuousMap.HomotopyWith f₀ f₁ P} (h : ∀ (x : ↑unitInterval × X), F x = G x) : F = G

def ContinuousMap.HomotopyWith.Simps.apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) : ↑unitInterval × 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

• ContinuousMap.HomotopyWith.Simps.apply F = ⇑F

theorem ContinuousMap.HomotopyWith.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) : Continuous ⇑F

@[simp]

theorem ContinuousMap.HomotopyWith.apply_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (x : X) : F (0, x) = f₀ x

@[simp]

theorem ContinuousMap.HomotopyWith.apply_one {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (x : X) : F (1, x) = f₁ x

theorem ContinuousMap.HomotopyWith.coe_toContinuousMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) : ⇑F.toContinuousMap = ⇑F

@[simp]

theorem ContinuousMap.HomotopyWith.coe_toHomotopy {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) : ⇑F.toHomotopy = ⇑F

theorem ContinuousMap.HomotopyWith.prop {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (t : ↑unitInterval) : P ((ContinuousMap.Homotopy.curry F.toHomotopy) t)

theorem ContinuousMap.HomotopyWith.extendProp {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (t : ℝ) : P ((ContinuousMap.Homotopy.extend F.toHomotopy) t)

@[simp]

theorem ContinuousMap.HomotopyWith.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} (f : C(X, Y)) (hf : P f) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.refl f hf) x = f x.2

@[simp]

theorem ContinuousMap.HomotopyWith.refl_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} (f : C(X, Y)) (hf : P f) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.refl f hf) x = f x.2

def ContinuousMap.HomotopyWith.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} (f : C(X, Y)) (hf : P f) : ContinuousMap.HomotopyWith f f P

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

Equations

• ContinuousMap.HomotopyWith.refl f hf = { toHomotopy := ContinuousMap.Homotopy.refl f, prop' := ⋯ }

instance ContinuousMap.HomotopyWith.instInhabitedHomotopyWithIdContinuousMapTrue {X : Type u} [TopologicalSpace X] : Inhabited (ContinuousMap.HomotopyWith (ContinuousMap.id X) (ContinuousMap.id X) fun (x : C(X, X)) => True)

Equations

• ContinuousMap.HomotopyWith.instInhabitedHomotopyWithIdContinuousMapTrue = { default := ContinuousMap.HomotopyWith.refl (ContinuousMap.id X) trivial }

@[simp]

theorem ContinuousMap.HomotopyWith.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.symm F) x = F (unitInterval.symm x.1, x.2)

@[simp]

theorem ContinuousMap.HomotopyWith.symm_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.symm F) x = F (unitInterval.symm x.1, x.2)

def ContinuousMap.HomotopyWith.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) : ContinuousMap.HomotopyWith f₁ f₀ P

Given a HomotopyWith f₀ f₁ P, we can define a HomotopyWith f₁ f₀ P by reversing the homotopy.

Equations

• ContinuousMap.HomotopyWith.symm F = { toHomotopy := ContinuousMap.Homotopy.symm F.toHomotopy, prop' := ⋯ }

@[simp]

theorem ContinuousMap.HomotopyWith.symm_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) : ContinuousMap.HomotopyWith.symm (ContinuousMap.HomotopyWith.symm F) = F

theorem ContinuousMap.HomotopyWith.symm_bijective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} : Function.Bijective ContinuousMap.HomotopyWith.symm

def ContinuousMap.HomotopyWith.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (G : ContinuousMap.HomotopyWith f₁ f₂ P) : ContinuousMap.HomotopyWith f₀ f₂ P

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].

Equations

• ContinuousMap.HomotopyWith.trans F G = let __src := ContinuousMap.Homotopy.trans F.toHomotopy G.toHomotopy; { toHomotopy := __src, prop' := ⋯ }

theorem ContinuousMap.HomotopyWith.trans_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (G : ContinuousMap.HomotopyWith f₁ f₂ P) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.trans F G) x = if h : ↑x.1 ≤ 1 / 2 then F ({ val := 2 * ↑x.1, property := ⋯ }, x.2) else G ({ val := 2 * ↑x.1 - 1, property := ⋯ }, x.2)

theorem ContinuousMap.HomotopyWith.symm_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (G : ContinuousMap.HomotopyWith f₁ f₂ P) : ContinuousMap.HomotopyWith.symm (ContinuousMap.HomotopyWith.trans F G) = ContinuousMap.HomotopyWith.trans (ContinuousMap.HomotopyWith.symm G) (ContinuousMap.HomotopyWith.symm F)

@[simp]

theorem ContinuousMap.HomotopyWith.cast_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.cast F h₀ h₁) a = F a

@[simp]

theorem ContinuousMap.HomotopyWith.cast_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (ContinuousMap.HomotopyWith.cast F h₀ h₁) a = F a

def ContinuousMap.HomotopyWith.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.HomotopyWith f₀ f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : ContinuousMap.HomotopyWith g₀ g₁ P

Casting a HomotopyWith f₀ f₁ P to a HomotopyWith g₀ g₁ P where f₀ = g₀ and f₁ = g₁.

Equations

• ContinuousMap.HomotopyWith.cast F h₀ h₁ = { toHomotopy := ContinuousMap.Homotopy.cast F.toHomotopy h₀ h₁, prop' := ⋯ }

def ContinuousMap.HomotopicWith {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (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 HomotopyWith f₀ f₁ P.

Equations

• ContinuousMap.HomotopicWith f₀ f₁ P = Nonempty (ContinuousMap.HomotopyWith f₀ f₁ P)

theorem ContinuousMap.HomotopicWith.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} (f : C(X, Y)) (hf : P f) : ContinuousMap.HomotopicWith f f P

theorem ContinuousMap.HomotopicWith.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ (h : ContinuousMap.HomotopicWith f g P) : ContinuousMap.HomotopicWith g f P

theorem ContinuousMap.HomotopicWith.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ ⦃h : C(X, Y)⦄ (h₀ : ContinuousMap.HomotopicWith f g P) (h₁ : ContinuousMap.HomotopicWith g h P) : ContinuousMap.HomotopicWith f h P

@[inline, reducible]

abbrev ContinuousMap.HomotopyRel {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (S : Set X) : Type (max u v)

A HomotopyRel f₀ f₁ S is a homotopy between f₀ and f₁ which is fixed on the points in S.

Equations

• ContinuousMap.HomotopyRel f₀ f₁ S = ContinuousMap.HomotopyWith f₀ f₁ fun (f : C(X, Y)) => ∀ x ∈ S, f x = f₀ x

theorem ContinuousMap.HomotopyRel.eq_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (t : ↑unitInterval) {x : X} (hx : x ∈ S) : F (t, x) = f₀ x

theorem ContinuousMap.HomotopyRel.eq_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (t : ↑unitInterval) {x : X} (hx : x ∈ S) : F (t, x) = f₁ x

theorem ContinuousMap.HomotopyRel.fst_eq_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) {x : X} (hx : x ∈ S) : f₀ x = f₁ x

@[simp]

theorem ContinuousMap.HomotopyRel.refl_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.refl f S) x = f x.2

@[simp]

theorem ContinuousMap.HomotopyRel.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.refl f S) x = f x.2

def ContinuousMap.HomotopyRel.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) : ContinuousMap.HomotopyRel f f S

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.

Equations

• ContinuousMap.HomotopyRel.refl f S = ContinuousMap.HomotopyWith.refl f ⋯

@[simp]

theorem ContinuousMap.HomotopyRel.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.symm F) x = F (unitInterval.symm x.1, x.2)

@[simp]

theorem ContinuousMap.HomotopyRel.symm_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.symm F) x = F (unitInterval.symm x.1, x.2)

def ContinuousMap.HomotopyRel.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) : ContinuousMap.HomotopyRel f₁ f₀ S

Given a HomotopyRel f₀ f₁ S, we can define a HomotopyRel f₁ f₀ S by reversing the homotopy.

Equations

• ContinuousMap.HomotopyRel.symm F = { toHomotopy := ContinuousMap.Homotopy.symm F.toHomotopy, prop' := ⋯ }

@[simp]

theorem ContinuousMap.HomotopyRel.symm_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) : ContinuousMap.HomotopyRel.symm (ContinuousMap.HomotopyRel.symm F) = F

theorem ContinuousMap.HomotopyRel.symm_bijective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} : Function.Bijective ContinuousMap.HomotopyRel.symm

def ContinuousMap.HomotopyRel.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (G : ContinuousMap.HomotopyRel f₁ f₂ S) : ContinuousMap.HomotopyRel f₀ f₂ S

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].

Equations

• ContinuousMap.HomotopyRel.trans F G = { toHomotopy := ContinuousMap.Homotopy.trans F.toHomotopy G.toHomotopy, prop' := ⋯ }

theorem ContinuousMap.HomotopyRel.trans_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (G : ContinuousMap.HomotopyRel f₁ f₂ S) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.trans F G) x = if h : ↑x.1 ≤ 1 / 2 then F ({ val := 2 * ↑x.1, property := ⋯ }, x.2) else G ({ val := 2 * ↑x.1 - 1, property := ⋯ }, x.2)

theorem ContinuousMap.HomotopyRel.symm_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} {S : Set X} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (G : ContinuousMap.HomotopyRel f₁ f₂ S) : ContinuousMap.HomotopyRel.symm (ContinuousMap.HomotopyRel.trans F G) = ContinuousMap.HomotopyRel.trans (ContinuousMap.HomotopyRel.symm G) (ContinuousMap.HomotopyRel.symm F)

@[simp]

theorem ContinuousMap.HomotopyRel.cast_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.cast F h₀ h₁) a = F a

@[simp]

theorem ContinuousMap.HomotopyRel.cast_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.cast F h₀ h₁) a = F a

def ContinuousMap.HomotopyRel.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : ContinuousMap.HomotopyRel g₀ g₁ S

Casting a HomotopyRel f₀ f₁ S to a HomotopyRel g₀ g₁ S where f₀ = g₀ and f₁ = g₁.

Equations

• ContinuousMap.HomotopyRel.cast F h₀ h₁ = { toHomotopy := ContinuousMap.Homotopy.cast F.toHomotopy h₀ h₁, prop' := ⋯ }

@[simp]

theorem ContinuousMap.HomotopyRel.compContinuousMap_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (g : C(Y, Z)) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.compContinuousMap F g) x = g (F x)

@[simp]

theorem ContinuousMap.HomotopyRel.compContinuousMap_toFun {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (g : C(Y, Z)) (x : ↑unitInterval × X) : (ContinuousMap.HomotopyRel.compContinuousMap F g) x = g (F x)

def ContinuousMap.HomotopyRel.compContinuousMap {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.HomotopyRel f₀ f₁ S) (g : C(Y, Z)) : ContinuousMap.HomotopyRel (ContinuousMap.comp g f₀) (ContinuousMap.comp g f₁) S

Post-compose a homotopy relative to a set by a continuous function.

Equations

• ContinuousMap.HomotopyRel.compContinuousMap F g = { toHomotopy := ContinuousMap.Homotopy.hcomp F.toHomotopy (ContinuousMap.Homotopy.refl g), prop' := ⋯ }

def ContinuousMap.HomotopicRel {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (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 HomotopyRel f₀ f₁ S.

Equations

• ContinuousMap.HomotopicRel f₀ f₁ S = Nonempty (ContinuousMap.HomotopyRel f₀ f₁ S)

theorem ContinuousMap.HomotopicRel.homotopic {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (h : ContinuousMap.HomotopicRel f₀ f₁ S) : ContinuousMap.Homotopic f₀ f₁

If two maps are homotopic relative to a set, then they are homotopic.

theorem ContinuousMap.HomotopicRel.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} (f : C(X, Y)) : ContinuousMap.HomotopicRel f f S

theorem ContinuousMap.HomotopicRel.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ (h : ContinuousMap.HomotopicRel f g S) : ContinuousMap.HomotopicRel g f S

theorem ContinuousMap.HomotopicRel.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ ⦃h : C(X, Y)⦄ (h₀ : ContinuousMap.HomotopicRel f g S) (h₁ : ContinuousMap.HomotopicRel g h S) : ContinuousMap.HomotopicRel f h S

theorem ContinuousMap.HomotopicRel.equivalence {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} : Equivalence fun (f g : C(X, Y)) => ContinuousMap.HomotopicRel f g S

@[simp]

theorem ContinuousMap.homotopicRel_empty {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} : ContinuousMap.HomotopicRel f₀ f₁ ∅ ↔ ContinuousMap.Homotopic f₀ f₁