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.

TODO: Future work will 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 : SSet.Truncated 2) : Type u_1

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

Equations

• SSet.OneTruncation₂ S = S.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂.proof_1 })

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

Equations

• SSet.δ₂ i hn hn' = SimplexCategory.δ i

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

Equations

• SSet.σ₂ i hn hn' = SimplexCategory.σ i

@[simp]

theorem SSet.δ₂_zero_comp_σ₂_zero : CategoryTheory.CategoryStruct.comp (SSet.δ₂ 0 ⋯ ⋯) (SSet.σ₂ 0 ⋯ ⋯) = CategoryTheory.CategoryStruct.id { obj := SimplexCategory.mk 0, property := ⋯ }

@[simp]

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

@[simp]

theorem SSet.δ₂_one_comp_σ₂_zero : CategoryTheory.CategoryStruct.comp (SSet.δ₂ 1 ⋯ ⋯) (SSet.σ₂ 0 ⋯ ⋯) = CategoryTheory.CategoryStruct.id { obj := SimplexCategory.mk 0, property := ⋯ }

@[simp]

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

structure SSet.OneTruncation₂.Hom {S : SSet.Truncated 2} (X Y : SSet.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 (SSet.δ₂ 1 ⋯ ⋯).op self.edge = X

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

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem SSet.oneTruncation₂_map_map_edge {S T : SSet.Truncated 2} (F : S ⟶ T) {X✝ Y✝ : ↑((fun (S : SSet.Truncated 2) => CategoryTheory.ReflQuiv.of (SSet.OneTruncation₂ S)) S)} (f : X✝ ⟶ Y✝) : ((SSet.oneTruncation₂.map F).map f).edge = F.app (Opposite.op { obj := SimplexCategory.mk 1, property := SSet.oneTruncation₂.proof_2 }) f.edge

@[simp]

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

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

def SSet.OneTruncation₂.nerveEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] : SSet.OneTruncation₂ ((SSet.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

A hom equivalence over the function OneTruncation₂.nerveEquiv.

Equations

• One or more equations did not get rendered due to their size.

def SSet.OneTruncation₂.ofNerve₂ (C : Type u) [CategoryTheory.Category.{u, u} C] : CategoryTheory.ReflQuiv.of (SSet.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.

Equations

• SSet.OneTruncation₂.ofNerve₂ C = CategoryTheory.ReflQuiv.isoOfEquiv SSet.OneTruncation₂.nerveEquiv SSet.OneTruncation₂.nerveHomEquiv ⋯

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

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

Equations

• SSet.OneTruncation₂.ofNerve₂.natIso = CategoryTheory.NatIso.ofComponents (fun (C : CategoryTheory.Cat) => SSet.OneTruncation₂.ofNerve₂ ↑C) @SSet.OneTruncation₂.ofNerve₂.natIso.proof_1

@[simp]

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

@[simp]

theorem SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map (X : CategoryTheory.Cat) {X✝ Y : ↑(CategoryTheory.Quiv.of ↑(CategoryTheory.Cat.of ↑X))} (f : X✝ ⟶ Y) : (SSet.OneTruncation₂.ofNerve₂.natIso.inv.app X).map f = (SSet.OneTruncation₂.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✝) : ((SSet.OneTruncation₂.ofNerve₂.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) : ((SSet.OneTruncation₂.ofNerve₂.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 (SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve ↑(CategoryTheory.Cat.of ↑X)))))} (a : X✝ ⟶ Y✝) : (SSet.OneTruncation₂.ofNerve₂.natIso.hom.app X).map a = (SSet.OneTruncation₂.nerveHomEquiv X✝ Y✝) a

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.

Equations

• SSet.Truncated.ι0₂ = CategoryTheory.CategoryStruct.comp (SSet.δ₂ 1 SSet.Truncated.ι0₂.proof_1 SSet.Truncated.ι0₂.proof_2) (SSet.δ₂ 1 SSet.Truncated.ι0₂.proof_6 SSet.Truncated.ι0₂.proof_7)

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.

Equations

• SSet.Truncated.ι1₂ = CategoryTheory.CategoryStruct.comp (SSet.δ₂ 0 SSet.Truncated.ι1₂.proof_1 SSet.Truncated.ι1₂.proof_2) (SSet.δ₂ 2 SSet.Truncated.ι1₂.proof_6 SSet.Truncated.ι1₂.proof_7)

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.

Equations

• SSet.Truncated.ι2₂ = CategoryTheory.CategoryStruct.comp (SSet.δ₂ 0 SSet.Truncated.ι2₂.proof_1 SSet.Truncated.ι2₂.proof_2) (SSet.δ₂ 1 SSet.Truncated.ι2₂.proof_6 SSet.Truncated.ι2₂.proof_7)

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

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

Equations

• SSet.Truncated.ev0₂ φ = V.map SSet.Truncated.ι0₂.op φ

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

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

Equations

• SSet.Truncated.ev1₂ φ = V.map SSet.Truncated.ι1₂.op φ

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

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

Equations

• SSet.Truncated.ev2₂ φ = V.map SSet.Truncated.ι2₂.op φ

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.

Equations

• SSet.Truncated.δ0₂ = SSet.δ₂ 0 SSet.Truncated.δ0₂.proof_2 SSet.Truncated.δ0₂.proof_3

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.

Equations

• SSet.Truncated.δ1₂ = SSet.δ₂ 1 SSet.Truncated.δ1₂.proof_2 SSet.Truncated.δ1₂.proof_3

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.

Equations

• SSet.Truncated.δ2₂ = SSet.δ₂ 2 SSet.Truncated.δ2₂.proof_2 SSet.Truncated.δ2₂.proof_3

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

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

Equations

• SSet.Truncated.ev12₂ φ = { edge := V.map SSet.Truncated.δ0₂.op φ, src_eq := ⋯, tgt_eq := ⋯ }

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

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

Equations

• SSet.Truncated.ev02₂ φ = { edge := V.map SSet.Truncated.δ1₂.op φ, src_eq := ⋯, tgt_eq := ⋯ }

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

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

Equations

• SSet.Truncated.ev01₂ φ = { edge := V.map SSet.Truncated.δ2₂.op φ, src_eq := ⋯, tgt_eq := ⋯ }

inductive SSet.Truncated.HoRel₂ {V : SSet.Truncated 2} (X Y : CategoryTheory.Cat.FreeRefl (SSet.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 : SSet.Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) : SSet.Truncated.HoRel₂ { as := V.toPrefunctor.2 SSet.Truncated.ι0₂.op φ } { as := V.toPrefunctor.2 SSet.Truncated.ι2₂.op φ } (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (SSet.Truncated.ev02₂ φ).toPath) (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) ((SSet.Truncated.ev01₂ φ).toPath.comp (SSet.Truncated.ev12₂ φ).toPath))

theorem SSet.Truncated.HoRel₂.mk' {V : SSet.Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) {X₀ X₁ X₂ : SSet.OneTruncation₂ V} (f₀₁ : X₀ ⟶ X₁) (f₁₂ : X₁ ⟶ X₂) (f₀₂ : X₀ ⟶ X₂) (h₀₁ : f₀₁.edge = V.map (SSet.δ₂ 2 ⋯ ⋯).op φ) (h₁₂ : f₁₂.edge = V.map (SSet.δ₂ 0 ⋯ ⋯).op φ) (h₀₂ : f₀₂.edge = V.map (SSet.δ₂ 1 ⋯ ⋯).op φ) : SSet.Truncated.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 : SSet.Truncated 2) : Type u

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

Equations

• V.HomotopyCategory = CategoryTheory.Quotient SSet.Truncated.HoRel₂

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

Equations

• V.instCategoryHomotopyCategory = inferInstanceAs (CategoryTheory.Category.{?u.12, ?u.12} (CategoryTheory.Quotient SSet.Truncated.HoRel₂))

def SSet.Truncated.HomotopyCategory.quotientFunctor (V : SSet.Truncated 2) : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (SSet.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.

Equations

• SSet.Truncated.HomotopyCategory.quotientFunctor V = CategoryTheory.Quotient.functor SSet.Truncated.HoRel₂

theorem SSet.Truncated.HomotopyCategory.lift_unique' (V : SSet.Truncated 2) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F₁ F₂ : CategoryTheory.Functor V.HomotopyCategory D) (h : (SSet.Truncated.HomotopyCategory.quotientFunctor V).comp F₁ = (SSet.Truncated.HomotopyCategory.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 : SSet.Truncated 2} (F : V ⟶ W) : CategoryTheory.Functor V.HomotopyCategory W.HomotopyCategory

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.Truncated.hoFunctor₂_naturality {X Y : SSet.Truncated 2} (f : X ⟶ Y) : CategoryTheory.Functor.comp ((SSet.oneTruncation₂.comp CategoryTheory.Cat.freeRefl).map f) (SSet.Truncated.HomotopyCategory.quotientFunctor Y) = (SSet.Truncated.HomotopyCategory.quotientFunctor X).comp (SSet.Truncated.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.

Equations

• SSet.hoFunctor = (SSet.truncation 2).comp SSet.Truncated.hoFunctor₂