chore(Topology/Category): fix imports in TopCat.Basic (#17258)

A new file `TopCat.Sphere` is added so as to remove the import to `Analysis.InnerProductSpace.PiL2` that was added to the file `Topology.Category.TopCat.Basic` in PR #12502.

Mathlib.lean

@@ -4549,6 +4549,7 @@ import Mathlib.Topology.Category.TopCat.Limits.Products
 import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
 import Mathlib.Topology.Category.TopCat.OpenNhds
 import Mathlib.Topology.Category.TopCat.Opens
+import Mathlib.Topology.Category.TopCat.Sphere
 import Mathlib.Topology.Category.TopCat.Yoneda
 import Mathlib.Topology.Category.TopCommRingCat
 import Mathlib.Topology.Category.UniformSpace

Mathlib/Topology/CWComplex.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jiazhen Xia, Elliot Dean Young
 -/
 import Mathlib.Topology.Category.TopCat.Limits.Basic
+import Mathlib.Topology.Category.TopCat.Sphere
 import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Functor.OfSequence
 
@@ -34,7 +35,9 @@ universe u
 
 namespace RelativeCWComplex
 
-/-- The inclusion map from the `n`-sphere to the `(n + 1)`-disk -/
+/-- The inclusion map from the `n`-sphere to the `(n + 1)`-disk. (For `n = -1`, this
+involves the empty space `𝕊 (-1)`. This is the reason why `sphere` takes `n : ℤ` as
+an input rather than `n : ℕ`.) -/
 def sphereInclusion (n : ℤ) : 𝕊 n ⟶ 𝔻 (n + 1) where
   toFun := fun ⟨p, hp⟩ ↦ ⟨p, le_of_eq hp⟩
   continuous_toFun := ⟨fun t ⟨s, ⟨r, hro, hrs⟩, hst⟩ ↦ by
@@ -75,11 +78,11 @@ namespace RelativeCWComplex
 
 noncomputable section Topology
 
-/-- The inclusion map from `X` to `X'`, given that `X'` is obtained from `X` by attaching
-`(n + 1)`-disks -/
-def AttachCells.inclusion {X X' : TopCat.{u}} {n : ℤ} (att : AttachCells n X X') : X ⟶ X' :=
-  Limits.pushout.inl (Limits.Sigma.desc att.attachMaps)
-    (Limits.Sigma.map fun _ ↦ sphereInclusion n) ≫ att.iso_pushout.inv
+/-- The inclusion map from `X` to `X'`, when `X'` is obtained from `X`
+by attaching generalized cells `f : S ⟶ D`. -/
+def AttachGeneralizedCells.inclusion {S D : TopCat.{u}} {f : S ⟶ D} {X X' : TopCat.{u}}
+    (att : AttachGeneralizedCells f X X') : X ⟶ X' :=
+  Limits.pushout.inl _ _ ≫ att.iso_pushout.inv
 
 /-- The inclusion map from `sk n` (i.e., the $(n-1)$-skeleton) to `sk (n + 1)` (i.e., the
 $n$-skeleton) of a relative CW-complex -/

Mathlib/Topology/Category/TopCat/Basic.lean

@@ -5,7 +5,6 @@ Authors: Patrick Massot, Kim Morrison, Mario Carneiro
 -/
 import Mathlib.CategoryTheory.ConcreteCategory.BundledHom
 import Mathlib.Topology.ContinuousFunction.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
 
 /-!
 # Category instance for topological spaces
@@ -188,20 +187,4 @@ theorem openEmbedding_iff_isIso_comp' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶
   simp only [← Functor.map_comp]
   exact openEmbedding_iff_isIso_comp f g
 
-/-- The `n`-sphere is the set of points in ℝⁿ⁺¹ whose norm equals `1`,
-endowed with the subspace topology. -/
-noncomputable def sphere (n : ℤ) : TopCat.{u} :=
-  TopCat.of <| ULift <| Metric.sphere (0 : EuclideanSpace ℝ <| Fin <| (n + 1).toNat) 1
-
-/-- The `n`-disk is the set of points in ℝⁿ whose norm is at most `1`,
-endowed with the subspace topology. -/
-noncomputable def disk (n : ℤ) : TopCat.{u} :=
-  TopCat.of <| ULift <| Metric.closedBall (0 : EuclideanSpace ℝ <| Fin <| n.toNat) 1
-
-/-- `𝕊 n` denotes the `n`-sphere. -/
-scoped prefix:arg "𝕊 " => sphere
-
-/-- `𝔻 n` denotes the `n`-disk. -/
-scoped prefix:arg "𝔻 " => disk
-
 end TopCat

Mathlib/Topology/Category/TopCat/Sphere.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2024 Elliot Dean Young and Jiazhen Xia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jiazhen Xia, Elliot Dean Young
+-/
+
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Topology.Category.TopCat.Basic
+
+/-!
+# Euclidean spheres
+
+This files defines the `n`-sphere `𝕊 n` and the `n`-disk `𝔻` as objects in `TopCat`.
+The parameter `n` is in `ℤ` so as to facilitate the definition of
+CW-complexes (see the file `Topology.CWComplex`).
+
+-/
+
+universe u
+
+namespace TopCat
+
+/-- The `n`-sphere is the set of points in ℝⁿ⁺¹ whose norm equals `1`,
+endowed with the subspace topology. -/
+noncomputable def sphere (n : ℤ) : TopCat.{u} :=
+  TopCat.of <| ULift <| Metric.sphere (0 : EuclideanSpace ℝ <| Fin <| (n + 1).toNat) 1
+
+/-- The `n`-disk is the set of points in ℝⁿ whose norm is at most `1`,
+endowed with the subspace topology. -/
+noncomputable def disk (n : ℤ) : TopCat.{u} :=
+  TopCat.of <| ULift <| Metric.closedBall (0 : EuclideanSpace ℝ <| Fin <| n.toNat) 1
+
+/-- `𝕊 n` denotes the `n`-sphere. -/
+scoped prefix:arg "𝕊 " => sphere
+
+/-- `𝔻 n` denotes the `n`-disk. -/
+scoped prefix:arg "𝔻 " => disk
+
+end TopCat