Fundamental groupoid preserves products #
In this file, we give the following definitions/theorems:
FundamentalGroupoidFunctor.piIsoAn 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ᵢ.
FundamentalGroupoidFunctor.prodIsoAn 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
FundamentalGroupoidFunctor.preservesProductA 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).
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
piToPiTop is an isomorphism, whose inverse is precisely the pi product
of the induced projections. This shows that
fundamentalGroupoidFunctor preserves products.
Equivalence between the categories of cones over the objects
π Xᵢ written in two ways
piIso.inv as a cone morphism (in fact, isomorphism)
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
prodToProdTop is an isomorphism, whose inverse is precisely the product
of the induced left and right projections.