Simplicial sets #

A simplicial set is just a simplicial object in Type, i.e. a Type-valued presheaf on the simplex category.

(One might be tempted to call these "simplicial types" when working in type-theoretic foundations, but this would be unnecessarily confusing given the existing notion of a simplicial type in homotopy type theory.)

We define the standard simplices Δ[n] as simplicial sets, and their boundaries ∂Δ[n] and horns Λ[n, i]. (The notations are available via 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 :
Type (u + 1)

The category of simplicial sets. This is the category of contravariant functors from SimplexCategory to Type u.

Equations
Instances For
Equations
Equations
Equations
theorem SSet.hom_ext {X : SSet} {Y : SSet} {f : X Y} {g : X Y} (w : ∀ (n : ), f.app n = g.app n) :
f = g

The ulift functor SSet.{u} ⥤ SSet.{max u v} on simplicial sets.

Equations
Instances For

The n-th standard simplex Δ[n] associated with a nonempty finite linear order n is the Yoneda embedding of n.

Equations
Instances For

The n-th standard simplex Δ[n] associated with a nonempty finite linear order n is the Yoneda embedding of n.

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

Pretty printer defined by notation3 command.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
def SSet.standardSimplex.objEquiv (n : SimplexCategory) (m : ) :
( n).obj m (m.unop n)

Simplices of the standard simplex identify to morphisms in SimplexCategory.

Equations
• = Equiv.ulift
Instances For
@[inline, reducible]
abbrev SSet.standardSimplex.objMk {n : SimplexCategory} {m : } (f : Fin (SimplexCategory.len m.unop + 1) →o Fin ()) :
( n).obj m

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

Equations
Instances For
theorem SSet.standardSimplex.map_apply {m₁ : } {m₂ : } (f : m₁ m₂) {n : SimplexCategory} (x : ( n).obj m₁) :
( n).map f x = .symm (CategoryTheory.CategoryStruct.comp f.unop ( x))
def SSet.yonedaEquiv (X : SSet) (n : SimplexCategory) :
( n X) X.obj ()

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

Equations
Instances For
def SSet.standardSimplex.const (n : ) (k : Fin (n + 1)) (m : ) :
().obj m

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

Equations
Instances For
@[simp]
theorem SSet.standardSimplex.const_down_toOrderHom (n : ) (k : Fin (n + 1)) (m : ) :
def SSet.standardSimplex.edge (n : ) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) :
().obj

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

Equations
Instances For
theorem SSet.standardSimplex.coe_edge_down_toOrderHom (n : ) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) :
(SimplexCategory.Hom.toOrderHom ().down) = ![a, b]
def SSet.standardSimplex.triangle {n : } (a : Fin (n + 1)) (b : Fin (n + 1)) (c : Fin (n + 1)) (hab : a b) (hbc : b c) :
().obj

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

