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. (In this version, we allow the presheaf `P` to have values in
    a larger universe.) -/
@[simps]
def tautologicalCocone' (P : Cᵒᵖ ⥤ Type max w v₁) : Cocone (CostructuredArrow.proj uliftYoneda.{w} P ⋙ uliftYoneda.{w})
    where
  pt := P
  ι := { app X := X.hom }

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

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

Разделы

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

Аффилиация

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