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.

TODO

• Define the subcomplex of X corresponding to an element in π₀ X (@joelriou)
• Show π₀ X is a coequalizer of the two face maps X _⦋1⦌ → X _⦋0⦌ (@joelriou)
• Show π₀ X identifies to the colimit of X as a functor to types

References:

• Kerodon 00G5: Connected Components of Simplicial Sets

def SSet.π₀Rel {X : SSet} (x₀ x₁ : X.obj (Opposite.op { len := 0 })) : Prop

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₁.

Equations

• SSet.π₀Rel x₀ x₁ = Nonempty (SSet.Edge x₀ x₁)

@[irreducible]

def SSet.π₀ (X : SSet) : Type u

The type of connected components of a simplicial set.

Equations

• X.π₀ = Quot SSet.π₀Rel

def SSet.π₀.mk {X : SSet} : X.obj (Opposite.op { len := 0 }) → X.π₀

The connected component of a 0-simplex of a simplicial set.

Equations

• SSet.π₀.mk = Quot.mk SSet.π₀Rel

theorem SSet.π₀.mk_surjective {X : SSet} : Function.Surjective mk

theorem SSet.π₀.sound {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : Edge x₀ x₁) : mk x₀ = mk x₁

theorem SSet.π₀.mk_eq_mk_iff {X : SSet} (x₀ x₁ : X.obj (Opposite.op { len := 0 })) : mk x₀ = mk x₁ ↔ Relation.EqvGen π₀Rel x₀ x₁

theorem SSet.π₀.rec {X : SSet} {motive : X.π₀ → Prop} (mk : ∀ (x : X.obj (Opposite.op { len := 0 })), motive (mk x)) (x : X.π₀) : motive x

def SSet.π₀.lift {X : SSet} {T : Type u_1} (f : X.obj (Opposite.op { len := 0 }) → T) (hf : ∀ ⦃x₀ x₁ : X.obj (Opposite.op { len := 0 })⦄ (x : Edge x₀ x₁), f x₀ = f x₁) : X.π₀ → T

Constructor for maps from the type of connected components of a simplicial set.

Equations

• SSet.π₀.lift f hf = Quot.lift f ⋯

@[simp]

theorem SSet.π₀.lift_mk {X : SSet} {T : Type u_1} (f : X.obj (Opposite.op { len := 0 }) → T) (hf : ∀ ⦃x₀ x₁ : X.obj (Opposite.op { len := 0 })⦄ (x : Edge x₀ x₁), f x₀ = f x₁) (x : X.obj (Opposite.op { len := 0 })) : lift f hf (mk x) = f x

def SSet.mapπ₀ {X Y : SSet} (f : X ⟶ Y) : X.π₀ → Y.π₀

The map π₀ X → π₀ Y induced by a morphism X ⟶ Y of simplicial sets.

Equations

• SSet.mapπ₀ f = SSet.π₀.lift (SSet.π₀.mk ∘ ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 })))) ⋯

@[simp]

theorem SSet.mapπ₀_mk {X Y : SSet} (f : X ⟶ Y) (x₀ : X.obj (Opposite.op { len := 0 })) : mapπ₀ f (π₀.mk x₀) = π₀.mk ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₀)

@[simp]

theorem SSet.mapπ₀_id_apply {X : SSet} (x : X.π₀) : mapπ₀ (CategoryTheory.CategoryStruct.id X) x = x

@[simp]

theorem SSet.mapπ₀_comp_apply {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X.π₀) : mapπ₀ (CategoryTheory.CategoryStruct.comp f g) x = mapπ₀ g (mapπ₀ f x)

def SSet.π₀Functor : CategoryTheory.Functor SSet (Type u)

The functor which sends a simplicial set to the type of its connected components.

Equations

• SSet.π₀Functor = { obj := fun (X : SSet) => X.π₀, map := fun {X Y : SSet} (f : X ⟶ Y) => TypeCat.ofHom (SSet.mapπ₀ f), map_id := SSet.π₀Functor._proof_2, map_comp := @SSet.π₀Functor._proof_4 }

@[simp]

theorem SSet.π₀Functor_obj (X : SSet) : π₀Functor.obj X = X.π₀

@[simp]

theorem SSet.π₀Functor_map {X✝ Y✝ : SSet} (f : X✝ ⟶ Y✝) : π₀Functor.map f = TypeCat.ofHom (mapπ₀ f)

def SSet.toπ₀NatTrans : SSet.evaluation.obj (Opposite.op { len := 0 }) ⟶ π₀Functor

The map π₀.mk : X _⦋0⦌ ⟶ π₀ X for all simplicial sets X, as a natural transformation.

Equations

• SSet.toπ₀NatTrans = { app := fun (X : SSet) => TypeCat.ofHom SSet.π₀.mk, naturality := SSet.toπ₀NatTrans._proof_1 }

@[reducible, inline]

abbrev SSet.coforkπ₀ {X : SSet} : CategoryTheory.Limits.Cofork (CategoryTheory.SimplicialObject.δ X 1) (CategoryTheory.SimplicialObject.δ X 0)

The (colimit) cofork expressing π₀ X as a coequalizer of X.δ 0 : X _⦋1⦌ → X _⦋0⦌ and X.δ 1.

Equations

• SSet.coforkπ₀ = CategoryTheory.Limits.Cofork.ofπ (TypeCat.ofHom SSet.π₀.mk) ⋯

def SSet.isColimitCoforkπ₀ {X : SSet} : CategoryTheory.Limits.IsColimit coforkπ₀

If X is a simplicial set, £₀ X is a coequalizer of X.δ 0 : X _⦋1⦌ → X _⦋0⦌ and X.δ 1.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev SSet.coforkπ₀Functor : CategoryTheory.Limits.Cofork (SSet.evaluation.map (SimplexCategory.δ 1).op) (SSet.evaluation.map (SimplexCategory.δ 0).op)

The colimit cofork exhibiting the natural transformation toπ₀NatTrans : SSet.evaluation.obj (op ⦋0⦌) ⟶ π₀Functor as a coequalizer of the two face maps, considered as natural transformations of functors SSet.{u} ⥤ Type u.

Equations

• SSet.coforkπ₀Functor = CategoryTheory.Limits.Cofork.ofπ SSet.toπ₀NatTrans SSet.coforkπ₀Functor._proof_1

def SSet.isColimitCoforkπ₀Functor : CategoryTheory.Limits.IsColimit coforkπ₀Functor

The functor π₀Functor : SSet.{u} ⥤ Type u is the coequalizer of the two face maps δ (0 : Fin 2) and δ 1, considered as natural transformations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.π₀.nonempty_iff (X : SSet) : Nonempty X.π₀ ↔ X.Nonempty

@[reducible, inline]

abbrev SSet.IsPreconnected (X : SSet) : Prop

A simplicial set is preconnected when it has at most one connected component.

Equations

• X.IsPreconnected = Subsingleton X.π₀

class SSet.IsConnected (X : SSet) extends Subsingleton X.π₀ : Prop

A simplicial set is econnected when it has exactly one connected component.

• allEq (a b : X.π₀) : a = b
• nonempty : X.Nonempty

instance SSet.instNonemptyπ₀OfIsConnected (X : SSet) [X.IsConnected] : Nonempty X.π₀

theorem SSet.isConnected_iff (X : SSet) : X.IsConnected ↔ X.IsPreconnected ∧ X.Nonempty

theorem SSet.isConnected_iff_nonempty_unique (X : SSet) : X.IsConnected ↔ Nonempty (Unique X.π₀)