The splitting of a simplicial set

Let X be a simplicial set. The fact that any simplex x : X _⦋n⦌ can be written in a unique way as X.map f.op y for an epimorphism f : ⦋n⦌ ⟶ ⦋m⦌ and a nondegenerate simplex y : X _⦋m⦌ is translated in this file as the data of a splitting of X.

noncomputable def SSet.splitting (X : SSet) : CategoryTheory.SimplicialObject.Splitting X

The canonical splitting of a simplicial set that is given by the nondegenerate simplices.

Equations

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

@[simp]

theorem SSet.splitting_ι (X : SSet) (n : ℕ) : X.splitting.ι n = TypeCat.ofHom Subtype.val

@[simp]

theorem SSet.splitting_N (X : SSet) (n : ℕ) : X.splitting.N n = ↑(X.nonDegenerate n)