Any simplicial set is the colimit of its monogenous subcomplexes

Let X be a simplicial set. The definition SSet.isColimitCoconeN shows that X is the colimit of the monogenous subcomplexes of X (the index category of this colimit is the partially ordered type X.N of nondegenerate simplices of X).

def SSet.functorN (X : SSet) : CategoryTheory.Functor X.N SSet

If X : SSet, this is the functor X.N ⥤ SSet which sends a nondegenerate simplex of X to the subcomplex of X that it generates.

Equations

• X.functorN = ⋯.functor.comp SSet.Subcomplex.toSSetFunctor

@[simp]

theorem SSet.functorN_obj (X : SSet) (X✝ : X.N) : X.functorN.obj X✝ = X✝.subcomplex.toSSet

@[implicit_reducible]

def SSet.coconeN (X : SSet) : CategoryTheory.Limits.Cocone X.functorN

Given X : SSet, this is the (colimit) cocone consisting of the inclusions of the monogenous subcomplexes of X. (Note: a monogenous subcomplex of X is generated by a unique nondegenerate simplex x : X.N.)

Equations

• X.coconeN = { pt := X, ι := { app := fun (x : X.N) => (⋯.functor.obj x).ι, naturality := ⋯ } }

noncomputable def SSet.isColimitCoconeN (X : SSet) : CategoryTheory.Limits.IsColimit X.coconeN

If X : SSet, then X is the colimit of the its monogenous subcomplexes. (Note: a monogenous subcomplex of X is generated by a unique nondegenerate simplex x : X.N.)

Equations

• X.isColimitCoconeN = { desc := SSet.isColimitCoconeN.desc✝, fac := ⋯, uniq := ⋯ }