Zulip Chat Archive

Stream: general

Topic: Moving fundamental groupoid out of topology/homotopy

Praneeth Kolichala (Jan 22 2022 at 01:31):

Not sure what exactly should fall in the category of algebraic_topology -- maybe it will only focus primarily on homology or cohomology of topological spaces once we have those -- but I think some of the things in topology/homotopy would be better placed there, maybe in a folder algebraic_topology/fundamental_groupoid. Specifically, the file topology/homotopy/fundamental_groupoid.lean and the part oftopology/homotopy/product.lean which deals explicitly with the fundamental groupoid functor might be better placed there.

Last updated: Dec 20 2023 at 11:08 UTC