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 : ℕ) : (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

• SSet.boundary n = { obj := fun (x : SimplexCategoryᵒᵖ) => {s : (SSet.stdSimplex.obj (SimplexCategory.mk n)).obj x | ¬Function.Surjective ⇑(SSet.stdSimplex.asOrderHom s)}, map := ⋯ }

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.

theorem SSet.boundary_eq_iSup (n : ℕ) : boundary n = ⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ

@[reducible, inline, deprecated SSet.boundary (since := "2025-01-26")]

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

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

Equations

• SSet.boundaryInclusion n = (SSet.boundary n).ι