equivAugmentedSimplicialObjectFunctorCompPointIso

English

There is an isomorphism between the composed functor AugmentedSimplicialObject and the evaluation at the initial point of the augmented simplex category.

Русский

Существет изоморфизм между AugmentedSimplicialObject и оценкой по начальной точке аугментированного симпликсового категориального объекта.

LaTeX

$$EquivAugmentedSimplicialObjectFunctorCompPointIso$$

Lean4

/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
taking the point of the augmentation corresponds to evaluation at the initial object. -/
@[simps!]
def equivAugmentedSimplicialObjectFunctorCompPointIso :
    equivAugmentedSimplicialObject.functor ⋙ SimplicialObject.Augmented.point ≅ (evaluation _ C).obj (.op .star) :=
  .refl _

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