English
The counit component of the nerve adjunction is compatible with the quotient construction and whiskering, yielding an equality of functors from the nerve to Cat.
Русский
Компонента контра-единицы сопряжения нервной конструкционной связи совместима с конструктором квази-эквивалентности и отклонением, порождая равенство функторов от нерва к категории Cat.
LaTeX
$$$\mathrm{quotientFunctor}(\mathrm{nerveFunctor}_2(\mathrm{Cat.of}\ C)) \circ \mathrm{nerve₂Adj.counit.app}\, C = \Big( \mathrm{whiskerRight}(\mathrm{OneTruncation₂.ofNerve₂.natIso.hom}) \circ \mathrm{ReflQuiv.adj.counit} \!\Big).\mathrm{app}(\mathrm{Cat.of}\ C).$$$
Lean4
/-- The components of the counit of `nerve₂Adj`. -/
@[simps!]
def app (C : Type u) [SmallCategory C] : (nerveFunctor₂.obj (Cat.of C)).HomotopyCategory ⥤ C :=
by
fapply Quotient.lift
· exact (whiskerRight (OneTruncation₂.ofNerve₂.natIso).hom _ ≫ ReflQuiv.adj.{u}.counit).app (Cat.of C)
· intro x y f g rel
obtain ⟨φ⟩ := rel
simpa [ReflQuiv.adj, Quot.liftOn, Cat.FreeRefl.quotientFunctor, Quotient.functor, pathComposition, Quiv.adj,
OneTruncation₂.nerveHomEquiv] using
φ.map_comp (X := 0) (Y := 1) (Z := 2) (homOfLE (by decide)) (homOfLE (by decide))
