chore(AlgebraicTopology/SingularSet): factor topology out of `Simplic…

…ialSet` into new file (#9428)

Mathlib.lean

@@ -561,6 +561,7 @@ import Mathlib.AlgebraicTopology.Quasicategory
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialSet
+import Mathlib.AlgebraicTopology.SingularSet
 import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.Analysis.Analytic.Basic

Mathlib/AlgebraicTopology/SimplicialSet.lean

@@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison, Adam Topaz
 -/
 import Mathlib.AlgebraicTopology.SimplicialObject
-import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.CategoryTheory.Yoneda
-import Mathlib.Topology.Category.TopCat.Limits.Basic
 
 #align_import algebraic_topology.simplicial_set from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
 /-!
+# Simplicial sets
+
 A simplicial set is just a simplicial object in `Type`,
 i.e. a `Type`-valued presheaf on the simplex category.
 
@@ -218,29 +218,3 @@ set_option linter.uppercaseLean3 false in
 end Augmented
 
 end SSet
-
-/-- The functor associating the singular simplicial set to a topological space. -/
-noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
-  ColimitAdj.restrictedYoneda SimplexCategory.toTop
-set_option linter.uppercaseLean3 false in
-#align Top.to_sSet TopCat.toSSet
-
-/-- The geometric realization functor. -/
-noncomputable def SSet.toTop : SSet ⥤ TopCat :=
-  ColimitAdj.extendAlongYoneda SimplexCategory.toTop
-set_option linter.uppercaseLean3 false in
-#align sSet.to_Top SSet.toTop
-
-/-- Geometric realization is left adjoint to the singular simplicial set construction. -/
-noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
-  ColimitAdj.yonedaAdjunction _
-set_option linter.uppercaseLean3 false in
-#align sSet_Top_adj sSetTopAdj
-
-/-- The geometric realization of the representable simplicial sets agree
-  with the usual topological simplices. -/
-noncomputable def SSet.toTopSimplex :
-    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
-  ColimitAdj.isExtensionAlongYoneda _
-set_option linter.uppercaseLean3 false in
-#align sSet.to_Top_simplex SSet.toTopSimplex

Mathlib/AlgebraicTopology/SingularSet.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison, Adam Topaz
+-/
+import Mathlib.AlgebraicTopology.SimplicialSet
+import Mathlib.AlgebraicTopology.TopologicalSimplex
+import Mathlib.Topology.Category.TopCat.Limits.Basic
+
+/-!
+# The singular simplicial set of a topological space and geometric realization of a simplicial set
+
+The *singular simplicial set* `TopCat.to_SSet.obj X` of a topological space `X`
+has as `n`-simplices the continuous maps `[n].toTop → X`.
+Here, `[n].toTop` is the standard topological `n`-simplex,
+defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology.
+
+The *geometric realization* functor `SSet.toTop.obj` is left adjoint to `TopCat.toSSet`.
+It is the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
+
+# Main definitions
+
+* `TopCat.toSSet : TopCat ⥤ SSet` is the functor
+  assigning the singular simplicial set to a topological space.
+* `SSet.toTop : SSet ⥤ TopCat` is the functor
+  assigning the geometric realization to a simplicial set.
+* `sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet` is the adjunction between these two functors.
+
+## TODO
+
+- Show that the singular simplicial set is a Kan complex.
+- Show the adjunction `sSetTopAdj` is a Quillen adjunction.
+
+-/
+
+open CategoryTheory
+
+/-- The functor associating the *singular simplicial set* to a topological space.
+
+Let `X` be a topological space.
+Then the singular simplicial set of `X`
+has as `n`-simplices the continuous maps `[n].toTop → X`.
+Here, `[n].toTop` is the standard topological `n`-simplex,
+defined as `{ f : Fin (n+1) → ℝ≥0 // ∑ i, f i = 1 }` with its subspace topology. -/
+noncomputable def TopCat.toSSet : TopCat ⥤ SSet :=
+  ColimitAdj.restrictedYoneda SimplexCategory.toTop
+set_option linter.uppercaseLean3 false in
+#align Top.to_sSet TopCat.toSSet
+
+/-- The *geometric realization functor* is
+the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.
+
+It is left adjoint to `TopCat.toSSet`, as witnessed by `sSetTopAdj`. -/
+noncomputable def SSet.toTop : SSet ⥤ TopCat :=
+  ColimitAdj.extendAlongYoneda SimplexCategory.toTop
+set_option linter.uppercaseLean3 false in
+#align sSet.to_Top SSet.toTop
+
+/-- Geometric realization is left adjoint to the singular simplicial set construction. -/
+noncomputable def sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet :=
+  ColimitAdj.yonedaAdjunction _
+set_option linter.uppercaseLean3 false in
+#align sSet_Top_adj sSetTopAdj
+
+/-- The geometric realization of the representable simplicial sets agree
+  with the usual topological simplices. -/
+noncomputable def SSet.toTopSimplex :
+    (yoneda : SimplexCategory ⥤ _) ⋙ SSet.toTop ≅ SimplexCategory.toTop :=
+  ColimitAdj.isExtensionAlongYoneda _
+set_option linter.uppercaseLean3 false in
+#align sSet.to_Top_simplex SSet.toTopSimplex

Mathlib/AlgebraicTopology/TopologicalSimplex.lean

@@ -14,7 +14,7 @@ import Mathlib.Topology.Instances.NNReal
 
 We define the natural functor from `SimplexCategory` to `TopCat` sending `[n]` to the
 topological `n`-simplex.
-This is used to define `TopCat.toSSet` in `AlgebraicTopology.SimplicialSet`.
+This is used to define `TopCat.toSSet` in `AlgebraicTopology.SingularSet`.
 -/