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

Equations

• FundamentalGroupoidFunctor.proj X i = FundamentalGroupoid.fundamentalGroupoidFunctor.map { toFun := fun (p : (i : I) → ↑(X i)) => p i, continuous_toFun := ⋯ }

@[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

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)

Equations

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

@[simp]

theorem FundamentalGroupoidFunctor.piToPiTop_obj_as {I : Type u} (X : I → TopCat) (g : (i : I) → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))) (i : I) : ((FundamentalGroupoidFunctor.piToPiTop X).obj g).as i = (g i).as

@[simp]

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

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.

Equations

• FundamentalGroupoidFunctor.piIso X = { hom := FundamentalGroupoidFunctor.piToPiTop X, inv := CategoryTheory.Functor.pi' (FundamentalGroupoidFunctor.proj X), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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.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

Equations

• FundamentalGroupoidFunctor.coneDiscreteComp X = CategoryTheory.Limits.Cones.postcomposeEquivalence (CategoryTheory.Discrete.compNatIsoDiscrete X FundamentalGroupoid.fundamentalGroupoidFunctor)

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 : I) => FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i)

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

Equations

• FundamentalGroupoidFunctor.piTopToPiCone X = { hom := CategoryTheory.Functor.pi' (FundamentalGroupoidFunctor.proj X), w := ⋯ }

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

Equations

• ⋯ = ⋯

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

The fundamental groupoid functor preserves products

Equations

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

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

Equations

• FundamentalGroupoidFunctor.projLeft A B = FundamentalGroupoid.fundamentalGroupoidFunctor.map { toFun := Prod.fst, continuous_toFun := ⋯ }

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

Equations

• FundamentalGroupoidFunctor.projRight A B = FundamentalGroupoid.fundamentalGroupoidFunctor.map { toFun := Prod.snd, continuous_toFun := ⋯ }

@[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

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

Equations

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

@[simp]

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

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₁

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.

Equations

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

@[simp]

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

@[simp]

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