mathlib documentation

algebraic_topology.simplicial_set

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_locale 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 simplex_category to Type u.

Equations

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

Equations

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

Equations
def sSet.boundary (n : ) :

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

Equations

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

Equations
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).

Equations

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

Equations
def sSet.truncated (n : ) :
Type (u+1)

Truncated simplicial sets.

Equations
def sSet.sk (n : ) :

The skeleton functor on simplicial sets.

Equations