tautologicalCocone

Mathlib.CategoryTheory.Limits.Presheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.tautologicalCocone

Lean4

/-- For a presheaf `P`, consider the forgetful functor from the category of representable
    presheaves over `P` to the category of presheaves. There is a tautological cocone over this
    functor whose leg for a natural transformation `V ⟶ P` with `V` representable is just that
    natural transformation. -/
@[simps]
def tautologicalCocone (P : Cᵒᵖ ⥤ Type v₁) : Cocone (CostructuredArrow.proj yoneda P ⋙ yoneda)
    where
  pt := P
  ι := { app X := X.hom }

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

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

Разделы

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

Аффилиация

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