quotientFunctor — Mathlib

English

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

Русский

Канонический функтор от свободной категории на refl-кворе, лежащей в основе 2-отрезанного симпликсального множества V, к его гомотопической категории.

LaTeX

$$$\\mathrm{quotientFunctor}(V) : \\mathrm{Cat.FreeRefl}(\\mathrm{OneTruncation}_2 V) \\to \\mathrm{HomotopyCategory}(V)$$$

Lean4

/-- A canonical functor from the free category on the refl quiver underlying a 2-truncated
simplicial set `V` to its homotopy category. -/
def _root_.SSet.Truncated.HomotopyCategory.quotientFunctor (V : SSet.Truncated.{u} 2) :
    Cat.FreeRefl (OneTruncation₂ V) ⥤ V.HomotopyCategory :=
  Quotient.functor _

Похожие утверждения