English
There is a canonical natural isomorphism between the functor associated to augmented simplicial objects and the arrow-valued functor obtained by evaluating at the unique initial map; this exhibits the arrow attached to an augmented cosimplicial object as evaluation at the distinguished star → [0] arrow under the relevant equivalence.
Русский
Существует каноническое естественное изоморательство между соответствующим фактором для дополненной симпликсильной категории и функтором стрелки, полученным через проверку на уникальном отображении star → [0] в рамках соответствия; стрелка у дополненного косимплициального объекта определяется посредством эвалюирования на особое отображение star → [0].
LaTeX
$$$\\big(\\text{equivAugmentedSimplicialObject.functor} \\circ \\text{SimplicialObject.Augmented.toArrow}\\big) \\cong \\big(\\text{Functor.mapArrowFunctor}(\\text{Opposite AugmentedSimplexCategory}, C) \\circ (\\text{evaluation}(-, -) .\\text{obj} \\, (\\mathrm{Arrow.mk}(\\mathrm{WithInitial.homTo}(\\mathrm{SimplexCategory.mk}0))^{\\mathrm{op}}))\\big).$$
Lean4
/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow
`star ⟶ of [0]`. -/
@[simps!]
def equivAugmentedSimplicialObjectFunctorCompToArrowIso :
equivAugmentedSimplicialObject.functor ⋙ SimplicialObject.Augmented.toArrow ≅
Functor.mapArrowFunctor _ C ⋙ (evaluation _ _ |>.obj <| .mk <| .op <| WithInitial.homTo <| .mk 0) :=
.refl _
