limitFunctor

Mathlib.CategoryTheory.Localization.FiniteProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor

Lean4

/-- The (candidate) limit functor for the localized category.
It is induced by `lim ⋙ L : (Discrete J ⥤ C) ⥤ D`. -/
noncomputable abbrev limitFunctor : (Discrete J ⥤ D) ⥤ D :=
  Localization.lift _ (inverts L W J) ((whiskeringRight (Discrete J) C D).obj L)

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

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

Разделы

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

Аффилиация

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