The homotopy category of a simplicial set

The homotopy category of a simplicial set is defined as a quotient of the free category on its underlying reflexive quiver (equivalently its one truncation). The quotient imposes an additional hom relation on this free category, asserting that f ≫ g = h whenever f, g, and h are respectively the 2nd, 0th, and 1st faces of a 2-simplex.

In fact, the associated functor

SSet.hoFunctor : SSet.{u} ⥤ Cat.{u, u} := SSet.truncation 2 ⋙ SSet.hoFunctor₂

is defined by first restricting from simplicial sets to 2-truncated simplicial sets (throwing away the data that is not used for the construction of the homotopy category) and then composing with an analogously defined SSet.hoFunctor₂ : SSet.Truncated.{u} 2 ⥤ Cat.{u,u} implemented relative to the syntax of the 2-truncated simplex category.

In the file Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean we show the functor SSet.hoFunctor to be left adjoint to the nerve by providing an analogous decomposition of the nerve functor, made by possible by the fact that nerves of categories are 2-coskeletal, and then composing a pair of adjunctions, which factor through the category of 2-truncated simplicial sets.

def SSet.OneTruncation₂ (S : Truncated 2) : Type u_1

A 2-truncated simplicial set S has an underlying refl quiver with S _⦋0⦌₂ as its underlying type.

@[deprecated SSet.Truncated.Edge (since := "2025-11-01")]

def SSet.OneTruncation₂.Hom {X : Truncated 2} (x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Truncated.Edge._proof_1 })) : Type u

Alias of SSet.Truncated.Edge.

instance SSet.OneTruncation₂.reflQuiver (S : Truncated 2) : CategoryTheory.ReflQuiver (OneTruncation₂ S)

A 2-truncated simplicial set S has an underlying refl quiver SSet.OneTruncation₂ S.

theorem SSet.OneTruncation₂.reflQuiver_Hom (S : Truncated 2) (x₀ x₁ : S.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Truncated.Edge._proof_1 })) : (x₀ ⟶ x₁) = Truncated.Edge x₀ x₁

theorem SSet.OneTruncation₂.reflQuiver_id (S : Truncated 2) (x : S.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Truncated.Edge._proof_1 })) : CategoryTheory.ReflQuiver.id x = Truncated.Edge.id x

theorem SSet.OneTruncation₂.hom_ext {S : Truncated 2} {x y : OneTruncation₂ S} {f g : x ⟶ y} (h : f.edge = g.edge) : f = g

theorem SSet.OneTruncation₂.hom_ext_iff {S : Truncated 2} {x y : OneTruncation₂ S} {f g : x ⟶ y} : f = g ↔ f.edge = g.edge

@[deprecated "Use reflQuiver_id" (since := "2025-11-01")]

theorem SSet.OneTruncation₂.id_edge {S : Truncated 2} (x : OneTruncation₂ S) : (CategoryTheory.ReflQuiver.id x).edge = S.map (SimplexCategory.Truncated.σ₂ 0 id_edge._proof_1 _proof_1).op x

def SSet.OneTruncation₂.map {S T : Truncated 2} (f : S ⟶ T) : OneTruncation₂ S ⥤rq OneTruncation₂ T

The prefunctor on refl quivers OneTruncation₂ induced by a morphism of 2-truncated simplicial sets.

@[simp]

theorem SSet.OneTruncation₂.map_obj {S T : Truncated 2} (f : S ⟶ T) (x : OneTruncation₂ S) : (map f).obj x = f.app (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 }) x

@[simp]

theorem SSet.OneTruncation₂.map_map {S T : Truncated 2} (f : S ⟶ T) {X✝ Y✝ : OneTruncation₂ S} (e : X✝ ⟶ Y✝) : (map f).map e = Truncated.Edge.map e f

def SSet.oneTruncation₂ : CategoryTheory.Functor (Truncated 2) CategoryTheory.ReflQuiv

The functor that carries a 2-truncated simplicial set to its underlying refl quiver.

@[simp]

