Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Fundamental groupoid preserves products #

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

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₁) :

    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) → ↑(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]

    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

      Shows piToPiTop is an isomorphism, whose inverse is precisely the pi product of the induced projections. This shows that fundamentalGroupoidFunctor 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

            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

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

              Instances For