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.

Equations

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

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 (SimplexCategory.Truncated.δ₂ 1 ⋯ ⋯).op self.edge = X

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

• tgt_eq : S.map (SimplexCategory.Truncated.δ₂ 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.

Equations

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

@[simp]

theorem SSet.OneTruncation₂.id_edge {S : Truncated 2} (X : OneTruncation₂ S) : (CategoryTheory.ReflQuiver.id X).edge = S.map (SimplexCategory.Truncated.σ₂ 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.

Equations

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

@[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₂_obj (S : Truncated 2) : oneTruncation₂.obj S = CategoryTheory.ReflQuiv.of (OneTruncation₂ S)

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

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.

Equations

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

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

@[simp]

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

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.

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 (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 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 : OneTruncation₂ ((truncation 2).obj (CategoryTheory.nerve ↑(CategoryTheory.Cat.of ↑X)))) : (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) : (natIso.inv.app X).map f = (nerveHomEquiv (CategoryTheory.ComposableArrows.mk₀ X✝) (CategoryTheory.ComposableArrows.mk₀ Y)).symm f

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

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

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

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

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

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

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

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.

Equations

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

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.

Equations

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

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.

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₂ = SimplexCategory.Truncated.δ₂ 0 SSet.oneTruncation₂._proof_2 SSet.Truncated.ι0₂._proof_4

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₂ = SimplexCategory.Truncated.δ₂ 1 SSet.oneTruncation₂._proof_2 SSet.Truncated.ι0₂._proof_4

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₂ = SimplexCategory.Truncated.δ₂ 2 SSet.oneTruncation₂._proof_2 SSet.Truncated.ι0₂._proof_4

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.

Equations

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

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.

Equations

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

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.

Equations

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

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 (SimplexCategory.Truncated.δ₂ 2 ⋯ ⋯).op φ) (h₁₂ : f₁₂.edge = V.map (SimplexCategory.Truncated.δ₂ 0 ⋯ ⋯).op φ) (h₀₂ : f₀₂.edge = V.map (SimplexCategory.Truncated.δ₂ 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.

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

def SSet.Truncated.hoFunctor₂ : CategoryTheory.Functor (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 : 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.

Equations

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

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.

Equations

• SSet.instUniqueOneTruncation₂DeltaZero = inferInstanceAs (Unique (ULift.{?u.5, 0} (SimplexCategory.mk 0 ⟶ SimplexCategory.mk 0)))

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.

Equations

• SSet.instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk x y = { default := ⋯ ▸ ⋯ ▸ CategoryTheory.ReflQuiver.id default, uniq := ⋯ }

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

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

Equations

• SSet.isTerminalHoFunctorDeltaZero = CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete

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

The homotopy category functor preserves generic terminal objects.

Equations

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

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

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