Commit 2025-10-18 17:29 2c2d7566

chore(AlgebraicTopology): clean up FundamentalGroupoid (#28234)

• Extract FundamentalGroupoid.map (f : C(X, Y)) : FundamentalGroupoid X ⥤ FundamentalGroupoid Y from fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd
• Define FundamentalGroup.map (f : C(X, Y)) (x : X) : FundamentalGroup X x →* FundamentalGroup Y (f x) and mapOfEq : FundamentalGroup X x →* FundamentalGroup Y y that takes an assumption f x = y.
• Redefine FundamentalGroup to be End rather than Aut: since FundamentalGroupoid is a groupoid, End already has a group structure. This requires fixing some proofs about HomotopyGroups, so we take this opportunity to golf a few proofs and replace => by ↦.
• Golf within the file FundamentalGroupoid/Basic.
• Generalize toArrow up to fromPath in FundamentalGroupoid/FundamentalGroup from X : TopCat to [TopologicalSpace X].