theorem SSet.oneTruncation₂_obj (S : Truncated 2) : oneTruncation₂.obj S = CategoryTheory.ReflQuiv.of (OneTruncation₂ S)

@[simp]

theorem SSet.oneTruncation₂_map {X✝ Y✝ : Truncated 2} (f : X✝ ⟶ Y✝) : oneTruncation₂.map f = OneTruncation₂.map f

@[simp]

theorem SSet.OneTruncation₂.homOfEq_edge {X : Truncated 2} {x₁ y₁ x₂ y₂ : OneTruncation₂ X} (f : x₁ ⟶ y₁) (hx : x₁ = x₂) (hy : y₁ = y₂) : (Quiver.homOfEq f hx hy).edge = f.edge

def SSet.OneTruncation₂.nerveEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve C)) ≃ C

An equivalence between the type of objects underlying a category and the type of 0-simplices in the 2-truncated nerve.

theorem SSet.OneTruncation₂.nerveEquiv_symm_apply_map {C : Type u} [CategoryTheory.Category.{v, u} C] (f : C) {X✝ Y✝ : Fin 1} (x✝ : X✝ ⟶ Y✝) : (nerveEquiv.symm f).map x✝ = CategoryTheory.CategoryStruct.id f

theorem SSet.OneTruncation₂.nerveEquiv_symm_apply_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (f : C) (x✝ : Fin 1) : (nerveEquiv.symm f).obj x✝ = f

theorem SSet.OneTruncation₂.nerveEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.ComposableArrows C 0) : nerveEquiv f = f.obj 0

def SSet.OneTruncation₂.nerveHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve C))} : (X ⟶ Y) ≃ (nerveEquiv X ⟶ nerveEquiv Y)

A hom equivalence over the function OneTruncation₂.nerveEquiv.

theorem SSet.OneTruncation₂.nerveHomEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve C))} (f : X ⟶ Y) : nerveHomEquiv f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.hom f.edge) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem SSet.OneTruncation₂.nerveHomEquiv_id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve C))) : nerveHomEquiv (CategoryTheory.ReflQuiver.id X) = CategoryTheory.CategoryStruct.id (nerveEquiv X)

def SSet.OneTruncation₂.ofNerve₂ (C : Type u) [CategoryTheory.Category.{u, u} C] : CategoryTheory.ReflQuiv.of (OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve C))) ≅ CategoryTheory.ReflQuiv.of C

The refl quiver underlying a nerve is isomorphic to the refl quiver underlying the category.

theorem SSet.OneTruncation₂.nerve_hom_ext {X : Truncated 2} {C : Type u} [CategoryTheory.Category.{u, u} C] {F G : X ⟶ (truncation 2).obj (CategoryTheory.nerve C)} (h : map F = map G) : F = G

@[deprecated SSet.OneTruncation₂.nerve_hom_ext (since := "2025-11-06")]

theorem CategoryTheory.toNerve₂.ext {X : SSet.Truncated 2} {C : Type u} [Category.{u, u} C] {F G : X ⟶ (SSet.truncation 2).obj (nerve C)} (h : SSet.OneTruncation₂.map F = SSet.OneTruncation₂.map G) : F = G

Alias of SSet.OneTruncation₂.nerve_hom_ext.

def SSet.OneTruncation₂.ofNerve₂.natIso : CategoryTheory.Nerve.nerveFunctor₂.comp oneTruncation₂ ≅ CategoryTheory.ReflQuiv.forget

The refl quiver underlying a nerve is naturally isomorphic to the refl quiver underlying the category.

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map (X : CategoryTheory.Cat) {X✝ Y : ↑(CategoryTheory.Quiv.of ↑X)} (f : X✝ ⟶ Y) : (natIso.inv.app X).map f = nerveHomEquiv.symm f

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map (X : CategoryTheory.Cat) (a : ↑X) {X✝ Y✝ : Fin 1} (x✝ : X✝ ⟶ Y✝) : ((natIso.inv.app X).obj a).map x✝ = CategoryTheory.CategoryStruct.id a

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj (X : CategoryTheory.Cat) (a : ↑X) (x✝ : Fin 1) : ((natIso.inv.app X).obj a).obj x✝ = a

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj (X : CategoryTheory.Cat) (a : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve ↑X))) : (natIso.hom.app X).obj a = nerveEquiv a

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map (X : CategoryTheory.Cat) {X✝ Y✝ : ↑(CategoryTheory.Quiv.of (OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve ↑X))))} (a : X✝ ⟶ Y✝) : (natIso.hom.app X).map a = nerveHomEquiv a

