# mathlib3documentation

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

@[protected, instance]
@[protected, instance]
@[protected, 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
Instances for sSet

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

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

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
noncomputable def sSet.S1  :

The simplicial circle.

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

Truncated simplicial sets.

Equations
Instances for sSet.truncated
@[protected, instance]
@[protected, instance]
def sSet.sk (n : ) :

The skeleton functor on simplicial sets.

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

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

@[simp]
@[simp]
@[simp]
theorem sSet.augmented.standard_simplex_map_right (Δ₁ Δ₂ : simplex_category) (θ : Δ₁ Δ₂) (ᾰ : {left := , right := , hom := {app := λ (Δ' : simplex_categoryᵒᵖ), , naturality' := _}}.right) :
@[simp]
theorem sSet.augmented.standard_simplex_map_left (Δ₁ Δ₂ : simplex_category) (θ : Δ₁ Δ₂) :
noncomputable def sSet.augmented.standard_simplex  :

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
def Top.to_sSet  :

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

Equations
noncomputable def sSet.to_Top  :

The geometric realization functor.

Equations