English
The product to product top map is an isomorphism whose inverse is given by the product of left and right projections.
Русский
Отображение prodToProdTop является изоморфизмом, обратное которому дано произведением левого и правого проекций.
LaTeX
$$$$ prodIso(A,B): (\\pi_x A × π_x B) \\cong π_x (TopCat.of (A × B)) $$$$
Lean4
/-- Shows `prodToProdTop` is an isomorphism, whose inverse is precisely the product
of the induced left and right projections.
-/
@[simps]
def prodIso : CategoryTheory.Grpd.of (πₓ A × πₓ B) ≅ πₓ (TopCat.of (A × B))
where
hom := prodToProdTop A B
inv := (projLeft A B).prod' (projRight A B)
hom_inv_id := by
change prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 _
apply CategoryTheory.Functor.hext; · intros; ext <;> simp <;> rfl
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ ⟨f₀, f₁⟩
have :
Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁ :=
And.intro (Path.Homotopic.projLeft_prod f₀ f₁) (Path.Homotopic.projRight_prod f₀ f₁)
simpa
inv_hom_id := by
change (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 _
apply CategoryTheory.Functor.hext
· intros; apply FundamentalGroupoid.ext; apply Prod.ext <;> simp <;> rfl
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ f
simpa [-Path.Homotopic.prod_projLeft_projRight] using Path.Homotopic.prod_projLeft_projRight f
