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₀ f₁ : C(X, Y)) extends C(↑unitInterval × X, Y) : 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₀ f₁ : outParam C(X, Y)) [FunLike F (↑unitInterval × X) Y] extends ContinuousMapClass F (↑unitInterval × X) Y : 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₀ f₁ : C(X, Y)} : FunLike (f₀.Homotopy f₁) (↑unitInterval × X) Y

Equations

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

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

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

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

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

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

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

Equations

• F.curry = F.curry

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• F.extend = ContinuousMap.IccExtend ContinuousMap.Homotopy.extend._proof_2 F.curry

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

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

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

@[simp]

theorem ContinuousMap.Homotopy.extend_of_mem_I {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {t : ℝ} (ht : t ∈ unitInterval) : F.extend t = F.curry ⟨t, ht⟩

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

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

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

theorem ContinuousMap.Homotopy.congr_fun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {F G : f₀.Homotopy 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₀ f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {x y : ↑unitInterval × X} (h : x = y) : F x = F y

def ContinuousMap.Homotopy.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace 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

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

@[simp]

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

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

Equations

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

def ContinuousMap.Homotopy.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace 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 = { toFun := fun (x : ↑unitInterval × X) => F (unitInterval.symm x.1, x.2), continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }

@[simp]

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

@[simp]

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

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

def ContinuousMap.Homotopy.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace 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].

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₀ f₁ f₂ : C(X, Y)} (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) (x : ↑unitInterval × X) : (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

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

def ContinuousMap.Homotopy.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace 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₁ = { toFun := ⇑F, continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }

@[simp]

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

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

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

Equations

• G.compContinuousMap f = { toContinuousMap := G.comp ((ContinuousMap.id ↑unitInterval).prodMap f), 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₀ g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (f : C(X, Y)) (a✝ : ↑unitInterval × X) : (G.compContinuousMap f) a✝ = G (Prod.map id (⇑f) a✝)

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

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

@[simp]

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

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

• F.prodMk G = { toContinuousMap := F.prodMk ↑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₀ f₁ : C(X, Y)} {g₀ g₁ : C(Z, Z')} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) : (f₀.prodMap g₀).Homotopy (f₁.prodMap 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

• F.prodMap G = ((ContinuousMap.Homotopy.refl ContinuousMap.fst).hcomp F).prodMk ((ContinuousMap.Homotopy.refl ContinuousMap.snd).hcomp G)

def ContinuousMap.Homotopy.pi {X : Type u} {ι : Type u_2} [TopologicalSpace X] {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (Y i)] {f₀ f₁ : (i : ι) → C(X, Y i)} (F : (i : ι) → (f₀ i).Homotopy (f₁ i)) : (pi f₀).Homotopy (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₀ f₁ : (i : ι) → C(X i, Y i)} (F : (i : ι) → (f₀ i).Homotopy (f₁ i)) : (piMap f₀).Homotopy (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.refl (ContinuousMap.eval i)).hcomp (F i)

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

Equations

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

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

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

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

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

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

theorem ContinuousMap.Homotopic.prodMk {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(X, Z)} : f₀.Homotopic f₁ → g₀.Homotopic g₁ → (f₀.prodMk g₀).Homotopic (f₁.prodMk 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₀ f₁ : C(X, Y)} {g₀ g₁ : C(Z, Z')} : f₀.Homotopic f₁ → g₀.Homotopic g₁ → (f₀.prodMap g₀).Homotopic (f₁.prodMap g₁)

theorem ContinuousMap.Homotopic.pi {X : Type u} {ι : Type u_2} [TopologicalSpace X] {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (Y i)] {f₀ f₁ : (i : ι) → C(X, Y i)} (F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)) : (pi f₀).Homotopic (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₀ f₁ : (i : ι) → C(X i, Y i)} (F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)) : (piMap f₀).Homotopic (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₀ f₁ : C(X, Y)) (P : C(X, Y) → Prop) extends f₀.Homotopy f₁ : 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₀ f₁ : C(X, Y)} {P : C(X, Y) → Prop} : FunLike (f₀.HomotopyWith f₁ P) (↑unitInterval × X) Y

Equations

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

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

theorem ContinuousMap.HomotopyWith.coeFn_injective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ 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₀ f₁ : C(X, Y)} {P : C(X, Y) → Prop} {F G : f₀.HomotopyWith f₁ P} (h : ∀ (x : ↑unitInterval × X), F x = G x) : F = G

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

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

@[simp]

theorem ContinuousMap.HomotopyWith.apply_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : f₀.HomotopyWith 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₀ f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : f₀.HomotopyWith 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₀ f₁ : C(X, Y)} {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P) : ⇑F.toContinuousMap = ⇑F

@[simp]

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

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

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

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) : f.HomotopyWith 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' := ⋯ }

@[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) : (refl f hf) x = f x.2

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

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

Equations

• f₀.HomotopicWith f₁ P = Nonempty (f₀.HomotopyWith 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) : f.HomotopicWith f P

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

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

@[reducible, inline]

abbrev ContinuousMap.HomotopyRel {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ 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

• f₀.HomotopyRel f₁ S = f₀.HomotopyWith 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₀ f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel 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₀ f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel 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₀ f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) {x : X} (hx : x ∈ S) : f₀ x = f₁ x

def ContinuousMap.HomotopyRel.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) : f.HomotopyRel 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.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) (x : ↑unitInterval × X) : (refl f S) x = f x.2

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

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

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

Equations

• F.compContinuousMap g = { toHomotopy := F.hcomp (ContinuousMap.Homotopy.refl g), 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₀ f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) (x : ↑unitInterval × X) : (F.compContinuousMap g) x = g (F x)

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

Equations

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

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

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

theorem ContinuousMap.HomotopicRel.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} ⦃f g h : C(X, Y)⦄ (h₀ : f.HomotopicRel g S) (h₁ : g.HomotopicRel h S) : f.HomotopicRel 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)) => f.HomotopicRel g S

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

@[simp]

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