mathlib documentation

algebraic_topology.fundamental_groupoid.product

Fundamental groupoid preserves products #

In this file, we give the following definitions/theorems:

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

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

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

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