def SSet.Truncated.ι0₂ : { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 } ⟶ { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 }

The map that picks up the initial vertex of a 2-simplex, as a morphism in the 2-truncated simplex category.

def SSet.Truncated.ι1₂ : { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 } ⟶ { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 }

The map that picks up the middle vertex of a 2-simplex, as a morphism in the 2-truncated simplex category.

def SSet.Truncated.ι2₂ : { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 } ⟶ { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 }

The map that picks up the final vertex of a 2-simplex, as a morphism in the 2-truncated simplex category.

def SSet.Truncated.ev0₂ {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 })) : OneTruncation₂ V

The initial vertex of a 2-simplex in a 2-truncated simplicial set.

def SSet.Truncated.ev1₂ {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 })) : OneTruncation₂ V

The middle vertex of a 2-simplex in a 2-truncated simplicial set.

def SSet.Truncated.ev2₂ {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 })) : OneTruncation₂ V

The final vertex of a 2-simplex in a 2-truncated simplicial set.

def SSet.Truncated.δ0₂ : { obj := SimplexCategory.mk 1, property := ι0₂._proof_4 } ⟶ { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 }

The 0th face of a 2-simplex, as a morphism in the 2-truncated simplex category.

def SSet.Truncated.δ1₂ : { obj := SimplexCategory.mk 1, property := ι0₂._proof_4 } ⟶ { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 }

The 1st face of a 2-simplex, as a morphism in the 2-truncated simplex category.

def SSet.Truncated.δ2₂ : { obj := SimplexCategory.mk 1, property := ι0₂._proof_4 } ⟶ { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 }

The 2nd face of a 2-simplex, as a morphism in the 2-truncated simplex category.

def SSet.Truncated.ev12₂ {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 })) : ev1₂ φ ⟶ ev2₂ φ

The arrow in the ReflQuiver OneTruncation₂ V of a 2-truncated simplicial set arising from the 0th face of a 2-simplex.

def SSet.Truncated.ev02₂ {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 })) : ev0₂ φ ⟶ ev2₂ φ

The arrow in the ReflQuiver OneTruncation₂ V of a 2-truncated simplicial set arising from the 1st face of a 2-simplex.

def SSet.Truncated.ev01₂ {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ι0₂._proof_3 })) : ev0₂ φ ⟶ ev1₂ φ

The arrow in the ReflQuiver OneTruncation₂ V of a 2-truncated simplicial set arising from the 2nd face of a 2-simplex.

inductive SSet.OneTruncation₂.HoRel₂ (V : Truncated 2) : HomRel (CategoryTheory.Cat.FreeRefl (OneTruncation₂ V))

The 2-simplices in a 2-truncated simplicial set V generate a hom relation on the free category on the underlying refl quiver of V.

