lim

Mathlib.CategoryTheory.Limits.Indization.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Ind.lim

Lean4

/-- This is the functor `(I ⥤ C) ⥤ Ind C` that sends a functor `F` to `colim (Y ∘ F)`, where `Y`
is the Yoneda embedding. It is known as "ind-lim" and denoted `“colim”` in [Kashiwara2006]. -/
protected noncomputable def lim (I : Type v) [SmallCategory I] [IsFiltered I] : (I ⥤ C) ⥤ Ind C :=
  (whiskeringRight _ _ _).obj Ind.yoneda ⋙ colim

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

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

Разделы

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

Аффилиация

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