Equations
Instances For
theorem SSet.standardSimplex.coe_triangle_down_toOrderHom {n : } (a : Fin (n + 1)) (b : Fin (n + 1)) (c : Fin (n + 1)) (hab : a b) (hbc : b c) :
def SSet.asOrderHom {n : } {m : } (α : ().obj m) :
Fin (SimplexCategory.len m.unop + 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
Instances For

The boundary ∂Δ[n] of the n-th standard simplex consists of all m-simplices of standardSimplex n that are not surjective (when viewed as monotone function m → n).

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

Pretty printer defined by notation3 command.

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

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

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SSet.horn (n : ) (i : Fin (n + 1)) :

horn n i (or Λ[n, i]) is the i-th horn of the n-th standard simplex, where i : n. It consists of all m-simplices α of Δ[n] for which the union of {i} and the range of α is not all of n (when viewing α as monotone function m → n).

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

The i-th horn Λ[n, i] of the standard n-simplex

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

Pretty printer defined by notation3 command.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SSet.hornInclusion (n : ) (i : Fin (n + 1)) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem SSet.horn.const_coe (n : ) (i : Fin (n + 3)) (k : Fin (n + 3)) (m : ) :
def SSet.horn.const (n : ) (i : Fin (n + 3)) (k : Fin (n + 3)) (m : ) :
(SSet.horn (n + 2) i).obj m

The (degenerate) subsimplex of Λ[n+2, i] concentrated in vertex k.

Equations
Instances For
@[simp]
theorem SSet.horn.edge_coe (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : {i, a, b}.card n) :
(SSet.horn.edge n i a b hab H) =
def SSet.horn.edge (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : {i, a, b}.card n) :
().obj

The edge of Λ[n, i] with endpoints a and b.

This edge only exists if {i, a, b} has cardinality less than n.

Equations
Instances For
@[simp]
theorem SSet.horn.edge₃_coe_down (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : 3 n) :
((SSet.horn.edge₃ n i a b hab H)).down = SimplexCategory.Hom.mk { toFun := ![a, b], monotone' := }
def SSet.horn.edge₃ (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : 3 n) :
().obj

Alternative constructor for the edge of Λ[n, i] with endpoints a and b, assuming 3 ≤ n.

Equations
Instances For
@[simp]
theorem SSet.horn.primitiveEdge_coe_down {n : } {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < ) (j : Fin n) :
(()).down = SimplexCategory.Hom.mk { toFun := ![, ], monotone' := }
def SSet.horn.primitiveEdge {n : } {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < ) (j : Fin n) :
().obj

The edge of Λ[n, i] with endpoints j and j+1.

This constructor assumes 0 < i < n, which is the type of horn that occurs in the horn-filling condition of quasicategories.

Equations
Instances For
@[simp]
theorem SSet.horn.primitiveTriangle_coe {n : } (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ) (h : k < n + 2) :
(SSet.horn.primitiveTriangle i h₀ hₙ k h) = SSet.standardSimplex.triangle { val := k, isLt := } { val := k + 1, isLt := } { val := k + 2, isLt := }
def SSet.horn.primitiveTriangle {n : } (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ) (h : k < n + 2) :
(SSet.horn (n + 3) i).obj

The triangle in the standard simplex with vertices k, k+1, and k+2.

This constructor assumes 0 < i < n, which is the type of horn that occurs in the horn-filling condition of quasicategories.

Equations
Instances For
@[simp]
theorem SSet.horn.face_coe {n : } (i : Fin (n + 2)) (j : Fin (n + 2)) (h : j i) :
() = ().symm
def SSet.horn.face {n : } (i : Fin (n + 2)) (j : Fin (n + 2)) (h : j i) :
(SSet.horn (n + 1) i).obj

The jth subface of the i-th horn.

Equations
• = { val := ().symm , property := }
Instances For
theorem SSet.horn.hom_ext {n : } {i : Fin (n + 2)} {S : SSet} (σ₁ : SSet.horn (n + 1) i S) (σ₂ : SSet.horn (n + 1) i S) (h : ∀ (j : Fin (n + 2)) (h : j i), σ₁.app () = σ₂.app ()) :
σ₁ = σ₂

Two morphisms from a horn are equal if they are equal on all suitable faces.

noncomputable def SSet.S1 :

The simplicial circle.

Equations
Instances For
def SSet.Truncated (n : ) :
Type (u + 1)

Truncated simplicial sets.

Equations
Instances For
Equations
• = id inferInstance
instance SSet.Truncated.hasLimits {n : } :
Equations
• =
Equations
• =
theorem SSet.Truncated.hom_ext {n : } {X : } {Y : } {f : X Y} {g : X Y} (w : ∀ (n_1 : ), f.app n_1 = g.app n_1) :
f = g
def SSet.sk (n : ) :

The skeleton functor on simplicial sets.

Equations
Instances For
Equations
• SSet.instInhabitedTruncated = { default := ().obj () }
@[inline, reducible]
abbrev SSet.Augmented :
Type (u + 1)

The category of augmented simplicial sets, as a particular case of augmented simplicial objects.

Equations
Instances For
@[simp]
theorem SSet.Augmented.standardSimplex_obj_hom_app (Δ : SimplexCategory) (Δ' : ) :
∀ (a : ( ( Δ)).obj Δ'), ().hom.app Δ' a = CategoryTheory.Limits.terminal.from (( ( Δ)).obj Δ') a
@[simp]
theorem SSet.Augmented.standardSimplex_map_right :
∀ {X Y : SimplexCategory} (θ : X Y) (a : ((fun (Δ : SimplexCategory) => { left := Δ, right := , hom := { app := fun (Δ' : ) => CategoryTheory.Limits.terminal.from (( ( Δ)).obj Δ'), naturality := } }) X).right), ().right a = CategoryTheory.Limits.terminal.from ((fun (Δ : SimplexCategory) => { left := Δ, right := , hom := { app := fun (Δ' : ) => CategoryTheory.Limits.terminal.from (( ( Δ)).obj Δ'), naturality := } }) X).right a
@[simp]
theorem SSet.Augmented.standardSimplex_map_left :
∀ {X Y : SimplexCategory} (θ : X Y), ().left = θ

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.
Instances For