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

def FundamentalGroupoidFunctor.proj {I : Type u} (X : ITopCat) (i : I) :
CategoryTheory.Functor ( (TopCat.of ((i : I) → (X i)))) ()

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

Equations
• = { toFun := fun (p : (i : I) → (X i)) => p i, continuous_toFun := }
Instances For
@[simp]
theorem FundamentalGroupoidFunctor.proj_map {I : Type u} (X : ITopCat) (i : I) (x₀ : ( (TopCat.of ((i : I) → (X i))))) (x₁ : ( (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_map {I : Type u} (X : ITopCat) :
∀ {X_1 Y : (i : I) → ()} (p : X_1 Y),
@[simp]
theorem FundamentalGroupoidFunctor.piToPiTop_obj_as {I : Type u} (X : ITopCat) (g : (i : I) → ()) (i : I) :
( g).as i = (g i).as
def FundamentalGroupoidFunctor.piToPiTop {I : Type u} (X : ITopCat) :
CategoryTheory.Functor ((i : I) → ()) ( (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)

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FundamentalGroupoidFunctor.piIso_hom {I : Type u} (X : ITopCat) :
@[simp]
theorem FundamentalGroupoidFunctor.piIso_inv {I : Type u} (X : ITopCat) :
def FundamentalGroupoidFunctor.piIso {I : Type u} (X : ITopCat) :
CategoryTheory.Grpd.of ((i : I) → ()) (TopCat.of ((i : I) → (X i)))

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

Equations
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For

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

Equations
Instances For
theorem FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone {I : Type u} (X : ITopCat) :
.functor.obj () = CategoryTheory.Limits.Fan.mk ( (TopCat.of ((i : I) → (X i))))

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

Equations
• = { hom := , w := }
Instances For
Equations
• =

The fundamental groupoid functor preserves products

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• = { toFun := Prod.fst, continuous_toFun := }
Instances For

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

Equations
• = { toFun := Prod.snd, continuous_toFun := }
Instances For
@[simp]
theorem FundamentalGroupoidFunctor.projLeft_map (A : TopCat) (B : TopCat) (x₀ : ( (TopCat.of (A × B)))) (x₁ : ( (TopCat.of (A × B)))) (p : x₀ x₁) :
@[simp]
theorem FundamentalGroupoidFunctor.projRight_map (A : TopCat) (B : TopCat) (x₀ : ( (TopCat.of (A × B)))) (x₁ : ( (TopCat.of (A × B)))) (p : x₀ x₁) :
@[simp]
theorem FundamentalGroupoidFunctor.prodToProdTop_obj (A : TopCat) (B : TopCat) (g : ) :
.obj g = { as := (g.1.as, g.2.as) }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem FundamentalGroupoidFunctor.prodToProdTop_map (A : TopCat) (B : TopCat) {x₀ : } {x₁ : } {y₀ : } {y₁ : } (p₀ : x₀ x₁) (p₁ : y₀ y₁) :
.map (p₀, p₁) =
@[simp]
theorem FundamentalGroupoidFunctor.prodIso_inv (A : TopCat) (B : TopCat) :
.inv = .prod'

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

Equations
• One or more equations did not get rendered due to their size.
Instances For