mathlib3 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 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for sSet

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.sk (n : ) :

The skeleton functor on simplicial sets.

Equations
@[reducible]
def sSet.augmented  :
Type (u+1)

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

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

Equations

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

Equations
noncomputable def sSet.to_Top  :

The geometric realization functor.

Equations
noncomputable def sSet_Top_adj  :

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