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

• SSet = CategoryTheory.SimplicialObject (Type u)

instance SSet.largeCategory : CategoryTheory.LargeCategory SSet

Equations

• SSet.largeCategory = id inferInstance

instance SSet.hasLimits : CategoryTheory.Limits.HasLimits SSet

Equations

• SSet.hasLimits = (_ : CategoryTheory.Limits.HasLimits SSet)

instance SSet.hasColimits : CategoryTheory.Limits.HasColimits SSet

Equations

• SSet.hasColimits = (_ : CategoryTheory.Limits.HasColimits SSet)

theorem SSet.hom_ext {X : SSet} {Y : SSet} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g

def SSet.uliftFunctor : CategoryTheory.Functor SSet SSet

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

Equations

• SSet.uliftFunctor = (CategoryTheory.SimplicialObject.whiskering (Type u) (Type (max u v))).toPrefunctor.obj CategoryTheory.uliftFunctor.{v, u}

def SSet.standardSimplex : CategoryTheory.Functor SimplexCategory SSet

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

Equations

• SSet.standardSimplex = CategoryTheory.Functor.comp CategoryTheory.yoneda SSet.uliftFunctor

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

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.

def Simplicial.«termΔ[_]».delab : 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.instInhabitedSSet : Inhabited SSet

Equations

• SSet.instInhabitedSSet = { default := SSet.standardSimplex.toPrefunctor.obj (SimplexCategory.mk 0) }

@[simp]

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

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

Simplices of the standard simplex identify to morphisms in SimplexCategory.

Equations

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

@[inline, reducible]

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

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

Equations

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

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

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

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

Equations

• SSet.yonedaEquiv X n = CategoryTheory.yonedaCompUliftFunctorEquiv X n

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

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

Equations

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

@[simp]

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

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

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

Equations

• SSet.standardSimplex.edge n a b hab = SSet.standardSimplex.objMk { toFun := ![a, b], monotone' := (_ : Monotone ![a, b]) }

theorem SSet.standardSimplex.coe_edge_down_toOrderHom (n : ℕ) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a ≤ b) : ⇑(SimplexCategory.Hom.toOrderHom (SSet.standardSimplex.edge n a b hab).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) : (SSet.standardSimplex.toPrefunctor.obj (SimplexCategory.mk n)).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 2))

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

Equations

• SSet.standardSimplex.triangle a b c hab hbc = SSet.standardSimplex.objMk { toFun := ![a, b, c], monotone' := (_ : Monotone ![a, b, c]) }

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) : ⇑(SimplexCategory.Hom.toOrderHom (SSet.standardSimplex.triangle a b c hab hbc).down) = ![a, b, c]

def SSet.asOrderHom {n : ℕ} {m : SimplexCategoryᵒᵖ} (α : (SSet.standardSimplex.toPrefunctor.obj (SimplexCategory.mk n)).toPrefunctor.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

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

def SSet.boundary (n : ℕ) : SSet

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.

def Simplicial.«term∂Δ[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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

Equations

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

def SSet.boundaryInclusion (n : ℕ) : SSet.boundary n ⟶ SSet.standardSimplex.toPrefunctor.obj (SimplexCategory.mk n)

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.

def SSet.horn (n : ℕ) (i : Fin (n + 1)) : SSet

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.

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

Equations

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

def Simplicial.«termΛ[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def SSet.hornInclusion (n : ℕ) (i : Fin (n + 1)) : SSet.horn n i ⟶ SSet.standardSimplex.toPrefunctor.obj (SimplexCategory.mk n)

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.

@[simp]

theorem SSet.horn.const_coe (n : ℕ) (i : Fin (n + 3)) (k : Fin (n + 3)) (m : SimplexCategoryᵒᵖ) : ↑(SSet.horn.const n i k m) = SSet.standardSimplex.const (n + 2) k m

def SSet.horn.const (n : ℕ) (i : Fin (n + 3)) (k : Fin (n + 3)) (m : SimplexCategoryᵒᵖ) : (SSet.horn (n + 2) i).toPrefunctor.obj m

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

Equations

• SSet.horn.const n i k m = { val := SSet.standardSimplex.const (n + 2) k m, property := (_ : Set.range ⇑(SSet.asOrderHom (SSet.standardSimplex.const (n + 2) k m)) ∪ {i} ≠ Set.univ) }

@[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) = SSet.standardSimplex.edge n a b hab

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) : (SSet.horn n i).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 1))

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

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

Equations

• SSet.horn.edge n i a b hab H = { val := SSet.standardSimplex.edge n a b hab, property := (_ : Set.range ⇑(SSet.asOrderHom (SSet.standardSimplex.edge n a b hab)) ∪ {i} ≠ Set.univ) }

@[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' := (_ : Monotone ![a, b]) }

def SSet.horn.edge₃ (n : ℕ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a ≤ b) (H : 3 ≤ n) : (SSet.horn n i).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 1))

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

Equations

• SSet.horn.edge₃ n i a b hab H = SSet.horn.edge n i a b hab (_ : {i, a, b}.card ≤ n)

@[simp]

theorem SSet.horn.primitiveEdge_coe_down {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) : (↑(SSet.horn.primitiveEdge h₀ hₙ j)).down = SimplexCategory.Hom.mk { toFun := ![Fin.castSucc j, Fin.succ j], monotone' := (_ : Monotone ![Fin.castSucc j, Fin.succ j]) }

def SSet.horn.primitiveEdge {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) : (SSet.horn n i).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 1))

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

• SSet.horn.primitiveEdge h₀ hₙ j = SSet.horn.edge n i (Fin.castSucc j) (Fin.succ j) (_ : Fin.castSucc j ≤ Fin.succ j) (_ : {i, Fin.castSucc j, Fin.succ j}.card ≤ n)

