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.3)

instance SSet.largeCategory : CategoryTheory.LargeCategory SSet

Equations

• SSet.largeCategory = id inferInstance

instance SSet.hasLimits : CategoryTheory.Limits.HasLimits SSet

Equations

• SSet.hasLimits = ⋯

instance SSet.hasColimits : CategoryTheory.Limits.HasColimits SSet

Equations

• SSet.hasColimits = ⋯

theorem SSet.hom_ext {X Y : SSet} {f 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.7) (Type (max ?u.7 ?u.8))).obj CategoryTheory.uliftFunctor.{?u.8, ?u.7}

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.yoneda.comp SSet.uliftFunctor

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

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.

instance SSet.instInhabited : Inhabited SSet

Equations

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

@[simp]

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

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

Simplices of the standard simplex identify to morphisms in SimplexCategory.

Equations

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

@[reducible, inline]

abbrev SSet.standardSimplex.objMk {n : SimplexCategory} {m : SimplexCategoryᵒᵖ} (f : Fin ((Opposite.unop m).len + 1) →o Fin (n.len + 1)) : (SSet.standardSimplex.obj n).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₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory} (x : (SSet.standardSimplex.obj n).obj m₁) : (SSet.standardSimplex.obj n).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.obj n ⟶ X) ≃ X.obj (Opposite.op n)

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

Equations

• X.yonedaEquiv n = CategoryTheory.yonedaCompUliftFunctorEquiv X n

def SSet.standardSimplex.const (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) : (SSet.standardSimplex.obj (SimplexCategory.mk n)).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 ((Opposite.unop m).len + 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 ((Opposite.unop m).len + 1))) k

