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.

@[reducible, inline]

abbrev SSet.δ₂ {n : ℕ} (i : Fin (n + 2)) (hn : (SimplexCategory.mk n).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) : { obj := SimplexCategory.mk n, property := hn } ⟶ { obj := SimplexCategory.mk (n + 1), property := hn' }

Abbreviations for face maps in the 2-truncated simplex category.

@[reducible, inline]

abbrev SSet.σ₂ {n : ℕ} (i : Fin (n + 1)) (hn : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk n).len ≤ 2 := by decide) : { obj := SimplexCategory.mk (n + 1), property := hn } ⟶ { obj := SimplexCategory.mk n, property := hn' }

Abbreviations for degeneracy maps in the 2-truncated simplex category.

@[simp]

theorem SSet.δ₂_zero_comp_σ₂_zero {n : ℕ} (hn : (SimplexCategory.mk n).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 0 hn hn') (σ₂ 0 hn' hn) = CategoryTheory.CategoryStruct.id { obj := SimplexCategory.mk n, property := hn }

@[simp]

theorem SSet.δ₂_zero_comp_σ₂_zero_assoc {n : ℕ} (hn : (SimplexCategory.mk n).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := SimplexCategory.mk n, property := hn } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 0 hn hn') (CategoryTheory.CategoryStruct.comp (σ₂ 0 hn' hn) h) = h

theorem SSet.δ₂_zero_comp_σ₂_one : CategoryTheory.CategoryStruct.comp (δ₂ 0 ⋯ ⋯) (σ₂ 1 ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (δ₂ 0 ⋯ ⋯)

theorem SSet.δ₂_zero_comp_σ₂_one_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := SimplexCategory.mk 1, property := ⋯ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 0 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (σ₂ 1 ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (δ₂ 0 ⋯ ⋯) h)

@[simp]

theorem SSet.δ₂_one_comp_σ₂_zero {n : ℕ} (hn : (SimplexCategory.mk n).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (σ₂ 0 hn' hn) = CategoryTheory.CategoryStruct.id { obj := SimplexCategory.mk n, property := hn }

@[simp]

theorem SSet.δ₂_one_comp_σ₂_zero_assoc {n : ℕ} (hn : (SimplexCategory.mk n).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := SimplexCategory.mk n, property := hn } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 1 hn hn') (CategoryTheory.CategoryStruct.comp (σ₂ 0 hn' hn) h) = h

@[simp]

theorem SSet.δ₂_two_comp_σ₂_one : CategoryTheory.CategoryStruct.comp (δ₂ 2 ⋯ ⋯) (σ₂ 1 ⋯ ⋯) = CategoryTheory.CategoryStruct.id { obj := SimplexCategory.mk 1, property := ⋯ }

@[simp]

theorem SSet.δ₂_two_comp_σ₂_one_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := SimplexCategory.mk 1, property := ⋯ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 2 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (σ₂ 1 ⋯ ⋯) h) = h

theorem SSet.δ₂_two_comp_σ₂_zero : CategoryTheory.CategoryStruct.comp (δ₂ 2 ⋯ ⋯) (σ₂ 0 ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (δ₂ 1 ⋯ ⋯)

theorem SSet.δ₂_two_comp_σ₂_zero_assoc {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ 2} (h : { obj := SimplexCategory.mk 1, property := ⋯ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ₂ 2 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp (σ₂ 0 ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (δ₂ 1 ⋯ ⋯) h)

structure SSet.OneTruncation₂.Hom {S : Truncated 2} (X Y : OneTruncation₂ S) : Type u_1

The hom-types of the refl quiver underlying a simplicial set S are types of edges in S _⦋1⦌₂ together with source and target equalities.

• edge : S.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })

  An arrow in OneTruncation₂.Hom X Y includes the data of a 1-simplex.

• src_eq : S.map (δ₂ 1 ⋯ ⋯).op self.edge = X

  An arrow in OneTruncation₂.Hom X Y includes a source equality.

• tgt_eq : S.map (δ₂ 0 ⋯ ⋯).op self.edge = Y

  An arrow in OneTruncation₂.Hom X Y includes a target equality.

theorem SSet.OneTruncation₂.Hom.ext_iff {S : Truncated 2} {X Y : OneTruncation₂ S} {x y : X.Hom Y} : x = y ↔ x.edge = y.edge

theorem SSet.OneTruncation₂.Hom.ext {S : Truncated 2} {X Y : OneTruncation₂ S} {x y : X.Hom Y} (edge : x.edge = y.edge) : x = y

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

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

@[simp]

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

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₂_map_map_edge {S T : Truncated 2} (F : S ⟶ T) {X✝ Y✝ : ↑(CategoryTheory.ReflQuiv.of (OneTruncation₂ S))} (f : X✝ ⟶ Y✝) : ((oneTruncation₂.map F).map f).edge = F.app (Opposite.op { obj := SimplexCategory.mk 1, property := oneTruncation₂._proof_2 }) f.edge

@[simp]

theorem SSet.oneTruncation₂_map_obj {S T : Truncated 2} (F : S ⟶ T) (a✝ : S.obj (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 })) : (oneTruncation₂.map F).obj a✝ = F.app (Opposite.op { obj := SimplexCategory.mk 0, property := OneTruncation₂._proof_1 }) a✝

