English
A map F between 2-truncated simplicial sets V ⟶ W induces a functor between their homotopy categories, via functorial construction on quotients.
Русский
Точное отображение F между 2-отрезанными симпликсальными множествами V и W порождает функтор между их гомотопиями.
LaTeX
$$$F \\mapsto \\mathrm{mapHomotopyCategory}(F): V\\!\\!\u2192 W \\text{ induces } V.HomotopyCategory \\to W.HomotopyCategory$$
Lean4
/-- A map of 2-truncated simplicial sets induces a functor between homotopy categories. -/
def mapHomotopyCategory {V W : SSet.Truncated.{u} 2} (F : V ⟶ W) : V.HomotopyCategory ⥤ W.HomotopyCategory :=
CategoryTheory.Quotient.lift _ ((oneTruncation₂ ⋙ Cat.freeRefl).map F ⋙ HomotopyCategory.quotientFunctor W)
(by
rintro _ _ _ _ ⟨φ⟩
apply CategoryTheory.Quotient.sound
apply
HoRel₂.mk' (φ := F.app _ φ) (f₀₁ := (oneTruncation₂.map F).map (ev01₂ φ)) (f₀₂ :=
(oneTruncation₂.map F).map (ev02₂ φ)) (f₁₂ := (oneTruncation₂.map F).map (ev12₂ φ))
all_goals apply FunctorToTypes.naturality)