def SSet.standardSimplex.edge (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : (SSet.standardSimplex.obj (SimplexCategory.mk n)).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' := ⋯ }

theorem SSet.standardSimplex.coe_edge_down_toOrderHom (n : ℕ) (a 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 b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) : (SSet.standardSimplex.obj (SimplexCategory.mk n)).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' := ⋯ }

theorem SSet.standardSimplex.coe_triangle_down_toOrderHom {n : ℕ} (a b 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.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

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∂Δ[_]» : Lean.ParserDescr

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

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.boundaryInclusion (n : ℕ) : SSet.boundary n ⟶ SSet.standardSimplex.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

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

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

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

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

Equations

• SSet.horn.const n i k m = ⟨SSet.standardSimplex.const (n + 2) k m, ⋯⟩

@[simp]

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

def SSet.horn.edge (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : {i, a, b}.card ≤ n) : (SSet.horn n i).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 = ⟨SSet.standardSimplex.edge n a b hab, ⋯⟩

@[simp]

theorem SSet.horn.edge_coe (n : ℕ) (i a 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 a b : Fin (n + 1)) (hab : a ≤ b) (H : 3 ≤ n) : (SSet.horn n i).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 ⋯

@[simp]

theorem SSet.horn.edge₃_coe_down (n : ℕ) (i a 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.primitiveEdge {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) : (SSet.horn n i).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 j.castSucc j.succ ⋯ ⋯

@[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 := ![j.castSucc, j.succ], monotone' := ⋯ }

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 (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

• SSet.horn.primitiveTriangle i h₀ hₙ k h = ⟨SSet.standardSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯, ⋯⟩

@[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 ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯

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

The jth subface of the i-th horn.

Equations

• SSet.horn.face i j h = ⟨(SSet.standardSimplex.objEquiv (SimplexCategory.mk (n + 1)) (Opposite.op (SimplexCategory.mk n))).symm (SimplexCategory.δ j), ⋯⟩

@[simp]

theorem SSet.horn.face_coe {n : ℕ} (i 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)

theorem SSet.horn.hom_ext {n : ℕ} {i : Fin (n + 2)} {S : SSet} (σ₁ σ₂ : 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

• SSet.S1 = CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair (SSet.standardSimplex.map (SimplexCategory.δ 0)) (SSet.standardSimplex.map (SimplexCategory.δ 1)))

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

Truncated simplicial sets.

Equations

• SSet.Truncated n = CategoryTheory.SimplicialObject.Truncated (Type ?u.10) 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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def SSet.Truncated.uliftFunctor (k : ℕ) : CategoryTheory.Functor (SSet.Truncated k) (SSet.Truncated k)

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

Equations

• SSet.Truncated.uliftFunctor k = (CategoryTheory.whiskeringRight (SimplexCategory.Truncated k)ᵒᵖ (Type ?u.16) (Type (max ?u.16 ?u.17))).obj CategoryTheory.uliftFunctor.{?u.17, ?u.16}

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

@[reducible, inline]

abbrev SSet.truncation (n : ℕ) : CategoryTheory.Functor SSet (SSet.Truncated n)

The truncation functor on simplicial sets.

Equations

• SSet.truncation n = CategoryTheory.SimplicialObject.truncation n

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

Equations

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

@[reducible, inline]

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

The n-skeleton as a functor SSet.Truncated n ⥤ SSet.

Equations

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

@[reducible, inline]

abbrev SSet.Truncated.cosk (n : ℕ) : CategoryTheory.Functor (SSet.Truncated n) SSet

The n-coskeleton as a functor SSet.Truncated n ⥤ SSet.

Equations

• SSet.Truncated.cosk n = CategoryTheory.SimplicialObject.Truncated.cosk n

@[reducible, inline]

abbrev SSet.sk (n : ℕ) : CategoryTheory.Functor SSet SSet

The n-skeleton as an endofunctor on SSet.

Equations

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

@[reducible, inline]

abbrev SSet.cosk (n : ℕ) : CategoryTheory.Functor SSet SSet

The n-coskeleton as an endofunctor on SSet.

Equations

• SSet.cosk n = CategoryTheory.SimplicialObject.cosk n

noncomputable def SSet.skAdj (n : ℕ) : SSet.Truncated.sk n ⊣ SSet.truncation n

The adjunction between the n-skeleton and n-truncation.

Equations

• SSet.skAdj n = CategoryTheory.SimplicialObject.skAdj n

noncomputable def SSet.coskAdj (n : ℕ) : SSet.truncation n ⊣ SSet.Truncated.cosk n

The adjunction between n-truncation and the n-coskeleton.

Equations

• SSet.coskAdj n = CategoryTheory.SimplicialObject.coskAdj n

instance SSet.Truncated.cosk_reflective (n : ℕ) : CategoryTheory.IsIso (SSet.coskAdj n).counit

Equations

• ⋯ = ⋯

instance SSet.Truncated.sk_coreflective (n : ℕ) : CategoryTheory.IsIso (SSet.skAdj n).unit

Equations

• ⋯ = ⋯

noncomputable def SSet.Truncated.cosk.fullyFaithful (n : ℕ) : (SSet.Truncated.cosk n).FullyFaithful

Since Truncated.inclusion is fully faithful, so is right Kan extension along it.

Equations

• SSet.Truncated.cosk.fullyFaithful n = CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful n

instance SSet.Truncated.cosk.full (n : ℕ) : (SSet.Truncated.cosk n).Full

Equations

• ⋯ = ⋯

instance SSet.Truncated.cosk.faithful (n : ℕ) : (SSet.Truncated.cosk n).Faithful

Equations

• ⋯ = ⋯

noncomputable instance SSet.Truncated.coskAdj.reflective (n : ℕ) : CategoryTheory.Reflective (SSet.Truncated.cosk n)

Equations

• SSet.Truncated.coskAdj.reflective n = CategoryTheory.SimplicialObject.Truncated.coskAdj.reflective n

noncomputable def SSet.Truncated.sk.fullyFaithful (n : ℕ) : (SSet.Truncated.sk n).FullyFaithful

Since Truncated.inclusion is fully faithful, so is left Kan extension along it.

Equations

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

instance SSet.Truncated.sk.full (n : ℕ) : (SSet.Truncated.sk n).Full

Equations

• ⋯ = ⋯

instance SSet.Truncated.sk.faithful (n : ℕ) : (SSet.Truncated.sk n).Faithful

Equations

• ⋯ = ⋯

noncomputable instance SSet.Truncated.skAdj.coreflective (n : ℕ) : CategoryTheory.Coreflective (SSet.Truncated.sk n)

Equations

• SSet.Truncated.skAdj.coreflective n = CategoryTheory.SimplicialObject.Truncated.skAdj.coreflective n

@[reducible, inline]

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.3)

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem SSet.δ_comp_δ_apply {S : SSet} {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))) : CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.δ S j.succ x) = CategoryTheory.SimplicialObject.δ S j (CategoryTheory.SimplicialObject.δ S i.castSucc x)

theorem SSet.δ_comp_δ'_apply {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))) : CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.δ S j x) = CategoryTheory.SimplicialObject.δ S (j.pred ⋯) (CategoryTheory.SimplicialObject.δ S i.castSucc x)

theorem SSet.δ_comp_δ''_apply {S : SSet} {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))) : CategoryTheory.SimplicialObject.δ S (i.castLT ⋯) (CategoryTheory.SimplicialObject.δ S j.succ x) = CategoryTheory.SimplicialObject.δ S j (CategoryTheory.SimplicialObject.δ S i x)

