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₀ : (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_as {I : Type u} (X : ITopCat) (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 : ITopCat) :
    ∀ {X_1 Y : (i : I) → (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))} (p : X_1 Y), (FundamentalGroupoidFunctor.piToPiTop X).map p = Path.Homotopic.pi p

    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

      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

        The fundamental groupoid functor preserves products

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

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

          Equations
          Instances For

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

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

              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