colimitCoyonedaHomIsoLimitUnop_π_apply

English

The Induction Yoneda construction yields that Ind.yoneda (C) is a full functor.

Русский

Конструкция Ind.yoneda для C образует полную вложенную вложенную адвекцию (полную ленту) Functor.

LaTeX

$$$(Ind.yoneda)(C)\text{ is full}$$$

Lean4

@[simp]
theorem colimitCoyonedaHomIsoLimitUnop_π_apply (f : colimit (D ⋙ coyoneda) ⟶ F) (i : I) :
    limit.π (D.unop ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitCoyonedaHomIsoLimitUnop D F).hom f) =
      ⟨f.app (D.obj (op i)).unop ((colimit.ι (D ⋙ coyoneda) ⟨i⟩).app (D.obj (op i)).unop (𝟙 (D.obj (op i)).unop))⟩ :=
  haveI : HasColimit (D.unop.op ⋙ coyoneda) := inferInstanceAs <| HasColimit (D ⋙ coyoneda)
  colimitCoyonedaHomIsoLimit'_π_apply _ _ _ _

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