# Documentation

Mathlib.Topology.Homotopy.Product

# Product of homotopies #

In this file, we introduce definitions for the product of homotopies. We show that the products of relative homotopies are still relative homotopies. Finally, we specialize to the case of path homotopies, and provide the definition for the product of path classes. We show various lemmas associated with these products, such as the fact that path products commute with path composition, and that projection is the inverse of products.

## Definitions #

### General homotopies #

• ContinuousMap.Homotopy.pi homotopies: Let f and g be a family of functions indexed on I, such that for each i ∈ I, fᵢ and gᵢ are maps from A to Xᵢ. Let homotopies be a family of homotopies from fᵢ to gᵢ for each i. Then Homotopy.pi homotopies is the canonical homotopy from ∏ f to ∏ g, where ∏ f is the product map from A to Πi, Xᵢ, and similarly for ∏ g.

• ContinuousMap.HomotopyRel.pi homotopies: Same as ContinuousMap.Homotopy.pi, but all homotopies are done relative to some set S ⊆ A.

• ContinuousMap.Homotopy.prod F G is the product of homotopies F and G, where F is a homotopy between f₀ and f₁, G is a homotopy between g₀ and g₁. The result F × G is a homotopy between (f₀ × g₀) and (f₁ × g₁). Again, all homotopies are done relative to S.

• ContinuousMap.HomotopyRel.prod F G: Same as ContinuousMap.Homotopy.prod, but all homotopies are done relative to some set S ⊆ A.

### Path products #

• Path.Homotopic.pi The product of a family of path classes, where a path class is an equivalence class of paths up to path homotopy.

• Path.Homotopic.prod The product of two path classes.

@[simp]
theorem ContinuousMap.HomotopyRel.pi_apply {I : Type u_1} {A : Type u_2} {X : IType u_3} [(i : I) → TopologicalSpace (X i)] [] {f : (i : I) → C(A, X i)} {g : (i : I) → C(A, X i)} {S : Set A} (homotopies : (i : I) → ContinuousMap.HomotopyRel (f i) (g i) S) (a : ) (i : I) :
↑(ContinuousMap.HomotopyRel.pi homotopies) a i = ↑(homotopies i) a
@[simp]
theorem ContinuousMap.HomotopyRel.pi_toFun {I : Type u_1} {A : Type u_2} {X : IType u_3} [(i : I) → TopologicalSpace (X i)] [] {f : (i : I) → C(A, X i)} {g : (i : I) → C(A, X i)} {S : Set A} (homotopies : (i : I) → ContinuousMap.HomotopyRel (f i) (g i) S) (a : ) (i : I) :
↑(ContinuousMap.HomotopyRel.pi homotopies) a i = ↑(homotopies i) a
def ContinuousMap.HomotopyRel.pi {I : Type u_1} {A : Type u_2} {X : IType u_3} [(i : I) → TopologicalSpace (X i)] [] {f : (i : I) → C(A, X i)} {g : (i : I) → C(A, X i)} {S : Set A} (homotopies : (i : I) → ContinuousMap.HomotopyRel (f i) (g i) S) :

The relative product homotopy of homotopies between functions f and g

Instances For
@[simp]
theorem ContinuousMap.Homotopy.prod_apply {α : Type u_1} {β : Type u_2} [] [] {A : Type u_3} [] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} (F : ) (G : ) (t : ) :
↑() t = (F t, G t)
def ContinuousMap.Homotopy.prod {α : Type u_1} {β : Type u_2} [] [] {A : Type u_3} [] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} (F : ) (G : ) :

The product of homotopies F and G, where F takes f₀ to f₁ and G takes g₀ to g₁

Instances For
@[simp]
theorem ContinuousMap.HomotopyRel.prod_toFun {α : Type u_1} {β : Type u_2} [] [] {A : Type u_3} [] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} {S : Set A} (F : ) (G : ) (t : ) :
↑() t = (F t, G t)
@[simp]
theorem ContinuousMap.HomotopyRel.prod_apply {α : Type u_1} {β : Type u_2} [] [] {A : Type u_3} [] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} {S : Set A} (F : ) (G : ) (t : ) :
↑() t = (F t, G t)
def ContinuousMap.HomotopyRel.prod {α : Type u_1} {β : Type u_2} [] [] {A : Type u_3} [] {f₀ : C(A, α)} {f₁ : C(A, α)} {g₀ : C(A, β)} {g₁ : C(A, β)} {S : Set A} (F : ) (G : ) :

