Product of homotopies #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
-
continuous_map.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ᵢ. Lethomotopiesbe a family of homotopies from fᵢ to gᵢ for each i. Thenhomotopy.pi homotopiesis the canonical homotopy from ∏ f to ∏ g, where ∏ f is the product map from A to Πi, Xᵢ, and similarly for ∏ g. -
continuous_map.homotopy_rel.pi homotopies: Same ascontinuous_map.homotopy.pi, but all homotopies are done relative to some set S ⊆ A. -
continuous_map.homotopy.prod F Gis 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. -
continuous_map.homotopy_rel.prod F G: Same ascontinuous_map.homotopy.prod, but all homotopies are done relative to some set S ⊆ A.
Path products #
-
path.homotopic.piThe product of a family of path classes, where a path class is an equivalence class of paths up to path homotopy. -
path.homotopic.prodThe product of two path classes.
The product homotopy of homotopies between functions f and g
Equations
- continuous_map.homotopy.pi homotopies = {to_continuous_map := {to_fun := λ (t : ↥unit_interval × A) (i : I), ⇑(homotopies i) t, continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}
The relative product homotopy of homotopies between functions f and g
Equations
- continuous_map.homotopy_rel.pi homotopies = {to_homotopy := {to_continuous_map := (continuous_map.homotopy.pi (λ (i : I), (homotopies i).to_homotopy)).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
The product of homotopies F and G,
where F takes f₀ to f₁ and G takes g₀ to g₁
Equations
- F.prod G = {to_continuous_map := {to_fun := λ (t : ↥unit_interval × A), (⇑F t, ⇑G t), continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}
The relative product of homotopies F and G,
where F takes f₀ to f₁ and G takes g₀ to g₁
Equations
- F.prod G = {to_homotopy := {to_continuous_map := (F.to_homotopy.prod G.to_homotopy).to_continuous_map, map_zero_left' := _, map_one_left' := _}, prop' := _}
The product of a family of path homotopies. This is just a specialization of homotopy_rel
Equations
The product of a family of path homotopy classes
Equations
- path.homotopic.pi γ = quotient.map path.pi path.homotopic.pi._proof_1 (quotient.choice γ)
Composition and products commute.
This is path.trans_pi_eq_pi_trans descended to path homotopy classes
Abbreviation for projection onto the ith coordinate
Equations
- path.homotopic.proj i p = p.map_fn {to_fun := λ (p : Π (i : ι), X i), p i, continuous_to_fun := _}
Lemmas showing projection is the inverse of pi
The product of homotopies h₁ and h₂.
This is homotopy_rel.prod specialized for path homotopies.
Equations
The product of path classes q₁ and q₂. This is path.prod descended to the quotient
Equations
- path.homotopic.prod q₁ q₂ = quotient.map₂ path.prod path.homotopic.prod._proof_1 q₁ q₂
Products commute with path composition.
This is trans_prod_eq_prod_trans descended to the quotient.
Abbreviation for projection onto the left coordinate of a path class
Equations
- path.homotopic.proj_left p = p.map_fn {to_fun := prod.fst β, continuous_to_fun := _}
Abbreviation for projection onto the right coordinate of a path class
Equations
- path.homotopic.proj_right p = p.map_fn {to_fun := prod.snd β, continuous_to_fun := _}
Lemmas showing projection is the inverse of product