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 : I → TopCat) (i : I) : CategoryTheory.Functor ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i)))) ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))

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

@[simp]

theorem FundamentalGroupoidFunctor.proj_map {I : Type u} (X : I → TopCat) (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₁) : (FundamentalGroupoidFunctor.proj X i).map p = Path.Homotopic.proj i p

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

instance FundamentalGroupoidFunctor.instForAllTopologicalSpaceαGroupoidObjTopCatToQuiverToCategoryStructInstTopCatLargeCategoryGrpdCategoryToPrefunctorFundamentalGroupoidFunctor {I : Type u} (X : I → TopCat) (i : I) : TopologicalSpace ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))

@[simp]

theorem FundamentalGroupoidFunctor.piToPiTop_obj {I : Type u} (X : I → TopCat) (g : (i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))) (i : I) : ((i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))).obj CategoryTheory.CategoryStruct.toQuiver (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) CategoryTheory.CategoryStruct.toQuiver (FundamentalGroupoidFunctor.piToPiTop X).toPrefunctor g i = g i

@[simp]

theorem FundamentalGroupoidFunctor.piToPiTop_map {I : Type u} (X : I → TopCat) : ∀ {X Y : (i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))} (p : X ⟶ Y), (FundamentalGroupoidFunctor.piToPiTop X).map p = Path.Homotopic.pi p

def FundamentalGroupoidFunctor.piToPiTop {I : Type u} (X : I → TopCat) : CategoryTheory.Functor ((i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X 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)

@[simp]

theorem FundamentalGroupoidFunctor.piIso_hom {I : Type u} (X : I → TopCat) : (FundamentalGroupoidFunctor.piIso X).hom = FundamentalGroupoidFunctor.piToPiTop X

@[simp]

theorem FundamentalGroupoidFunctor.piIso_inv {I : Type u} (X : I → TopCat) : (FundamentalGroupoidFunctor.piIso X).inv = CategoryTheory.Functor.pi' (FundamentalGroupoidFunctor.proj X)

def FundamentalGroupoidFunctor.piIso {I : Type u} (X : I → TopCat) : CategoryTheory.Grpd.of ((i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))) ≅ FundamentalGroupoid.fundamentalGroupoidFunctor.obj (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.

def FundamentalGroupoidFunctor.coneDiscreteComp {I : Type u} (X : I → TopCat) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Discrete.functor X) FundamentalGroupoid.fundamentalGroupoidFunctor) ≌ CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor fun i => FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))

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

theorem FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone {I : Type u} (X : I → TopCat) : (FundamentalGroupoidFunctor.coneDiscreteComp X).functor.obj (FundamentalGroupoid.fundamentalGroupoidFunctor.mapCone (TopCat.piFan X)) = CategoryTheory.Limits.Fan.mk (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i)))) (FundamentalGroupoidFunctor.proj X)

def FundamentalGroupoidFunctor.piTopToPiCone {I : Type u} (X : I → TopCat) : CategoryTheory.Limits.Fan.mk (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i)))) (FundamentalGroupoidFunctor.proj X) ⟶ CategoryTheory.Grpd.piLimitFan fun i => FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i)

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

instance FundamentalGroupoidFunctor.instIsIsoFanGrpdCategoryObjTopCatToQuiverToCategoryStructInstTopCatLargeCategoryToPrefunctorFundamentalGroupoidFunctorCategoryDiscreteDiscreteCategoryFunctorMkOfForAllαTopologicalSpaceTopologicalSpaceTopologicalSpace_coeProjPiLimitFanPiTopToPiCone {I : Type u} (X : I → TopCat) : CategoryTheory.IsIso (FundamentalGroupoidFunctor.piTopToPiCone X)

def FundamentalGroupoidFunctor.preservesProduct {I : Type u} (X : I → TopCat) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor X) FundamentalGroupoid.fundamentalGroupoidFunctor

The fundamental groupoid functor preserves products

def FundamentalGroupoidFunctor.projLeft (A : TopCat) (B : TopCat) : CategoryTheory.Functor ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B))) ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)

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

def FundamentalGroupoidFunctor.projRight (A : TopCat) (B : TopCat) : CategoryTheory.Functor ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B))) ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)

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

@[simp]

theorem FundamentalGroupoidFunctor.projLeft_map (A : TopCat) (B : TopCat) (x₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))) (x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))) (p : x₀ ⟶ x₁) : (FundamentalGroupoidFunctor.projLeft A B).map p = Path.Homotopic.projLeft p

@[simp]

theorem FundamentalGroupoidFunctor.projRight_map (A : TopCat) (B : TopCat) (x₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))) (x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))) (p : x₀ ⟶ x₁) : (FundamentalGroupoidFunctor.projRight A B).map p = Path.Homotopic.projRight p

@[simp]

theorem FundamentalGroupoidFunctor.prodToProdTop_obj (A : TopCat) (B : TopCat) (g : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) × ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) : (FundamentalGroupoidFunctor.prodToProdTop A B).obj g = g

def FundamentalGroupoidFunctor.prodToProdTop (A : TopCat) (B : TopCat) : CategoryTheory.Functor (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) × ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))

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

theorem FundamentalGroupoidFunctor.prodToProdTop_map (A : TopCat) (B : TopCat) {x₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)} {x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)} {y₀ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)} {y₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)} (p₀ : x₀ ⟶ x₁) (p₁ : y₀ ⟶ y₁) : (FundamentalGroupoidFunctor.prodToProdTop A B).map (p₀, p₁) = Path.Homotopic.prod p₀ p₁

@[simp]

theorem FundamentalGroupoidFunctor.prodIso_inv (A : TopCat) (B : TopCat) : (FundamentalGroupoidFunctor.prodIso A B).inv = CategoryTheory.Functor.prod' (FundamentalGroupoidFunctor.projLeft A B) (FundamentalGroupoidFunctor.projRight A B)

@[simp]

theorem FundamentalGroupoidFunctor.prodIso_hom (A : TopCat) (B : TopCat) : (FundamentalGroupoidFunctor.prodIso A B).hom = FundamentalGroupoidFunctor.prodToProdTop A B

def FundamentalGroupoidFunctor.prodIso (A : TopCat) (B : TopCat) : CategoryTheory.Grpd.of (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) × ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) ≅ FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B))

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