The boundary of the standard simplex

We introduce the boundary ∂Δ[n] of the standard simplex Δ[n]. (These notations become available by doing 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.boundary (n : ℕ) : SSet

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

Equations

• One or more equations did not get rendered due to their size.

def Simplicial.«term∂Δ[_]» : Lean.ParserDescr

The boundary ∂Δ[n] of the n-th standard simplex

Equations

• One or more equations did not get rendered due to their size.

def Simplicial.«term∂Δ[_]».«delab_app.SSet.boundary» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SSet.boundaryInclusion (n : ℕ) : boundary n ⟶ stdSimplex.obj (SimplexCategory.mk n)

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

Equations

• One or more equations did not get rendered due to their size.