Theorems · Definition · algebraic topology

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

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Cited by

7 results in Mathlib

Foundations

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