theorem SSet.δ_comp_δ_self_apply {S : SSet} {n : ℕ} {i : Fin (n + 2)} (x : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))) : CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.δ S i.castSucc x) = CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.δ S i.succ x)

theorem SSet.δ_comp_δ_self'_apply {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))) : CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.δ S j x) = CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.δ S i.succ x)

theorem SSet.δ_comp_σ_of_le_apply {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 1)))) : CategoryTheory.SimplicialObject.δ S i.castSucc (CategoryTheory.SimplicialObject.σ S j.succ x) = CategoryTheory.SimplicialObject.σ S j (CategoryTheory.SimplicialObject.δ S i x)

@[simp]

theorem SSet.δ_comp_σ_self_apply {S : SSet} {n : ℕ} (i : Fin (n + 1)) (x : S.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.δ S i.castSucc (CategoryTheory.SimplicialObject.σ S i x) = x

theorem SSet.δ_comp_σ_self'_apply {S : SSet} {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) (x : S.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.δ S j (CategoryTheory.SimplicialObject.σ S i x) = x

@[simp]

theorem SSet.δ_comp_σ_succ_apply {S : SSet} {n : ℕ} (i : Fin (n + 1)) (x : S.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.δ S i.succ (CategoryTheory.SimplicialObject.σ S i x) = x

theorem SSet.δ_comp_σ_succ'_apply {S : SSet} {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) (x : S.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.δ S j (CategoryTheory.SimplicialObject.σ S i x) = x

theorem SSet.δ_comp_σ_of_gt_apply {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 1)))) : CategoryTheory.SimplicialObject.δ S i.succ (CategoryTheory.SimplicialObject.σ S j.castSucc x) = CategoryTheory.SimplicialObject.σ S j (CategoryTheory.SimplicialObject.δ S i x)

theorem SSet.δ_comp_σ_of_gt'_apply {S : SSet} {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 1)))) : CategoryTheory.SimplicialObject.δ S i (CategoryTheory.SimplicialObject.σ S j x) = CategoryTheory.SimplicialObject.σ S (j.castLT ⋯) (CategoryTheory.SimplicialObject.δ S (i.pred ⋯) x)

theorem SSet.σ_comp_σ_apply {S : SSet} {n : ℕ} {i j : Fin (n + 1)} (H : i ≤ j) (x : S.obj (Opposite.op (SimplexCategory.mk n))) : CategoryTheory.SimplicialObject.σ S i.castSucc (CategoryTheory.SimplicialObject.σ S j x) = CategoryTheory.SimplicialObject.σ S j.succ (CategoryTheory.SimplicialObject.σ S i x)