colimitCoconeIsColimit

Mathlib.CategoryTheory.Limits.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Coyoneda.colimitCoconeIsColimit

Lean4

/-- The proposed colimit cocone over `coyoneda.obj X` is a colimit cocone.
-/
@[simps]
def colimitCoconeIsColimit (X : Cᵒᵖ) : IsColimit (colimitCocone X)
    where
  desc s _ := s.ι.app (unop X) (𝟙 _)
  fac s
    Y := by
    funext f
    convert congr_fun (s.w f).symm (𝟙 (unop X))
    simp only [coyoneda_obj_obj, Functor.const_obj_obj, types_comp_apply, coyoneda_obj_map, Category.id_comp]
  uniq s m
    w := by
    apply funext; rintro ⟨⟩
    rw [← w]
    simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru