English
The unit of the 2-truncated nerve adjunction has components described by nerve-based maps into ho-functor objects, realized levelwise by refl-quiver identifications.
Русский
Единица 2-уровня нервной adjunction имеет компоненты, заданные через отображения нерва в объекты ho-функтора, реализованные на каждом уровне через идентификации refl-quiver.
LaTeX
$$$\text{unit.app}: X \to \mathrm{nerveFunctor}_2(\mathrm{Cat.of}C)$ with levelwise components given by $\mathrm mk$-constructions.$$
Lean4
/-- The components of the 2-truncated nerve adjunction unit. -/
def app (X : SSet.Truncated.{u} 2) : X ⟶ nerveFunctor₂.obj (hoFunctor₂.obj X) :=
by
fapply toNerve₂.mk' (C := hoFunctor₂.obj X)
·
exact
(ReflQuiv.adj.{u}.unit.app (SSet.oneTruncation₂.obj X) ⋙rq
(SSet.Truncated.HomotopyCategory.quotientFunctor X).toReflPrefunctor ⋙rq
(OneTruncation₂.ofNerve₂.natIso).inv.app (hoFunctor₂.obj X))
· exact fun φ ↦ Quotient.sound _ (HoRel₂.mk φ)
