Fundamental groupoid preserves products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file, we give the following definitions/theorems:
-
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 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
Instances for fundamental_groupoid_functor.pi_Top_to_pi_cone
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_fan_is_limit (λ (i : I), fundamental_groupoid.fundamental_groupoid_functor.obj (X i))).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' := _}