# Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

# Fundamental groupoid preserves products #

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

• FundamentalGroupoidFunctor.piIso 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ᵢ.

• FundamentalGroupoidFunctor.prodIso 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

• FundamentalGroupoidFunctor.preservesProduct A 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).

Instances For
@[simp]
theorem FundamentalGroupoidFunctor.proj_map {I : Type u} (X : ITopCat) (i : I) (x₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) (x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) (p : x₀ x₁) :
().map p =

The projection map is precisely Path.Homotopic.proj interpreted as a functor

@[simp]
theorem FundamentalGroupoidFunctor.piToPiTop_obj {I : Type u} (X : ITopCat) (g : (i : I) → ↑()) (i : I) :
((i : I) → ↑()).obj CategoryTheory.CategoryStruct.toQuiver (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor g i = g i
@[simp]
theorem FundamentalGroupoidFunctor.piToPiTop_map {I : Type u} (X : ITopCat) :
∀ {X Y : (i : I) → ↑()} (p : X Y),
def FundamentalGroupoidFunctor.piToPiTop {I : Type u} (X : ITopCat) :
CategoryTheory.Functor ((i : I) → ↑()) ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))

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

Instances For
@[simp]
theorem FundamentalGroupoidFunctor.piIso_hom {I : Type u} (X : ITopCat) :
@[simp]
theorem FundamentalGroupoidFunctor.piIso_inv {I : Type u} (X : ITopCat) :

Shows piToPiTop is an isomorphism, whose inverse is precisely the pi product of the induced projections. This shows that fundamentalGroupoidFunctor preserves products.

Instances For

Equivalence between the categories of cones over the objects π Xᵢ written in two ways

Instances For

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

Instances For

The fundamental groupoid functor preserves products

Instances For

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

Instances For

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

Instances For
@[simp]
@[simp]
@[simp]
theorem FundamentalGroupoidFunctor.prodToProdTop_obj (A : TopCat) (B : TopCat) (g : ) :
().obj g = g

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

Instances For
theorem FundamentalGroupoidFunctor.prodToProdTop_map (A : TopCat) (B : TopCat) {x₀ : } {x₁ : } {y₀ : } {y₁ : } (p₀ : x₀ x₁) (p₁ : y₀ y₁) :
().map (p₀, p₁) =

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

Instances For