Shrinking the fixed set of a relative homotopy, and pointed homotopy

A homotopy relative to a set S fixes every point of S at all times, so it is also a homotopy relative to every subset of S. This lets relative homotopies obtained relative to different sets be composed relative to a common subset. Precomposed with a map e, it is a homotopy relative to the preimage e ⁻¹' S.

Homotopy relative to a single point is pointed homotopy: it is an equivalence relation on the pointed maps (Y, y₀) → (X, x), whose classes are the pointed homotopy classes of maps.

Main declarations

• ContinuousMap.HomotopyRel.mono: a homotopy relative to S as a homotopy relative to T ⊆ S.
• ContinuousMap.HomotopicRel.mono: maps homotopic relative to S are homotopic relative to every T ⊆ S.
• ContinuousMap.HomotopyRel.precomp, ContinuousMap.HomotopicRel.precomp: precomposing a homotopy relative to S with e gives a homotopy relative to e ⁻¹' S.
• TauCeti.pointedHomotopySetoid: pointed homotopy, as an equivalence relation on pointed maps.

def ContinuousMap.HomotopyRel.mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S T : Set X} (F : f₀.HomotopyRel f₁ S) (hTS : T ⊆ S) : f₀.HomotopyRel f₁ T

A homotopy relative to S is a homotopy relative to every subset of S.

@[simp]

theorem ContinuousMap.HomotopyRel.mono_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S T : Set X} (F : f₀.HomotopyRel f₁ S) (hTS : T ⊆ S) (x : ↑unitInterval × X) : (F.mono hTS) x = F x

Shrinking the fixed set does not change the homotopy.

theorem ContinuousMap.HomotopicRel.mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S T : Set X} (h : f₀.HomotopicRel f₁ S) (hTS : T ⊆ S) : f₀.HomotopicRel f₁ T

Maps homotopic relative to S are homotopic relative to every subset of S.

def ContinuousMap.HomotopyRel.precomp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X} {W : Type u_3} [TopologicalSpace W] (F : f₀.HomotopyRel f₁ S) (e : C(W, X)) : (f₀.comp e).HomotopyRel (f₁.comp e) (⇑e ⁻¹' S)

Precomposing a homotopy relative to S with e : C(W, X) gives a homotopy relative to the preimage e ⁻¹' S.

@[simp]

theorem ContinuousMap.HomotopyRel.precomp_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X} {W : Type u_3} [TopologicalSpace W] (F : f₀.HomotopyRel f₁ S) (e : C(W, X)) (x : ↑unitInterval × W) : (F.precomp e) x = F (x.1, e x.2)

The precomposed homotopy is the original homotopy evaluated at the image point.

theorem ContinuousMap.HomotopicRel.precomp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X} {W : Type u_3} [TopologicalSpace W] (h : f₀.HomotopicRel f₁ S) (e : C(W, X)) : (f₀.comp e).HomotopicRel (f₁.comp e) (⇑e ⁻¹' S)

If f₀ and f₁ are homotopic relative to S, then f₀ ∘ e and f₁ ∘ e are homotopic relative to e ⁻¹' S.

def TauCeti.pointedHomotopySetoid {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (y₀ : Y) (x : X) : Setoid { f : C(Y, X) // f y₀ = x }

Pointed homotopy, homotopy relative to the base point, as an equivalence relation on the pointed maps (Y, y₀) → (X, x). Its classes are the pointed homotopy classes of maps.

theorem TauCeti.pointedHomotopySetoid_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y₀ : Y} {x : X} {f g : { f : C(Y, X) // f y₀ = x }} : (pointedHomotopySetoid y₀ x) f g ↔ (↑f).HomotopicRel ↑g {y₀}