Theorems · Definition · algebraic topology

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)

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Cited by

3 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound