The standard simplex

We define the standard simplices Δ[n] as simplicial sets. See files SimplicialSet.Boundary and SimplicialSet.Horn for their boundaries∂Δ[n] and horns Λ[n, i]. (The notations are available via open Simplicial.)

def SSet.stdSimplex : CategoryTheory.CosimplicialObject SSet

The functor SimplexCategory ⥤ SSet which sends SimplexCategory.mk n to the standard simplex Δ[n] is a cosimplicial object in the category of simplicial sets. (This functor is essentially given by the Yoneda embedding).

Equations

• SSet.stdSimplex = CategoryTheory.yoneda.comp SSet.uliftFunctor

@[deprecated SSet.stdSimplex (since := "2025-01-23")]

def SSet.standardSimplex : CategoryTheory.CosimplicialObject SSet

Alias of SSet.stdSimplex.

---

The functor SimplexCategory ⥤ SSet which sends SimplexCategory.mk n to the standard simplex Δ[n] is a cosimplicial object in the category of simplicial sets. (This functor is essentially given by the Yoneda embedding).

Equations

• SSet.standardSimplex = SSet.stdSimplex

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

The functor SimplexCategory ⥤ SSet which sends SimplexCategory.mk n to the standard simplex Δ[n] is a cosimplicial object in the category of simplicial sets. (This functor is essentially given by the Yoneda embedding).

Equations

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

def Simplicial.«termΔ[_]».«delab_app.Prefunctor.obj» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

instance SSet.instInhabited : Inhabited SSet

Equations

• SSet.instInhabited = { default := SSet.stdSimplex.obj (SimplexCategory.mk 0) }

instance SSet.instInhabitedTruncated {n : ℕ} : Inhabited (Truncated n)

Equations

• SSet.instInhabitedTruncated = { default := (SSet.truncation n).obj (SSet.stdSimplex.obj (SimplexCategory.mk 0)) }

@[simp]

theorem SSet.stdSimplex.map_id (n : SimplexCategory) : stdSimplex.map (SimplexCategory.Hom.mk OrderHom.id) = CategoryTheory.CategoryStruct.id (stdSimplex.obj n)

def SSet.stdSimplex.objEquiv (n : SimplexCategory) (m : SimplexCategoryᵒᵖ) : (stdSimplex.obj n).obj m ≃ (Opposite.unop m ⟶ n)

Simplices of the standard simplex identify to morphisms in SimplexCategory.

Equations

• SSet.stdSimplex.objEquiv n m = Equiv.ulift

@[reducible, inline]

abbrev SSet.stdSimplex.objMk {n : SimplexCategory} {m : SimplexCategoryᵒᵖ} (f : Fin ((Opposite.unop m).len + 1) →o Fin (n.len + 1)) : (stdSimplex.obj n).obj m

Constructor for simplices of the standard simplex which takes a OrderHom as an input.

Equations

• SSet.stdSimplex.objMk f = (SSet.stdSimplex.objEquiv n m).symm (SimplexCategory.Hom.mk f)

theorem SSet.stdSimplex.map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory} (x : (stdSimplex.obj n).obj m₁) : (stdSimplex.obj n).map f x = (objEquiv n m₂).symm (CategoryTheory.CategoryStruct.comp f.unop ((objEquiv n m₁) x))

def SSet.yonedaEquiv (X : SSet) (n : SimplexCategory) : (stdSimplex.obj n ⟶ X) ≃ X.obj (Opposite.op n)

The canonical bijection (stdSimplex.obj n ⟶ X) ≃ X.obj (op n).

Equations

• X.yonedaEquiv n = CategoryTheory.yonedaCompUliftFunctorEquiv X n

def SSet.stdSimplex.id (n : ℕ) : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk n))

The unique non-degenerate n-simplex in Δ[n].

Equations

• SSet.stdSimplex.id n = ((SSet.stdSimplex.obj (SimplexCategory.mk n)).yonedaEquiv (SimplexCategory.mk n)) (CategoryTheory.CategoryStruct.id (SSet.stdSimplex.obj (SimplexCategory.mk n)))

theorem SSet.stdSimplex.id_eq_objEquiv_symm (n : ℕ) : id n = (objEquiv (Opposite.unop (Opposite.op n)) (Opposite.op n)).symm (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op n)))

theorem SSet.stdSimplex.objEquiv_id (n : ℕ) : (objEquiv (SimplexCategory.mk n) (Opposite.op (SimplexCategory.mk n))) (id n) = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (SimplexCategory.mk n)))

def SSet.stdSimplex.const (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : (stdSimplex.obj (SimplexCategory.mk n)).obj m

The (degenerate) m-simplex in the standard simplex concentrated in vertex k.

Equations

• SSet.stdSimplex.const n k m = SSet.stdSimplex.objMk ((OrderHom.const (Fin ((Opposite.unop m).len + 1))) k)

@[simp]

theorem SSet.stdSimplex.const_down_toOrderHom (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : SimplexCategory.Hom.toOrderHom (const n k m).down = (OrderHom.const (Fin ((Opposite.unop m).len + 1))) k

def SSet.stdSimplex.edge (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk 1))

The edge of the standard simplex with endpoints a and b.

Equations

• SSet.stdSimplex.edge n a b hab = SSet.stdSimplex.objMk { toFun := ![a, b], monotone' := ⋯ }

theorem SSet.stdSimplex.coe_edge_down_toOrderHom (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : ⇑(SimplexCategory.Hom.toOrderHom (edge n a b hab).down) = ![a, b]

def SSet.stdSimplex.triangle {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) : (stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk 2))

The triangle in the standard simplex with vertices a, b, and c.

Equations

• SSet.stdSimplex.triangle a b c hab hbc = SSet.stdSimplex.objMk { toFun := ![a, b, c], monotone' := ⋯ }

theorem SSet.stdSimplex.coe_triangle_down_toOrderHom {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) : ⇑(SimplexCategory.Hom.toOrderHom (triangle a b c hab hbc).down) = ![a, b, c]

def SSet.asOrderHom {n : ℕ} {m : SimplexCategoryᵒᵖ} (α : (stdSimplex.obj (SimplexCategory.mk n)).obj m) : Fin ((Opposite.unop m).len + 1) →o Fin (n + 1)

The m-simplices of the n-th standard simplex are the monotone maps from Fin (m+1) to Fin (n+1).

Equations

• SSet.asOrderHom α = SimplexCategory.Hom.toOrderHom α.down

noncomputable def SSet.S1 : SSet

The simplicial circle.

Equations

• SSet.S1 = CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair (SSet.stdSimplex.δ 0) (SSet.stdSimplex.δ 1))

noncomputable def SSet.Augmented.stdSimplex : CategoryTheory.Functor SimplexCategory Augmented

The functor which sends ⦋n⦌ to the simplicial set Δ[n] equipped by the obvious augmentation towards the terminal object of the category of sets.

Equations

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

@[simp]

theorem SSet.Augmented.stdSimplex_obj_right (Δ : SimplexCategory) : (stdSimplex.obj Δ).right = ⊤_ Type u

@[simp]

theorem SSet.Augmented.stdSimplex_obj_hom_app (Δ : SimplexCategory) (x✝ : SimplexCategoryᵒᵖ) (a✝ : ((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x✝) : (stdSimplex.obj Δ).hom.app x✝ a✝ = CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x✝) a✝

@[simp]

theorem SSet.Augmented.stdSimplex_map_left {X✝ Y✝ : SimplexCategory} (θ : X✝ ⟶ Y✝) : (stdSimplex.map θ).left = SSet.stdSimplex.map θ

@[simp]

theorem SSet.Augmented.stdSimplex_map_right {X✝ Y✝ : SimplexCategory} (θ : X✝ ⟶ Y✝) (a✝ : ((fun (Δ : SimplexCategory) => { left := SSet.stdSimplex.obj Δ, right := ⊤_ Type u, hom := { app := fun (x : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x), naturality := ⋯ } }) X✝).right) : (stdSimplex.map θ).right a✝ = CategoryTheory.Limits.terminal.from ((fun (Δ : SimplexCategory) => { left := SSet.stdSimplex.obj Δ, right := ⊤_ Type u, hom := { app := fun (x : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.stdSimplex.obj Δ)).obj x), naturality := ⋯ } }) X✝).right a✝

@[simp]

theorem SSet.Augmented.stdSimplex_obj_left (Δ : SimplexCategory) : (stdSimplex.obj Δ).left = SSet.stdSimplex.obj Δ