• of_compStruct {V : Truncated 2} {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₀₂ : Truncated.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : HoRel₂ V ((CategoryTheory.Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (CategoryTheory.CategoryStruct.comp (Quiver.Hom.toPath e₀₁) (Quiver.Hom.toPath e₁₂))) ((CategoryTheory.Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂))

@[deprecated "HoRel₂.of_compStruct" (since := "2025-11-06")]

theorem SSet.OneTruncation₂.HoRel₂.mk (V : Truncated 2) {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_1 })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₀₂ : Truncated.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : HoRel₂ V ((CategoryTheory.Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (CategoryTheory.CategoryStruct.comp (Quiver.Hom.toPath e₀₁) (Quiver.Hom.toPath e₁₂))) ((CategoryTheory.Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂))

def SSet.Truncated.HomotopyCategory (V : Truncated 2) : Type u

The type underlying the homotopy category of a 2-truncated simplicial set V.

instance SSet.Truncated.instCategoryHomotopyCategory (V : Truncated 2) : CategoryTheory.Category.{u_1, u_1} V.HomotopyCategory

def SSet.Truncated.HomotopyCategory.quotientFunctor (V : Truncated 2) : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (OneTruncation₂ V)) V.HomotopyCategory

A canonical functor from the free category on the refl quiver underlying a 2-truncated simplicial set V to its homotopy category.

instance SSet.Truncated.HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor (V : Truncated 2) : (quotientFunctor V).Full

def SSet.Truncated.HomotopyCategory.mk {V : Truncated 2} (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : V.HomotopyCategory

Constructor for objects of the homotopy category of a 2-truncated simplicial set.

theorem SSet.Truncated.HomotopyCategory.mk_surjective {V : Truncated 2} : Function.Surjective mk

theorem SSet.Truncated.HomotopyCategory.ext {V : Truncated 2} {x y : V.HomotopyCategory} (h : x.as.as = y.as.as) : x = y

theorem SSet.Truncated.HomotopyCategory.cases_on {V : Truncated 2} {motive : V.HomotopyCategory → Prop} (h : ∀ (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })), motive (mk x)) (x : V.HomotopyCategory) : motive x

def SSet.Truncated.HomotopyCategory.homMk {V : Truncated 2} {x₀ x₁ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e : Edge x₀ x₁) : mk x₀ ⟶ mk x₁

The morphism in the homotopy category of a 2-truncated simplicial set that is induced by an edge.

