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 #
-
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.
Fundamental groupoid preserves products #
-
fundamental_groupoid_functor.pi_isoAn isomorphism between Π i, (π Xᵢ) and π (Πi, Xᵢ), whose inverse is precisely the product of the maps π (Π i, Xᵢ) → π (Xᵢ), each induced by the projection inTopΠ i, Xᵢ → Xᵢ. -
fundamental_groupoid_functor.prod_isoAn isomorphism between πX × πY and π (X × Y), whose inverse is precisely the product of the maps π (X × Y) → πX and π (X × Y) → Y, each induced by the projections X × Y → X and X × Y → Y -
fundamental_groupoid_functor.preserves_productA proof that the fundamental groupoid functor preserves all products.
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 := _}, to_fun_zero := _, to_fun_one := _}
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, to_fun_zero := _, to_fun_one := _}, 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 := _}, to_fun_zero := _, to_fun_one := _}
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, to_fun_zero := _, to_fun_one := _}, 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
The projection map Π i, X i → X i induces a map π(Π i, X i) ⟶ π(X i).
Equations
- fundamental_groupoid_functor.proj X i = fundamental_groupoid.fundamental_groupoid_functor.map {to_fun := λ (p : Π (i : I), ↥(X i)), p i, continuous_to_fun := _}
The projection map is precisely path.homotopic.proj interpreted as a functor
The map taking the pi product of a family of fundamental groupoids to the fundamental
groupoid of the pi product. This is actually an isomorphism (see pi_iso)
Equations
- fundamental_groupoid_functor.pi_to_pi_Top X = {obj := λ (g : Π (i : I), (fundamental_groupoid.fundamental_groupoid_functor.obj (X i)).α), g, map := λ (v₁ v₂ : Π (i : I), (fundamental_groupoid.fundamental_groupoid_functor.obj (X i)).α) (p : v₁ ⟶ v₂), path.homotopic.pi p, map_id' := _, map_comp' := _}
Shows pi_to_pi_Top is an isomorphism, whose inverse is precisely the pi product
of the induced projections. This shows that fundamental_groupoid_functor preserves products.
Equations
Equivalence between the categories of cones over the objects π Xᵢ written in two ways
This is pi_iso.inv as a cone morphism (in fact, isomorphism)
Equations
The fundamental groupoid functor preserves products
Equations
- fundamental_groupoid_functor.preserves_product X = category_theory.limits.preserves_limit_of_preserves_limit_cone (Top.pi_fan_is_limit X) ((category_theory.limits.is_limit.of_cone_equiv (fundamental_groupoid_functor.cone_discrete_comp X)).to_fun (_.mpr ((category_theory.Groupoid.pi_limit_cone (category_theory.discrete.functor (λ (i : I), fundamental_groupoid.fundamental_groupoid_functor.obj (X i)))).is_limit.of_iso_limit (category_theory.as_iso (fundamental_groupoid_functor.pi_Top_to_pi_cone X)).symm)))
The induced map of the left projection map X × Y → X
Equations
The induced map of the right projection map X × Y → Y
Equations
The map taking the product of two fundamental groupoids to the fundamental groupoid of the product
of the two topological spaces. This is in fact an isomorphism (see prod_iso).
Equations
- fundamental_groupoid_functor.prod_to_prod_Top A B = {obj := λ (g : (fundamental_groupoid.fundamental_groupoid_functor.obj A).α × (fundamental_groupoid.fundamental_groupoid_functor.obj B).α), g, map := λ (x y : (fundamental_groupoid.fundamental_groupoid_functor.obj A).α × (fundamental_groupoid.fundamental_groupoid_functor.obj B).α) (p : x ⟶ y), fundamental_groupoid_functor.prod_to_prod_Top._match_1 A B x y p, map_id' := _, map_comp' := _}
- fundamental_groupoid_functor.prod_to_prod_Top._match_1 A B (x₀, x₁) (y₀, y₁) (p₀, p₁) = path.homotopic.prod p₀ p₁
Shows prod_to_prod_Top is an isomorphism, whose inverse is precisely the product
of the induced left and right projections.
Equations
- fundamental_groupoid_functor.prod_iso A B = {hom := fundamental_groupoid_functor.prod_to_prod_Top A B, inv := (fundamental_groupoid_functor.proj_left A B).prod' (fundamental_groupoid_functor.proj_right A B), hom_inv_id' := _, inv_hom_id' := _}