feat(AlgebraicTopology/SimplicialSet): connected components of simplicial sets

Mathlib.lean

@@ -1534,8 +1534,10 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
 public import Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
+public import Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
 public import Mathlib.AlgebraicTopology.SimplicialSet.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.Path
+public import Mathlib.AlgebraicTopology.SimplicialSet.PiZero
 public import Mathlib.AlgebraicTopology.SimplicialSet.Presentable
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
@@ -1548,6 +1550,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
 public import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
 public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
+public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
 public import Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
 public import Mathlib.AlgebraicTopology.SingularHomology.Basic
 public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance

Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

@@ -74,6 +74,11 @@ lemma const_comp {X Y Z : SSet.{u}} (y : Y _⦋0⦌) (g : Y ⟶ Z) :
 def uliftFunctor : SSet.{u} ⥤ SSet.{max u v} :=
   (SimplicialObject.whiskering _ _).obj CategoryTheory.uliftFunctor.{v, u}
 
+/-- The functor which sends `n : SimplexCategoryᵒᵖ` to the evaluation
+functor `SSet.{u} ⥤ Type u` on the object `n`. -/
+protected abbrev evaluation : SimplexCategoryᵒᵖ ⥤ SSet.{u} ⥤ Type u :=
+  evaluation _ _
+
 /-- Truncated simplicial sets. -/
 abbrev Truncated (n : ℕ) := SimplicialObject.Truncated (Type u) n
 

Mathlib/AlgebraicTopology/SimplicialSet/Nonempty.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
+
+/-!
+# Nonempty simplicial sets
+
+-/
+
+@[expose] public section
+
+universe u
+
+open Simplicial CategoryTheory Limits
+
+namespace SSet
+
+variable (X : SSet.{u})
+
+/-- A simplicial set is nonempty when the type of `0`-simplices is nonempty. -/
+protected abbrev Nonempty : Prop := _root_.Nonempty (X _⦋0⦌)
+
+instance (n : SimplexCategoryᵒᵖ) [X.Nonempty] : Nonempty (X.obj n) :=
+  ⟨X.map (SimplexCategory.const n.unop ⦋0⦌ 0).op (Classical.arbitrary _)⟩
+
+instance [X.Nonempty] : Nonempty X.N := ⟨N.mk (n := 0) (Classical.arbitrary _) (by simp)⟩
+
+instance [X.Nonempty] : Nonempty X.S := ⟨S.mk (dim := 0) (Classical.arbitrary _)⟩
+
+instance (T : Type u) [Preorder T] [Nonempty T] : (nerve T).Nonempty :=
+  ⟨.mk₀ (Classical.arbitrary _)⟩
+
+instance (n : SimplexCategory) : (stdSimplex.obj n).Nonempty :=
+  ⟨stdSimplex.objEquiv.symm (SimplexCategory.const _ _ 0)⟩
+
+variable {X} in
+lemma nonempty_of_hom {Y : SSet.{u}} (f : Y ⟶ X) [Y.Nonempty] : X.Nonempty :=
+  ⟨f.app _ (Classical.arbitrary _)⟩
+
+lemma notNonempty_iff_hasDimensionLT_zero :
+    ¬ X.Nonempty ↔ X.HasDimensionLT 0 := by
+  simp only [not_nonempty_iff]
+  refine ⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩
+  · have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)
+    ext x
+    exact isEmptyElim x
+  · exact (lt_self_iff_false _).1 (X.dim_lt_of_nonDegenerate ⟨x, by simp⟩ 0)
+
+variable {X} in
+/-- If a simplicial set is nonempty, it is an initial object. -/
+def isInitialOfNotNonempty (hX : ¬ X.Nonempty) : IsInitial X := by
+  simp only [not_nonempty_iff] at hX
+  have (n : SimplexCategoryᵒᵖ) : IsEmpty (X.obj n) :=
+    Function.isEmpty (X.map (⦋0⦌.const n.unop 0).op)
+  exact IsInitial.ofUniqueHom (fun _ ↦
+    { app _ x := isEmptyElim x
+      naturality _ _ _  := by ext x; exact isEmptyElim x })
+    (fun _ _ ↦ by ext _ x; exact isEmptyElim x)
+
+end SSet

