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.mem_boundary_iff_notMem_range {n d : ℕ} (s : (stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) : s ∈ (boundary n).obj (Opposite.op { len := d }) ↔ ∃ (j : Fin (n + 1)), j ∉ Set.range ⇑s

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

@[simp]

theorem SSet.boundary_zero : boundary 0 = ⊥

theorem SSet.op_boundary (n : ℕ) : (boundary n).op.preimage (stdSimplex.opIso { len := n }).inv = boundary n

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 ≠ ⊤

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

def SSet.boundary.faceι {n : ℕ} (i : Fin (n + 1)) : (stdSimplex.face {i}ᶜ).toSSet ⟶ (boundary n).toSSet

The inclusion of a face of ∂Δ[n].

Equations

• SSet.boundary.faceι i = SSet.Subcomplex.homOfLE ⋯

instance SSet.boundary.instMonoFaceι {n : ℕ} (i : Fin (n + 1)) : CategoryTheory.Mono (faceι i)

@[simp]

theorem SSet.boundary.faceι_ι {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (faceι i) (boundary (n + 1)).ι = (stdSimplex.face {i}ᶜ).ι

@[simp]

theorem SSet.boundary.faceι_ι_assoc {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : stdSimplex.obj { len := n + 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceι i) (CategoryTheory.CategoryStruct.comp (boundary (n + 1)).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.face {i}ᶜ).ι h

def SSet.boundary.ι {n : ℕ} (i : Fin (n + 2)) : stdSimplex.obj { len := n } ⟶ (boundary (n + 1)).toSSet

The morphism Δ[n] ⟶ ∂Δ[n + 1] corresponding to face the face i : Fin (n + 2).

Equations

• SSet.boundary.ι i = SSet.Subcomplex.lift (SSet.stdSimplex.map (SimplexCategory.δ i)) ⋯

@[simp]

theorem SSet.boundary.ι_ι {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (ι i) (boundary (n + 1)).ι = stdSimplex.δ i

@[simp]

theorem SSet.boundary.ι_ι_assoc {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : stdSimplex.obj { len := n + 1 } ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι i) (CategoryTheory.CategoryStruct.comp (boundary (n + 1)).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ i) h

@[simp]

theorem SSet.boundary.faceSingletonComplIso_inv_ι {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso i).inv (ι i) = faceι i

@[simp]

theorem SSet.boundary.faceSingletonComplIso_inv_ι_assoc {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : (boundary (n + 1)).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso i).inv (CategoryTheory.CategoryStruct.comp (ι i) h) = CategoryTheory.CategoryStruct.comp (faceι i) h

instance SSet.boundary.instMonoι {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.Mono (ι i)

instance SSet.boundary.instMonoδStdSimplex {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.Mono (stdSimplex.δ i)

theorem SSet.boundary.hom_ext {n : ℕ} {X : SSet} {f g : (boundary (n + 1)).toSSet ⟶ X} (h : ∀ (i : Fin (n + 2)), CategoryTheory.CategoryStruct.comp (ι i) f = CategoryTheory.CategoryStruct.comp (ι i) g) : f = g

theorem SSet.boundary.hom_ext₀ {X : SSet} {f g : (boundary 0).toSSet ⟶ X} : f = g

theorem SSet.boundary.hom_ext₀_iff {X : SSet} {f g : (boundary 0).toSSet ⟶ X} : f = g ↔ True