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

Equations
Instances For
    @[simp]
    theorem FundamentalGroupoidFunctor.proj_map {I : Type u} (X : ITopCat) (i : I) (x₀ 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

    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.piToPiTop_obj_as {I : Type u} (X : ITopCat) (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 : ITopCat) {X✝ Y✝ : (i : I) → (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))} (p : X✝ Y✝) :

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

      Equations
      Instances For
        @[simp]

        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

          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