Mathlib/AlgebraicTopology/SimplicialSet/PiZero.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
+
+/-!
+# Connected components of simplicial sets
+
+In this file, we define the type `π₀ X` of connected components
+of a simplicial sets. We also introduce typeclasses
+`IsPreconnected X` and `IsConnected X`.
+
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory Simplicial Limits Opposite
+
+namespace SSet
+
+variable {X Y Z : SSet.{u}}
+
+/-- The homotopy relation on `0`-simplices of a simplicial set. It holds
+for `x₀` and `x₁` when there exists an edge from `x₀` to `x₁`. -/
+def π₀Rel (x₀ x₁ : X _⦋0⦌) : Prop :=
+  Nonempty (Edge x₀ x₁)
+
+variable (X) in
+/-- The type of connected components of a simplicial set. -/
+def π₀ : Type u := Quot (π₀Rel (X := X))
+
+namespace π₀
+
+/-- The connected component of a `0`-simplex of a simplicial set. -/
+def mk : X _⦋0⦌ → π₀ X := Quot.mk _
+
+lemma mk_surjective : Function.Surjective (π₀.mk (X := X)) := Quot.mk_surjective
+
+lemma sound {x₀ x₁ : X _⦋0⦌} (e : Edge x₀ x₁) :
+    π₀.mk x₀ = π₀.mk x₁ :=
+  Quot.sound ⟨e⟩
+
+lemma mk_eq_mk_iff (x₀ x₁ : X _⦋0⦌) :
+    π₀.mk x₀ = π₀.mk x₁ ↔ Relation.EqvGen π₀Rel x₀ x₁ :=
+  Quot.eq
+
+@[elab_as_elim, cases_eliminator, induction_eliminator]
+lemma rec {motive : π₀ X → Prop} (mk : ∀ (x : X _⦋0⦌), motive (.mk x)) (x : π₀ X) :
+    motive x := by
+  obtain ⟨x, rfl⟩ := x.mk_surjective
+  exact mk x
+
+/-- Constructor for maps from the type of connected components of a simplicial set. -/
+def lift {T : Type*} (f : X _⦋0⦌ → T)
+    (hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (_ : X.Edge x₀ x₁), f x₀ = f x₁) :
+    π₀ X → T :=
+  Quot.lift f (by rintro x y ⟨e⟩; exact hf e)
+
+@[simp]
+lemma lift_mk {T : Type*} (f : X _⦋0⦌ → T)
+    (hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (_ : X.Edge x₀ x₁), f x₀ = f x₁) (x : X _⦋0⦌) :
+    lift f hf (.mk x) = f x :=
+  rfl
+
+end π₀
+
+/-- The map `π₀ X → π₀ Y` induced by a morphism `X ⟶ Y` of simplicial sets. -/
+def mapπ₀ (f : X ⟶ Y) : π₀ X → π₀ Y :=
+  π₀.lift (π₀.mk ∘ f.app _) (fun _ _ e ↦ π₀.sound (e.map f))
+
+@[simp]
+lemma mapπ₀_mk (f : X ⟶ Y) (x₀ : X _⦋0⦌) :
+    mapπ₀ f (π₀.mk x₀) = π₀.mk (f.app _ x₀) :=
+  rfl
+
+@[simp]
+lemma mapπ₀_id_apply (x : π₀ X) : mapπ₀ (𝟙 X) x = x := by
+  induction x
+  simp
+
+@[simp]
+lemma mapπ₀_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (x : π₀ X) :
+    mapπ₀ (f ≫ g) x = mapπ₀ g (mapπ₀ f x) := by
+  induction x
+  simp
+
+/-- The functor which sends a simplicial set to the type of its connected components. -/
+@[simps]
+def π₀Functor : SSet.{u} ⥤ Type u where
+  obj X := π₀ X
+  map f := mapπ₀ f
+
+variable (X)
+
+/-- A simplicial set is preconnected when it has at most one connected component. -/
+protected abbrev IsPreconnected : Prop := Subsingleton (π₀ X)
+
+/-- A simplicial set is econnected when it has exactly one connected component. -/
+protected class IsConnected : Prop extends SSet.IsPreconnected X where
+  nonempty : X.Nonempty := by infer_instance
+
+attribute [instance] IsConnected.nonempty
+
+end SSet

Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean

