mathlib3 documentation


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:

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


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)


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.


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).