chore(topology/category/Top/limits): split file (#18871)

Per 
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233487.20last.20minute.20split.3F

This file is already being ported at leanprover-community/mathlib4#3487, but:
* it's not going so well right now
* it is going well up to the point of the proposed new `limits/basic.lean`
* that is sufficient to port the files needed for Copenhagen



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -1,4 +1,4 @@
-import topology.category.Top.limits
+import topology.category.Top.limits.basic
 import topology.instances.real
 import topology.tactic
 

src/algebraic_geometry/open_immersion.lean

@@ -7,6 +7,7 @@ import algebraic_geometry.presheafed_space.has_colimits
 import category_theory.limits.shapes.binary_products
 import category_theory.limits.preserves.shapes.pullbacks
 import topology.sheaves.functors
+import topology.category.Top.limits.pullbacks
 import algebraic_geometry.Scheme
 import category_theory.limits.shapes.strict_initial
 import category_theory.limits.shapes.comm_sq

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebraic_geometry.presheafed_space
-import topology.category.Top.limits
+import topology.category.Top.limits.basic
 import topology.sheaves.limits
 
 /-!

src/algebraic_topology/fundamental_groupoid/product.lean

@@ -6,7 +6,7 @@ Authors: Praneeth Kolichala
 
 import category_theory.groupoid
 import algebraic_topology.fundamental_groupoid.basic
-import topology.category.Top.limits
+import topology.category.Top.limits.products
 import topology.homotopy.product
 
 /-!

src/algebraic_topology/simplicial_set.lean

@@ -8,7 +8,7 @@ import algebraic_topology.topological_simplex
 import category_theory.limits.presheaf
 import category_theory.limits.types
 import category_theory.yoneda
-import topology.category.Top.limits
+import topology.category.Top.limits.basic
 
 /-!
 A simplicial set is just a simplicial object in `Type`,

src/category_theory/cofiltered_system.lean

@@ -5,7 +5,7 @@ Authors: Kyle Miller, Adam Topaz, Rémi Bottinelli, Junyan Xu
 -/
 import category_theory.filtered
 import data.set.finite
-import topology.category.Top.limits
+import topology.category.Top.limits.konig
 
 /-!
 # Cofiltered systems

src/category_theory/extensive.lean

@@ -6,7 +6,7 @@ Authors: Andrew Yang
 import category_theory.limits.shapes.comm_sq
 import category_theory.limits.shapes.strict_initial
 import category_theory.limits.shapes.types
-import topology.category.Top.limits
+import topology.category.Top.limits.pullbacks
 import category_theory.limits.functor_category
 
 /-!

src/topology/category/CompHaus/basic.lean

@@ -8,7 +8,7 @@ import category_theory.adjunction.reflective
 import topology.stone_cech
 import category_theory.monad.limits
 import topology.urysohns_lemma
-import topology.category.Top.limits
+import topology.category.Top.limits.basic
 
 /-!
 # The category of Compact Hausdorff Spaces

src/topology/category/Profinite/cofiltered_limit.lean

@@ -6,6 +6,8 @@ Authors: Adam Topaz
 import topology.category.Profinite.basic
 import topology.locally_constant.basic
 import topology.discrete_quotient
+import topology.category.Top.limits.cofiltered
+import topology.category.Top.limits.konig
 
 /-!
 # Cofiltered limits of profinite sets.