@@ -159,6 +159,21 @@ lemma mem_ofSimplex_obj_iff {n : ℕ} (x : X _⦋n⦌) {m : SimplexCategoryᵒ
   dsimp [ofSimplex, Subfunctor.ofSection]
   aesop
 
+lemma ofSimplex_map_le {X : SSet.{u}} {n m : ℕ} (f : ⦋n⦌ ⟶ ⦋m⦌)
+    (x : X _⦋m⦌) :
+    ofSimplex (X.map f.op x) ≤ ofSimplex x := by
+  simp only [Subfunctor.ofSection_le_iff]
+  exact ⟨f.op, by simp⟩
+
+@[simp]
+lemma ofSimplex_map_of_epi {X : SSet.{u}} {n m : ℕ} (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f]
+    (x : X _⦋m⦌) :
+    ofSimplex (X.map f.op x) = ofSimplex x := by
+  refine le_antisymm (ofSimplex_map_le f x) ?_
+  simp only [Subfunctor.ofSection_le_iff]
+  have := isSplitEpi_of_epi f
+  exact ⟨(section_ f).op, by simp [← FunctorToTypes.map_comp_apply, ← op_comp]⟩
+
 section
 
 variable (f : X ⟶ Y)
@@ -239,6 +254,13 @@ lemma preimage_iSup {ι : Type*} (A : ι → X.Subcomplex) (p : Y ⟶ X) :
 lemma preimage_iInf {ι : Type*} (A : ι → X.Subcomplex) (p : Y ⟶ X) :
     (⨅ i, A i).preimage p = ⨅ i, (A i).preimage p := by aesop
 
+lemma preimage_comp {Z : SSet.{u}} (A : Z.Subcomplex) (f : X ⟶ Y) (g : Y ⟶ Z) :
+    A.preimage (f ≫ g) = (A.preimage g).preimage f := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma preimage_ι (A : X.Subcomplex) : A.preimage A.ι = ⊤ := by aesop
+
 end
 
 section

Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexEvaluation.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
+public import Mathlib.CategoryTheory.Limits.Preorder
+public import Mathlib.CategoryTheory.Limits.Set
+
+/-!
+# The evaluation functor on subcomplexes
+
+We define an evaluation functor `SSet.Subcomplex.evaluation : X.Subcomplex ⥤ Set (X.obj j)`
+when `X : SSet` and `j : SimplexCategoryᵒᵖ`. We use it to show that the functor
+`Subcomplex.toSSetFunctor : X.Subcomplex ⥤ SSet` preserves filtered colimits.
+
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory Limits
+
+namespace SSet.Subcomplex
+
+/-- The evaluation functor `X.Subcomplex ⥤ Set (X.obj j)` when `X : SSet`
+and `j : SimplexCategoryᵒᵖ`. -/
+@[simps]
+def evaluation (X : SSet.{u}) (j : SimplexCategoryᵒᵖ) :
+    X.Subcomplex ⥤ Set (X.obj j) where
+  obj A := A.obj j
+  map f := CategoryTheory.homOfLE (leOfHom f j)
+
+instance {J : Type*} [Category* J] {X : SSet.{u}} [IsFilteredOrEmpty J] :
+    PreservesColimitsOfShape J (Subcomplex.toSSetFunctor (X := X)) where
+  preservesColimit {F} :=
+    preservesColimit_of_preserves_colimit_cocone
+      (Preorder.colimitCoconeOfIsLUB F isLUB_iSup).isColimit
+        (evaluationJointlyReflectsColimits _ (fun j ↦ IsColimit.ofIsoColimit
+          (isColimitOfPreserves Set.functorToTypes
+              ((Preorder.colimitCoconeOfIsLUB (F ⋙ evaluation _ j) isLUB_iSup).isColimit))
+                (Cocone.ext (Set.functorToTypes.mapIso
+                  (CategoryTheory.eqToIso (by cat_disch))))))
+
+end SSet.Subcomplex