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

source

def SSet.boundary (n : ℕ) :

(stdSimplex.obj (SimplexCategory.mk n)).Subcomplex

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

Instances For

source

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

Lean.ParserDescr

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

Equations

Instances For

source

def Simplicial.«term∂Δ[_]».«delab_app.SSet.boundary» :

Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.