@[simp]

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

theorem SSet.OneTruncation₂.hom_ext {S : Truncated 2} {x y : OneTruncation₂ S} {f g : x ⟶ y} : 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

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

@[simp]

theorem SSet.OneTruncation₂.nerveEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : nerveEquiv.symm X = CategoryTheory.ComposableArrows.mk₀ X

@[simp]

theorem SSet.OneTruncation₂.nerveEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (X : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve C))) : nerveEquiv X = CategoryTheory.ComposableArrows.obj' X 0 nerveEquiv._proof_1

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.

def SSet.OneTruncation₂.ofNerve₂ (C : Type u) [CategoryTheory.Category.{u, u} C] : CategoryTheory.ReflQuiv.of (OneTruncation₂ (CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C))) ≅ CategoryTheory.ReflQuiv.of C

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

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 ↑(CategoryTheory.Cat.of ↑X))} (f : X✝ ⟶ Y) : (natIso.inv.app X).map f = (nerveHomEquiv (CategoryTheory.ComposableArrows.mk₀ X✝) (CategoryTheory.ComposableArrows.mk₀ Y)).symm f

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map (X : CategoryTheory.Cat) (a : ↑(CategoryTheory.Cat.of ↑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 : ↑(CategoryTheory.Cat.of ↑X)) (x✝ : Fin 1) : ((natIso.inv.app X).obj a).obj x✝ = a

@[simp]

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

@[simp]

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

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

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 := ⋯ } ⟶ { obj := SimplexCategory.mk 2, property := ⋯ }

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 := ⋯ } ⟶ { obj := SimplexCategory.mk 2, property := ⋯ }

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 := ⋯ })) : 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 := ⋯ })) : 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 := ⋯ })) : OneTruncation₂ V

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

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

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 := ⋯ } ⟶ { obj := SimplexCategory.mk 2, property := ⋯ }

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 := ⋯ } ⟶ { obj := SimplexCategory.mk 2, property := ⋯ }

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 := ⋯ })) : 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 := ⋯ })) : 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 := ⋯ })) : 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.Truncated.HoRel₂ {V : Truncated 2} (X Y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ V)) (f g : X ⟶ Y) : Prop

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.

• mk {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) : HoRel₂ { as := V.2 ι0₂.op φ } { as := V.2 ι2₂.op φ } (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (ev02₂ φ).toPath) (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) ((ev01₂ φ).toPath.comp (ev12₂ φ).toPath))

theorem SSet.Truncated.HoRel₂.mk' {V : Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) {X₀ X₁ X₂ : OneTruncation₂ V} (f₀₁ : X₀ ⟶ X₁) (f₁₂ : X₁ ⟶ X₂) (f₀₂ : X₀ ⟶ X₂) (h₀₁ : f₀₁.edge = V.map (δ₂ 2 ⋯ ⋯).op φ) (h₁₂ : f₁₂.edge = V.map (δ₂ 0 ⋯ ⋯).op φ) (h₀₂ : f₀₂.edge = V.map (δ₂ 1 ⋯ ⋯).op φ) : HoRel₂ { as := X₀ } { as := X₂ } (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) f₀₂.toPath) (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (f₀₁.toPath.comp f₁₂.toPath))

A 2-simplex whose faces are identified with certain arrows in OneTruncation₂ V defines a term of type HoRel₂ between those arrows.

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, u} 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.

theorem SSet.Truncated.HomotopyCategory.lift_unique' (V : Truncated 2) {D : Type u_1} [CategoryTheory.Category.{u_2, 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.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.

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) : CategoryTheory.Functor.comp ((oneTruncation₂.comp CategoryTheory.Cat.freeRefl).map f) (HomotopyCategory.quotientFunctor Y) = (HomotopyCategory.quotientFunctor X).comp (mapHomotopyCategory f)

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.

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.

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