theorem SSet.Truncated.HomotopyCategory.congr_arrowMk_homMk {V : Truncated 2} {x₀ x₁ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e : Edge x₀ x₁) {y₀ y₁ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e' : Edge y₀ y₁) (h : e.edge = e'.edge) : CategoryTheory.Arrow.mk (homMk e) = CategoryTheory.Arrow.mk (homMk e')

@[simp]

theorem SSet.Truncated.HomotopyCategory.homMk_id {V : Truncated 2} (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : homMk (Edge.id x) = CategoryTheory.CategoryStruct.id (mk x)

theorem SSet.Truncated.HomotopyCategory.homMk_comp_homMk {V : Truncated 2} {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : CategoryTheory.CategoryStruct.comp (homMk e₀₁) (homMk e₁₂) = homMk e₀₂

theorem SSet.Truncated.HomotopyCategory.homMk_comp_homMk_assoc {V : Truncated 2} {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) {Z : V.HomotopyCategory} (h✝ : mk x₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (homMk e₀₁) (CategoryTheory.CategoryStruct.comp (homMk e₁₂) h✝) = CategoryTheory.CategoryStruct.comp (homMk e₀₂) h✝

def SSet.Truncated.HomotopyCategory.morphismPropertyHomMk (V : Truncated 2) : CategoryTheory.MorphismProperty V.HomotopyCategory

If V is a 2-truncated simplicial sets, this is the family of morphisms in V.HomotopyCategory corresponding to the edges of V. (Any morphism in V.HomotopyCategory is in the multiplicative closure of this family of morphisms, see multiplicativeClosure_morphismPropertyHomMk.)

theorem SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_of_edge {V : Truncated 2} {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e : Edge x y) : morphismPropertyHomMk V (homMk e)

theorem SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap {V : Truncated 2} : morphismPropertyHomMk V = (CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V)

theorem SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk {V : Truncated 2} : (morphismPropertyHomMk V).multiplicativeClosure = ⊤

theorem SSet.Truncated.HomotopyCategory.morphismProperty_eq_top {V : Truncated 2} {W : CategoryTheory.MorphismProperty V.HomotopyCategory} [W.IsMultiplicative] (hW : ∀ {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)) : W = ⊤

def SSet.Truncated.HomotopyCategory.lift {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (obj : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }) → D) (map : {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_id : ∀ (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })), map (Edge.id x) = CategoryTheory.CategoryStruct.id (obj x)) (map_comp : ∀ {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) : CategoryTheory.Functor V.HomotopyCategory D

Constructor for functors from the homotopy category.

@[simp]

theorem SSet.Truncated.HomotopyCategory.lift_obj_mk {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (obj : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }) → D) (map : {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_id : ∀ (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })), map (Edge.id x) = CategoryTheory.CategoryStruct.id (obj x)) (map_comp : ∀ {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : (lift obj (fun {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} => map) map_id ⋯).obj (mk x) = obj x

@[simp]

theorem SSet.Truncated.HomotopyCategory.lift_map_homMk {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (obj : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }) → D) (map : {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)) (map_id : ∀ (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })), map (Edge.id x) = CategoryTheory.CategoryStruct.id (obj x)) (map_comp : ∀ {x₀ x₁ x₂ : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e : Edge x y) : (lift obj (fun {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} => map) map_id ⋯).map (homMk e) = map e

def SSet.Truncated.HomotopyCategory.mkNatTrans {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor V.HomotopyCategory D} (φ : (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)) (hφ : ∀ ⦃x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (φ y) = CategoryTheory.CategoryStruct.comp (φ x) (G.map (homMk e)) := by cat_disch) : F ⟶ G

Constructor for natural transformations between functors from V.HomotopyCategory.

@[simp]

theorem SSet.Truncated.HomotopyCategory.mkNatTrans_app_mk {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor V.HomotopyCategory D} (φ : (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)) (hφ : ∀ ⦃x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (φ y) = CategoryTheory.CategoryStruct.comp (φ x) (G.map (homMk e)) := by cat_disch) (v : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : (mkNatTrans φ hφ).app (mk v) = φ v

def SSet.Truncated.HomotopyCategory.mkNatIso {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor V.HomotopyCategory D} (iso : (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ≅ G.obj (mk x)) (hiso : ∀ ⦃x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (iso y).hom = CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (homMk e)) := by cat_disch) : F ≅ G

Constructor for natural isomorphisms between functors from V.HomotopyCategory.

@[simp]

theorem SSet.Truncated.HomotopyCategory.mkNatIso_hom_app_mk {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor V.HomotopyCategory D} (iso : (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ≅ G.obj (mk x)) (hiso : ∀ ⦃x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (iso y).hom = CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (homMk e)) := by cat_disch) (v : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : (mkNatIso iso hiso).hom.app (mk v) = (iso v).hom

@[simp]

theorem SSet.Truncated.HomotopyCategory.mkNatIso_inv_app_mk {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor V.HomotopyCategory D} (iso : (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ≅ G.obj (mk x)) (hiso : ∀ ⦃x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y), CategoryTheory.CategoryStruct.comp (F.map (homMk e)) (iso y).hom = CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (homMk e)) := by cat_disch) (v : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : (mkNatIso iso hiso).inv.app (mk v) = (iso v).inv

theorem SSet.Truncated.HomotopyCategory.functor_ext {V : Truncated 2} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor V.HomotopyCategory D} (h₁ : ∀ (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })), F.obj (mk x) = G.obj (mk x)) (h₂ : ∀ ⦃x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y), F.map (homMk e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map (homMk e)) (CategoryTheory.eqToHom ⋯))) : F = G

instance SSet.Truncated.HomotopyCategory.instSubsingletonOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk (X : Truncated 2) [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }))] : Subsingleton X.HomotopyCategory

instance SSet.Truncated.HomotopyCategory.subsingleton_hom (X : Truncated 2) [Unique (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ι0₂._proof_4 }))] (x y : X.HomotopyCategory) : Subsingleton (x ⟶ y)

instance SSet.Truncated.HomotopyCategory.instUniqueOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk (X : Truncated 2) [Unique (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }))] : Unique X.HomotopyCategory

def SSet.Truncated.HomotopyCategory.isTerminal (X : Truncated 2) [Unique (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ι0₂._proof_4 }))] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of X.HomotopyCategory)

If X : Truncated 2 has a unique 0-simplex and (at most) one 1-simplex, then X.HomotopyCategory is a terminal object in Cat.

