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

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

instance SSet.hasColimits : CategoryTheory.Limits.HasColimits SSet

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

@[simp]

theorem SSet.comp_app {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).app n = CategoryTheory.CategoryStruct.comp (f.app n) (g.app n)

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.Truncated (n : ℕ) : Type (u + 1)

Truncated simplicial sets.

Equations

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

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

Equations

• SSet.Truncated.largeCategory n = id inferInstance

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

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

def SSet.Truncated.uliftFunctor (k : ℕ) : CategoryTheory.Functor (Truncated k) (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.17) (Type (max ?u.17 ?u.18))).obj CategoryTheory.uliftFunctor.{?u.18, ?u.17}

theorem SSet.Truncated.hom_ext {n : ℕ} {X Y : 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 (Truncated n)

The truncation functor on simplicial sets.

Equations

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

@[reducible, inline]

abbrev SSet.Truncated.sk (n : ℕ) : CategoryTheory.Functor (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 (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 : ℕ) : Truncated.sk n ⊣ truncation n

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

Equations

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

noncomputable def SSet.coskAdj (n : ℕ) : truncation n ⊣ 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 (coskAdj n).counit

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

noncomputable def SSet.Truncated.cosk.fullyFaithful (n : ℕ) : (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 : ℕ) : (Truncated.cosk n).Full

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

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

Equations

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

noncomputable def SSet.Truncated.sk.fullyFaithful (n : ℕ) : (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 : ℕ) : (Truncated.sk n).Full

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

noncomputable instance SSet.Truncated.skAdj.coreflective (n : ℕ) : CategoryTheory.Coreflective (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)

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)

theorem SSet.δ_naturality_apply {S T : SSet} (f : S ⟶ T) {n : ℕ} (i : Fin (n + 2)) (x : S.obj (Opposite.op (SimplexCategory.mk (n + 1)))) : f.app (Opposite.op (SimplexCategory.mk n)) (CategoryTheory.SimplicialObject.δ S i x) = CategoryTheory.SimplicialObject.δ T i (f.app (Opposite.op (SimplexCategory.mk (n + 1))) x)

theorem SSet.σ_naturality_apply {S T : SSet} (f : S ⟶ T) {n : ℕ} (i : Fin (n + 1)) (x : S.obj (Opposite.op (SimplexCategory.mk n))) : f.app (Opposite.op (SimplexCategory.mk (n + 1))) (CategoryTheory.SimplicialObject.σ S i x) = CategoryTheory.SimplicialObject.σ T i (f.app (Opposite.op (SimplexCategory.mk n)) x)