# mathlibdocumentation

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].

@[instance]
@[instance]
@[instance]
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
@[instance]
Equations
def sSet.as_preorder_hom {n : } {m : simplex_categoryᵒᵖ} (α : m) :
fin ((opposite.unop m).len + 1) →ₘ fin (n + 1)

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
def sSet.horn_inclusion (n : ) (i : fin (n + 1)) :

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

Equations
def sSet.S1  :

The simplicial circle.

Equations
@[instance]
def sSet.truncated (n : ) :
Type (u+1)

Truncated simplicial sets.

Equations
@[instance]
@[instance]
def sSet.sk (n : ) :

The skeleton functor on simplicial sets.

Equations
@[instance]
Equations
def Top.to_sSet  :

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

Equations
def sSet.to_Top  :

The geometric realization functor.

Equations

Geometric realization is left adjoint to the singular simplicial set construction.

Equations

The geometric realization of the representable simplicial sets agree with the usual topological simplices.

Equations