Discrete simplicial sets

The discrete simplicial set on a type ι is the constant simplicial set (Functor.const SimplexCategoryᵒᵖ).obj ι: its simplices in every dimension are the elements of ι, and all its faces and degeneracies are identities. It is the free simplicial set on the vertices ι: a map from it to a simplicial set X is a family ι → X _⦋0⦌ of vertices (SSet.constHomEquiv). Its only nondegenerate simplices are its vertices, so it has exactly as many nondegenerate simplices as ι has elements (SSet.constNEquiv). Discrete simplicial sets are therefore the test objects for statements about families of vertices that are phrased in terms of the number of nondegenerate simplices, such as cardinal filteredness.

Main declarations

• SSet.constHomEquiv: maps from the discrete simplicial set on ι are families of vertices.
• SSet.isIso_constHomEquiv_symm: a simplicial set whose simplices are all totally degenerate is the discrete simplicial set on its vertices.
• SSet.constNEquiv: the nondegenerate simplices of the discrete simplicial set on ι are the elements of ι.
• SSet.kanComplex_const: discrete simplicial sets are Kan complexes.
• SSet.toπ₀: the map from a simplicial set to the discrete simplicial set on its connected components.
• SSet.homConstEquiv: maps from X to the discrete simplicial set on ι are functions π₀ X → ι; they factor uniquely through SSet.toπ₀.

noncomputable def SSet.constHomEquiv (ι : Type u) {X : SSet} : ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι ⟶ X) ≃ (ι → X.obj (Opposite.op { len := 0 }))

Maps from the discrete simplicial set on ι to X are families of vertices of X indexed by ι; the map attached to a family sends i in every dimension to the degenerate simplex on the vertex at i. This is the adjunction between constant presheaves and evaluation at the terminal object ⦋0⦌ of SimplexCategory.

@[simp]

theorem SSet.constHomEquiv_apply (ι : Type u) {X : SSet} (f : (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι ⟶ X) (i : ι) : (constHomEquiv ι) f i = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) i

@[simp]

theorem SSet.constHomEquiv_symm_app_zero (ι : Type u) {X : SSet} (x : ι → X.obj (Opposite.op { len := 0 })) (i : ι) : (CategoryTheory.ConcreteCategory.hom (((constHomEquiv ι).symm x).app (Opposite.op { len := 0 }))) i = x i

The map from the discrete simplicial set given by a family of vertices sends the vertex i to the vertex at i. The source of the component is stated as ι, its simp-normal form.

theorem SSet.isIso_constHomEquiv_symm {ι : Type u} {X : SSet} {v : ι → X.obj (Opposite.op { len := 0 })} (hv : Function.Bijective v) (h : ∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (X.map ({ len := n }.const { len := 0 } 0).op))) : CategoryTheory.IsIso ((constHomEquiv ι).symm v)

A simplicial set all of whose simplices are totally degenerate is discrete: if every simplex of X is the degenerate simplex at a vertex, then the map from the discrete simplicial set on ι given by a bijection v : ι → X _⦋0⦌ is an isomorphism.

@[simp]

theorem SSet.const_degenerate_succ (ι : Type u) (n : ℕ) : degenerate ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι) (n + 1) = Set.univ

Every simplex of positive dimension of a discrete simplicial set is degenerate.

def SSet.constNEquiv (ι : Type u) : N ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι) ≃ ι

The nondegenerate simplices of the discrete simplicial set on ι are its vertices, the elements of ι.

instance SSet.kanComplex_const (ι : Type u) : KanComplex ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι)

Discrete simplicial sets are Kan complexes: the faces of a horn in a discrete simplicial set are all the same element, which is then a filler.

noncomputable def SSet.toπ₀ (X : SSet) : X ⟶ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj X.π₀

The map from a simplicial set to the discrete simplicial set on its connected components, sending a simplex to the component of its vertices.

theorem SSet.toπ₀_app {X : SSet} {n : SimplexCategoryᵒᵖ} (σ : X.obj n) : (CategoryTheory.ConcreteCategory.hom (X.toπ₀.app n)) σ = π₀.mk ((CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const (Opposite.unop n) 0).op)) σ)

The map to the discrete simplicial set on the connected components sends a simplex to the component of its initial vertex.

@[simp]

theorem SSet.toπ₀_app_zero {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : (CategoryTheory.ConcreteCategory.hom (X.toπ₀.app (Opposite.op { len := 0 }))) x = π₀.mk x

The map to the discrete simplicial set on the connected components sends a vertex to its component.

noncomputable def SSet.homConstEquiv (ι : Type u) (X : SSet) : (X ⟶ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι) ≃ (X.π₀ → ι)

Maps from a simplicial set X to the discrete simplicial set on ι are functions on the connected components of X: such a map is constant on each component, and the map attached to a function π₀ X → ι factors through toπ₀ X.

@[simp]

theorem SSet.homConstEquiv_apply_mk (ι : Type u) {X : SSet} (f : X ⟶ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι) (x : X.obj (Opposite.op { len := 0 })) : (homConstEquiv ι X) f (π₀.mk x) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x

The function on connected components attached to a map to a discrete simplicial set takes the component of a vertex to the image of that vertex.

theorem SSet.homConstEquiv_symm_apply (ι : Type u) {X : SSet} (g : X.π₀ → ι) : (homConstEquiv ι X).symm g = CategoryTheory.CategoryStruct.comp X.toπ₀ ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).map (TypeCat.ofHom g))

The map attached to a function on connected components is its composite with toπ₀ X.

@[simp]

theorem SSet.toπ₀_comp_homConstEquiv (ι : Type u) {X : SSet} (f : X ⟶ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι) : CategoryTheory.CategoryStruct.comp X.toπ₀ ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).map (TypeCat.ofHom ((homConstEquiv ι X) f))) = f

Every map from X to a discrete simplicial set factors through toπ₀ X.

@[simp]

theorem SSet.toπ₀_comp_homConstEquiv_assoc (ι : Type u) {X : SSet} (f : X ⟶ (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι) {Z : SSet} (h : (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).obj ι ⟶ Z) : CategoryTheory.CategoryStruct.comp X.toπ₀ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).map (TypeCat.ofHom ((homConstEquiv ι X) f))) h) = CategoryTheory.CategoryStruct.comp f h

Every map from X to a discrete simplicial set factors through toπ₀ X.

theorem SSet.eq_of_toπ₀_comp_eq (ι : Type u) {X : SSet} {g g' : X.π₀ → ι} (h : CategoryTheory.CategoryStruct.comp X.toπ₀ ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).map (TypeCat.ofHom g)) = CategoryTheory.CategoryStruct.comp X.toπ₀ ((CategoryTheory.Functor.const SimplexCategoryᵒᵖ).map (TypeCat.ofHom g'))) : g = g'

Factorizations through toπ₀ X are unique.