English
The map from π_x A × π_x B to π_x (TopCat.of (A × B)) sends a pair (g,f) to the corresponding homotopy class of paths in the product space.
Русский
Отображение из произведения фундаментальных groupoid в фундаментальную groupoid произведения пространств отправляет пару на соответствующий гомотопический класс путей в произведении.
LaTeX
$$$$ prodToProdTop : \\pi_x A × π_x B \\to π_x (TopCat.of (A × B)) $$$$
Lean4
/-- 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`).
-/
@[simps obj]
def prodToProdTop : πₓ A × πₓ B ⥤ πₓ (TopCat.of (A × B))
where
obj g := ⟨g.fst.as, g.snd.as⟩
map {x y}
p :=
match x, y, p with
| (_, _), (_, _), (p₀, p₁) => @Path.Homotopic.prod _ _ (_) (_) _ _ _ _ p₀ p₁
map_id := by
rintro ⟨x₀, x₁⟩
simp only
rfl
map_comp {x y z} f
g :=
match x, y, z, f, g with
| (_, _), (_, _), (_, _), (f₀, f₁), (g₀, g₁) => (Path.Homotopic.comp_prod_eq_prod_comp f₀ f₁ g₀ g₁).symm
