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.

noncomputable 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₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))) (p : x₀ ⟶ x₁) : (proj X i).map p = Path.Homotopic.proj i p

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

noncomputable 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.piToPiTop_obj_as {I : Type u} (X : I → TopCat) (g : (i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))) (i : I) : ((piToPiTop X).obj g).as i = (g i).as

@[simp]

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

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

@[simp]

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

@[simp]

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

noncomputable def FundamentalGroupoidFunctor.coneDiscreteComp {I : Type u} (X : I → TopCat) : CategoryTheory.Limits.Cone ((CategoryTheory.Discrete.functor X).comp FundamentalGroupoid.fundamentalGroupoidFunctor) ≌ CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor fun (i : 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) : (coneDiscreteComp X).functor.obj (FundamentalGroupoid.fundamentalGroupoidFunctor.mapCone (TopCat.piFan X)) = CategoryTheory.Limits.Fan.mk (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i)))) (proj X)

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

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

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

theorem 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₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))) (p : x₀ ⟶ x₁) : (projLeft A B).map p = Path.Homotopic.projLeft p

@[simp]

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

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

@[simp]

theorem FundamentalGroupoidFunctor.prodToProdTop_obj (A : TopCat) (B : TopCat) (g : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) × ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) : (prodToProdTop A B).obj g = { as := (g.1.as, g.2.as) }

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

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

@[simp]

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

@[simp]

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