@[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 := (_ : k < n + 3 + 1) } { val := k + 1, isLt := (_ : k + 1 < n + 3 + 1) } { val := k + 2, isLt := (_ : k + 2 < n + 3 + 1) } (_ : { val := k, isLt := (_ : k < n + 3 + 1) } ≤ { val := k + 1, isLt := (_ : k + 1 < n + 3 + 1) }) (_ : { val := k + 1, isLt := (_ : k + 1 < n + 3 + 1) } ≤ { val := k + 2, isLt := (_ : k + 2 < n + 3 + 1) })

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).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 2))

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

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

@[simp]

theorem SSet.horn.face_coe {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 2)) (h : j ≠ i) : ↑(SSet.horn.face i j h) = (SSet.standardSimplex.objEquiv (SimplexCategory.mk (n + 1)) (Opposite.op (SimplexCategory.mk n))).symm (SimplexCategory.δ j)

def SSet.horn.face {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 2)) (h : j ≠ i) : (SSet.horn (n + 1) i).toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))

The jth subface of the i-th horn.

Equations

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

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 (Opposite.op (SimplexCategory.mk n)) (SSet.horn.face i j h) = σ₂.app (Opposite.op (SimplexCategory.mk n)) (SSet.horn.face i j h)) : σ₁ = σ₂

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

noncomputable def SSet.S1 : SSet

The simplicial circle.

Equations

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

def SSet.Truncated (n : ℕ) : Type (u + 1)

Truncated simplicial sets.

Equations

• SSet.Truncated n = CategoryTheory.SimplicialObject.Truncated (Type u) n

instance SSet.Truncated.largeCategory (n : ℕ) : CategoryTheory.LargeCategory (SSet.Truncated n)

Equations

• SSet.Truncated.largeCategory n = id inferInstance

instance SSet.Truncated.hasLimits {n : ℕ} : CategoryTheory.Limits.HasLimits (SSet.Truncated n)

Equations

• (_ : CategoryTheory.Limits.HasLimits (SSet.Truncated n)) = (_ : CategoryTheory.Limits.HasLimits (SSet.Truncated n))

instance SSet.Truncated.hasColimits {n : ℕ} : CategoryTheory.Limits.HasColimits (SSet.Truncated n)

Equations

• (_ : CategoryTheory.Limits.HasColimits (SSet.Truncated n)) = (_ : CategoryTheory.Limits.HasColimits (SSet.Truncated n))

theorem SSet.Truncated.hom_ext {n : ℕ} {X : SSet.Truncated n} {Y : SSet.Truncated n} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ (n_1 : (SimplexCategory.Truncated n)ᵒᵖ), f.app n_1 = g.app n_1) : f = g

def SSet.sk (n : ℕ) : CategoryTheory.Functor SSet (SSet.Truncated n)

The skeleton functor on simplicial sets.

Equations

• SSet.sk n = CategoryTheory.SimplicialObject.sk n

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

Equations

• SSet.instInhabitedTruncated = { default := (SSet.sk n).toPrefunctor.obj (SSet.standardSimplex.toPrefunctor.obj (SimplexCategory.mk 0)) }

@[inline, reducible]

abbrev SSet.Augmented : Type (u + 1)

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

Equations

• SSet.Augmented = CategoryTheory.SimplicialObject.Augmented (Type u)

@[simp]

theorem SSet.Augmented.standardSimplex_obj_hom_app (Δ : SimplexCategory) (Δ' : SimplexCategoryᵒᵖ) : ∀ (a : ((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).toPrefunctor.obj (SSet.standardSimplex.toPrefunctor.obj Δ)).toPrefunctor.obj Δ'), (SSet.Augmented.standardSimplex.toPrefunctor.obj Δ).hom.app Δ' a = CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).toPrefunctor.obj (SSet.standardSimplex.toPrefunctor.obj Δ)).toPrefunctor.obj Δ') a

@[simp]

theorem SSet.Augmented.standardSimplex_map_right : ∀ {X Y : SimplexCategory} (θ : X ⟶ Y) (a : ((fun (Δ : SimplexCategory) => { left := SSet.standardSimplex.toPrefunctor.obj Δ, right := ⊤_ Type u, hom := CategoryTheory.NatTrans.mk fun (Δ' : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).toPrefunctor.obj (SSet.standardSimplex.toPrefunctor.obj Δ)).toPrefunctor.obj Δ') }) X).right), (SSet.Augmented.standardSimplex.toPrefunctor.map θ).right a = CategoryTheory.Limits.terminal.from ((fun (Δ : SimplexCategory) => { left := SSet.standardSimplex.toPrefunctor.obj Δ, right := ⊤_ Type u, hom := CategoryTheory.NatTrans.mk fun (Δ' : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).toPrefunctor.obj (SSet.standardSimplex.toPrefunctor.obj Δ)).toPrefunctor.obj Δ') }) X).right a

@[simp]

theorem SSet.Augmented.standardSimplex_obj_left (Δ : SimplexCategory) : (SSet.Augmented.standardSimplex.toPrefunctor.obj Δ).left = SSet.standardSimplex.toPrefunctor.obj Δ

@[simp]

theorem SSet.Augmented.standardSimplex_map_left : ∀ {X Y : SimplexCategory} (θ : X ⟶ Y), (SSet.Augmented.standardSimplex.toPrefunctor.map θ).left = SSet.standardSimplex.toPrefunctor.map θ

@[simp]

theorem SSet.Augmented.standardSimplex_obj_right (Δ : SimplexCategory) : (SSet.Augmented.standardSimplex.toPrefunctor.obj Δ).right = ⊤_ Type u

noncomputable def SSet.Augmented.standardSimplex : CategoryTheory.Functor SimplexCategory SSet.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.