def SSet.Truncated.mapHomotopyCategory {V W : Truncated 2} (f : V ⟶ W) : CategoryTheory.Functor V.HomotopyCategory W.HomotopyCategory

A map of 2-truncated simplicial sets induces a functor between homotopy categories.

@[simp]

theorem SSet.Truncated.mapHomotopyCategory_obj {V W : Truncated 2} (f : V ⟶ W) (x : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : (mapHomotopyCategory f).obj (HomotopyCategory.mk x) = HomotopyCategory.mk (f.app (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }) x)

@[simp]

theorem SSet.Truncated.mapHomotopyCategory_homMk {V W : Truncated 2} (f : V ⟶ W) {x y : V.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })} (e : Edge x y) : (mapHomotopyCategory f).map (HomotopyCategory.homMk e) = HomotopyCategory.homMk (e.map f)

def SSet.Truncated.hoFunctor₂ : CategoryTheory.Functor (Truncated 2) CategoryTheory.Cat

The functor that takes a 2-truncated simplicial set to its homotopy category.

theorem SSet.Truncated.hoFunctor₂_naturality {X Y : Truncated 2} (f : X ⟶ Y) : ((oneTruncation₂.comp CategoryTheory.Cat.freeRefl).map f).toFunctor.comp (HomotopyCategory.quotientFunctor Y) = (HomotopyCategory.quotientFunctor X).comp (mapHomotopyCategory f)

theorem SSet.Truncated.HomotopyCategory.lift_unique' (V : Truncated 2) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F₁ F₂ : CategoryTheory.Functor V.HomotopyCategory D) (h : (quotientFunctor V).comp F₁ = (quotientFunctor V).comp F₂) : F₁ = F₂

By Quotient.lift_unique' (not Quotient.lift) we have that quotientFunctor V is an epimorphism.

def SSet.hoFunctor : CategoryTheory.Functor SSet CategoryTheory.Cat

The functor that takes a simplicial set to its homotopy category by passing through the 2-truncation.

def SSet.hoFunctor.obj.equiv (X : SSet) : ↑(hoFunctor.obj X) ≃ X.obj (Opposite.op (SimplexCategory.mk 0))

For a simplicial set X, the underlying type of hoFunctor.obj X is equivalent to X _⦋0⦌.

instance SSet.instUniqueOneTruncation₂DeltaZero : Unique (OneTruncation₂ ((truncation 2).obj (stdSimplex.obj (SimplexCategory.mk 0))))

Since ⦋0⦌ : SimplexCategory is terminal, Δ[0] has a unique point and thus OneTruncation₂ ((truncation 2).obj Δ[0]) has a unique inhabitant.

instance SSet.instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk (x y : OneTruncation₂ ((truncation 2).obj (stdSimplex.obj (SimplexCategory.mk 0)))) : Unique (x ⟶ y)

Since ⦋0⦌ : SimplexCategory is terminal, Δ[0] has a unique edge and thus the homs of OneTruncation₂ ((truncation 2).obj Δ[0]) have unique inhabitants.

instance SSet.instUniqueHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk : Unique ((truncation 2).obj (stdSimplex.obj (SimplexCategory.mk 0))).HomotopyCategory

instance SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk : CategoryTheory.IsDiscrete ((truncation 2).obj (stdSimplex.obj (SimplexCategory.mk 0))).HomotopyCategory

def SSet.isTerminalHoFunctorDeltaZero : CategoryTheory.Limits.IsTerminal (hoFunctor.obj (stdSimplex.obj (SimplexCategory.mk 0)))

The category hoFunctor.obj (Δ[0]) is terminal.

noncomputable def SSet.hoFunctor.terminalIso : hoFunctor.obj (⊤_ SSet) ≅ ⊤_ CategoryTheory.Cat

The homotopy category functor preserves generic terminal objects.

instance SSet.hoFunctor.preservesTerminal : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty SSet) hoFunctor

instance SSet.hoFunctor.preservesTerminal' : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) hoFunctor