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 of
topology/homotopy/product.lean which deals explicitly with the fundamental groupoid functor might be better placed there.
Last updated: Aug 03 2023 at 10:10 UTC