# Documentation

Mathlib.AlgebraicTopology.SimplicialSet

A simplicial set is just a simplicial object in Type, i.e. a Type-valued presheaf on the simplex category.

(One might be tempted to call these "simplicial types" when working in type-theoretic foundations, but this would be unnecessarily confusing given the existing notion of a simplicial type in homotopy type theory.)

We define the standard simplices Δ[n] as simplicial sets, and their boundaries ∂Δ[n] and horns Λ[n, i]. (The notations are available via Open Simplicial.)

## Future work #

There isn't yet a complete API for simplices, boundaries, and horns. As an example, we should have a function that constructs from a non-surjective order preserving function Fin n → Fin n a morphism Δ[n] ⟶ ∂Δ[n].

def SSet :
Type (u + 1)

The category of simplicial sets. This is the category of contravariant functors from SimplexCategory to Type u.

Instances For
theorem SSet.hom_ext {X : SSet} {Y : SSet} {f : X Y} {g : X Y} (w : ∀ (n : ), f.app n = g.app n) :
f = g

The n-th standard simplex Δ[n] associated with a nonempty finite linear order n is the Yoneda embedding of n.

Instances For
Instances For
def SSet.asOrderHom {n : } {m : } (α : ().obj m) :
Fin (SimplexCategory.len m.unop + 1) →o Fin (n + 1)

The m-simplices of the n-th standard simplex are the monotone maps from Fin (m+1) to Fin (n+1).

Instances For

The boundary ∂Δ[n] of the n-th standard simplex consists of all m-simplices of standardSimplex n that are not surjective (when viewed as monotone function m → n).

Instances For
Instances For

The inclusion of the boundary of the n-th standard simplex into that standard simplex.

Instances For
def SSet.horn (n : ) (i : Fin (n + 1)) :

horn n i (or Λ[n, i]) is the i-th horn of the n-th standard simplex, where i : n. It consists of all m-simplices α of Δ[n] for which the union of {i} and the range of α is not all of n (when viewing α as monotone function m → n).

Instances For
Instances For
def SSet.hornInclusion (n : ) (i : Fin (n + 1)) :

The inclusion of the i-th horn of the n-th standard simplex into that standard simplex.

Instances For
noncomputable def SSet.S1 :

The simplicial circle.

Instances For
def SSet.Truncated (n : ) :
Type (u + 1)

Truncated simplicial sets.

Instances For
theorem SSet.Truncated.hom_ext {n : } {X : } {Y : } {f : X Y} {g : X Y} (w : ∀ (n : ), f.app n = g.app n) :
f = g
def SSet.sk (n : ) :

The skeleton functor on simplicial sets.

Instances For
@[inline, reducible]
abbrev SSet.Augmented :
Type (u + 1)

The category of augmented simplicial sets, as a particular case of augmented simplicial objects.

Instances For
@[simp]
theorem SSet.Augmented.standardSimplex_map_left :
∀ {X Y : SimplexCategory} (θ : X Y), ().left = SSet.standardSimplex.map θ
@[simp]
theorem SSet.Augmented.standardSimplex_map_right :
∀ {X Y : SimplexCategory} (θ : X Y) (a : ((fun Δ => { left := SSet.standardSimplex.obj Δ, right := , hom := CategoryTheory.NatTrans.mk fun Δ' => CategoryTheory.Limits.terminal.from ((().obj (SSet.standardSimplex.obj Δ)).obj Δ') }) X).right), = CategoryTheory.Limits.terminal.from ((fun Δ => { left := SSet.standardSimplex.obj Δ, right := , hom := CategoryTheory.NatTrans.mk fun Δ' => CategoryTheory.Limits.terminal.from ((().obj (SSet.standardSimplex.obj Δ)).obj Δ') }) X).right a
@[simp]
theorem SSet.Augmented.standardSimplex_obj_hom_app (Δ : SimplexCategory) (Δ' : ) :
∀ (a : ().obj Δ'), ().hom.app Δ' a = CategoryTheory.Limits.terminal.from (().obj Δ') a

The functor which sends [n] to the simplicial set Δ[n] equipped by the obvious augmentation towards the terminal object of the category of sets.

Instances For
noncomputable def TopCat.toSSet :

The functor associating the singular simplicial set to a topological space.

Instances For
noncomputable def SSet.toTop :

The geometric realization functor.

Instances For