# mathlib3documentation

algebraic_topology.fundamental_groupoid.product

# 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_iso An isomorphism between Π i, (π Xᵢ) and π (Πi, Xᵢ), whose inverse is precisely the product of the maps π (Π i, Xᵢ) → π (Xᵢ), each induced by the projection in Top Π i, Xᵢ → Xᵢ.

• fundamental_groupoid_functor.prod_iso An 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_product A proof that the fundamental groupoid functor preserves all products.

noncomputable def fundamental_groupoid_functor.proj {I : Type u} (X : I Top) (i : I) :

The projection map Π i, X i → X i induces a map π(Π i, X i) ⟶ π(X i).

Equations
@[simp]
theorem fundamental_groupoid_functor.proj_map {I : Type u} (X : I Top) (i : I) (x₀ x₁ : (fundamental_groupoid.fundamental_groupoid_functor.obj (Top.of (Π (i : I), (X i))))) (p : x₀ x₁) :

The projection map is precisely path.homotopic.proj interpreted as a functor

@[simp]
theorem fundamental_groupoid_functor.pi_to_pi_Top_obj {I : Type u} (X : I Top) (g : Π (i : I), ) (i : I) :
= g i
@[simp]
theorem fundamental_groupoid_functor.pi_to_pi_Top_map {I : Type u} (X : I Top) (v₁ v₂ : Π (i : I), ) (p : v₁ v₂) :

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
@[simp]
@[simp]

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

Equations
noncomputable def fundamental_groupoid_functor.pi_Top_to_pi_cone {I : Type u} (X : I Top) :

This is pi_iso.inv as a cone morphism (in fact, isomorphism)

Equations
Instances for fundamental_groupoid_functor.pi_Top_to_pi_cone
@[protected, instance]

The fundamental groupoid functor preserves products

Equations
noncomputable def fundamental_groupoid_functor.proj_left (A B : Top) :

The induced map of the left projection map X × Y → X

Equations
noncomputable def fundamental_groupoid_functor.proj_right (A B : Top) :

The induced map of the right projection map X × Y → Y

Equations
@[simp]
theorem fundamental_groupoid_functor.proj_left_map (A B : Top) (x₀ x₁ : ) (p : x₀ x₁) :
@[simp]
theorem fundamental_groupoid_functor.proj_right_map (A B : Top) (x₀ x₁ : ) (p : x₀ x₁) :

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
• = {obj := , map := λ (x y : (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₁) = p₁
@[simp]
theorem fundamental_groupoid_functor.prod_to_prod_Top_map (A B : Top) {x₀ x₁ : } {y₀ y₁ : } (p₀ : x₀ x₁) (p₁ : y₀ y₁) :
(p₀, p₁) = p₁

Shows prod_to_prod_Top is an isomorphism, whose inverse is precisely the product of the induced left and right projections.

Equations
@[simp]
@[simp]