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_map {X✝ Y✝ : SSet} (f : X✝ ⟶ Y✝) : π₀Functor.map f = TypeCat.ofHom (mapπ₀ f)

@[simp]

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

@[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