Lean4
/-- Shows `piToPiTop` is an isomorphism, whose inverse is precisely the pi product
of the induced projections. This shows that `fundamentalGroupoidFunctor` preserves products.
-/
@[simps]
def piIso : CategoryTheory.Grpd.of (∀ i : I, πₓ (X i)) ≅ πₓ (TopCat.of (∀ i, X i))
where
hom := piToPiTop X
inv := CategoryTheory.Functor.pi' (proj X)
hom_inv_id := by
change piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 _
apply CategoryTheory.Functor.ext ?_ ?_
· intros; rfl
· intros; ext; simp
inv_hom_id := by
change CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 _
apply CategoryTheory.Functor.ext
· intro _ _ f
suffices Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f by simpa
change Path.Homotopic.pi (fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = _
simp
· intros; rfl