The relative product of homotopies F and G, where F takes f₀ to f₁ and G takes g₀ to g₁

Instances For
def Path.Homotopic.piHomotopy {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (as i) (bs i)) (H : (i : ι) → Path.Homotopy (γ₀ i) (γ₁ i)) :
Path.Homotopy (Path.pi γ₀) (Path.pi γ₁)

The product of a family of path homotopies. This is just a specialization of HomotopyRel.

Instances For
def Path.Homotopic.pi {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (γ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) :

The product of a family of path homotopy classes.

Instances For
theorem Path.Homotopic.pi_lift {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (γ : (i : ι) → Path (as i) (bs i)) :
(Path.Homotopic.pi fun i => Quotient.mk (Path.Homotopic.setoid (as i) (bs i)) (γ i)) = Quotient.mk (Path.Homotopic.setoid (fun i => as i) fun i => bs i) ()
theorem Path.Homotopic.comp_pi_eq_pi_comp {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} {cs : (i : ι) → X i} (γ₀ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) (γ₁ : (i : ι) → Path.Homotopic.Quotient (bs i) (cs i)) :
= Path.Homotopic.pi fun i => Path.Homotopic.Quotient.comp (γ₀ i) (γ₁ i)

Composition and products commute. This is Path.trans_pi_eq_pi_trans descended to path homotopy classes.

@[reducible]
def Path.Homotopic.proj {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (i : ι) (p : ) :

Abbreviation for projection onto the ith coordinate.

Instances For
@[simp]
theorem Path.Homotopic.proj_pi {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (i : ι) (paths : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)) :

Lemmas showing projection is the inverse of pi.

@[simp]
theorem Path.Homotopic.pi_proj {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {as : (i : ι) → X i} {bs : (i : ι) → X i} (p : ) :
(Path.Homotopic.pi fun i => ) = p
def Path.Homotopic.prodHomotopy {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} {p₁ : Path a₁ a₂} {p₁' : Path a₁ a₂} {p₂ : Path b₁ b₂} {p₂' : Path b₁ b₂} (h₁ : Path.Homotopy p₁ p₁') (h₂ : Path.Homotopy p₂ p₂') :
Path.Homotopy (Path.prod p₁ p₂) (Path.prod p₁' p₂')

The product of homotopies h₁ and h₂. This is HomotopyRel.prod specialized for path homotopies.

Instances For
def Path.Homotopic.prod {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (q₁ : ) (q₂ : ) :
Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)

The product of path classes q₁ and q₂. This is Path.prod descended to the quotient.

Instances For
theorem Path.Homotopic.prod_lift {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (p₁ : Path a₁ a₂) (p₂ : Path b₁ b₂) :
Path.Homotopic.prod (Quotient.mk () p₁) (Quotient.mk () p₂) = Quotient.mk (Path.Homotopic.setoid (a₁, b₁) (a₂, b₂)) (Path.prod p₁ p₂)
theorem Path.Homotopic.comp_prod_eq_prod_comp {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {a₃ : α} {b₁ : β} {b₂ : β} {b₃ : β} (q₁ : ) (q₂ : ) (r₁ : ) (r₂ : ) :

Products commute with path composition. This is trans_prod_eq_prod_trans descended to the quotient.

@[reducible]
def Path.Homotopic.projLeft {α : Type u_1} {β : Type u_2} [] [] {c₁ : α × β} {c₂ : α × β} (p : ) :
Path.Homotopic.Quotient c₁.fst c₂.fst

Abbreviation for projection onto the left coordinate of a path class.

Instances For
@[reducible]
def Path.Homotopic.projRight {α : Type u_1} {β : Type u_2} [] [] {c₁ : α × β} {c₂ : α × β} (p : ) :
Path.Homotopic.Quotient c₁.snd c₂.snd

Abbreviation for projection onto the right coordinate of a path class.

Instances For
@[simp]
theorem Path.Homotopic.projLeft_prod {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (q₁ : ) (q₂ : ) :
= q₁

Lemmas showing projection is the inverse of product.

@[simp]
theorem Path.Homotopic.projRight_prod {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (q₁ : ) (q₂ : ) :
= q₂
@[simp]
theorem Path.Homotopic.prod_projLeft_projRight {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)) :