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

@[reducible, inline]

abbrev SSet : Type (u + 1)

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

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

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

@[simp]

theorem SSet.id_app (X : SSet) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.CategoryStruct.id X).app n = CategoryTheory.CategoryStruct.id (X.obj n)

@[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)

theorem SSet.comp_app_assoc {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ) {Z✝ : Type u_1} (h : Z.obj n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).app n) h = CategoryTheory.CategoryStruct.comp (f.app n) (CategoryTheory.CategoryStruct.comp (g.app n) h)

def SSet.const {X Y : SSet} (y : Y.obj (Opposite.op (SimplexCategory.mk 0))) : X ⟶ Y

The constant map of simplicial sets X ⟶ Y induced by a simplex y : Y _[0].

@[simp]

theorem SSet.const_app {X Y : SSet} (y : Y.obj (Opposite.op (SimplexCategory.mk 0))) (n : SimplexCategoryᵒᵖ) (x✝ : X.obj n) : (const y).app n x✝ = Y.map ((Opposite.unop n).const (SimplexCategory.mk 0) 0).op y

@[simp]

theorem SSet.comp_const {X Y Z : SSet} (f : X ⟶ Y) (z : Z.obj (Opposite.op (SimplexCategory.mk 0))) : CategoryTheory.CategoryStruct.comp f (const z) = const z

@[simp]

theorem SSet.const_comp {X Y Z : SSet} (y : Y.obj (Opposite.op (SimplexCategory.mk 0))) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (const y) g = const (g.app (Opposite.op (SimplexCategory.mk 0)) y)

def SSet.uliftFunctor : CategoryTheory.Functor SSet SSet

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

@[reducible, inline]

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

Truncated simplicial sets.

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.

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

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

@[reducible, inline]

abbrev SSet.Truncated.trunc (n m : ℕ) (h : m ≤ n := by lia) : CategoryTheory.Functor (Truncated n) (Truncated m)

Further truncation of truncated simplicial sets.

@[simp]

theorem SSet.Truncated.id_app {n : ℕ} (X : Truncated n) (d : (SimplexCategory.Truncated n)ᵒᵖ) : (CategoryTheory.CategoryStruct.id X).app d = CategoryTheory.CategoryStruct.id (X.obj d)

@[simp]

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

theorem SSet.Truncated.comp_app_assoc {n : ℕ} {X Y Z : Truncated n} (f : X ⟶ Y) (g : Y ⟶ Z) (d : (SimplexCategory.Truncated n)ᵒᵖ) {Z✝ : Type u_1} (h : Z.obj d ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).app d) h = CategoryTheory.CategoryStruct.comp (f.app d) (CategoryTheory.CategoryStruct.comp (g.app d) h)

@[reducible, inline]

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

The truncation functor on simplicial sets.

def SSet.truncationCompTrunc {n m : ℕ} (h : m ≤ n) : (truncation n).comp (Truncated.trunc n m ⋯) ≅ truncation m

For all m ≤ n, truncation m factors through SSet.Truncated n.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The n-skeleton as an endofunctor on SSet.

@[reducible, inline]

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

The n-coskeleton as an endofunctor on SSet.

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

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

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

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

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.

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

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

@[implicit_reducible]

noncomputable instance SSet.Truncated.coskAdj.reflective (n : ℕ) : CategoryTheory.Reflective (Truncated.cosk 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.

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

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

@[implicit_reducible]

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

@[reducible, inline]

abbrev SSet.Augmented : Type (u + 1)

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

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)