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 { len := 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 { len := 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.

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

instance SSet.instHasDimensionLTToSSetBoundary {n : ℕ} : (boundary n).toSSet.HasDimensionLT n

theorem SSet.face_singleton_compl_le_boundary {n : ℕ} (i : Fin (n + 1)) : stdSimplex.face {i}ᶜ ≤ boundary n

theorem SSet.stdSimplex.notMem_boundary (n : ℕ) : objMk OrderHom.id ∉ (boundary n).obj (Opposite.op { len := n })

theorem SSet.boundary_lt_top (n : ℕ) : boundary n < ⊤

theorem SSet.boundary_obj_eq_univ (m n : ℕ) (h : m < n := by lia) : (boundary n).obj (Opposite.op { len := m }) = Set.univ

theorem SSet.stdSimplex.subcomplex_hasDimensionLT_of_neq_top {n : ℕ} (A : (stdSimplex.obj { len := n }).Subcomplex) (h : A ≠ ⊤) : A.toSSet.HasDimensionLT n

theorem SSet.stdSimplex.le_boundary_iff {n : ℕ} (A : (stdSimplex.obj { len := n }).Subcomplex) : A ≤ boundary n ↔ A ≠ ⊤