instHasFiniteLimitsFunctor

Mathlib.CategoryTheory.Limits.FunctorCategory.Finite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.instHasFiniteLimitsFunctor

English

If C has finite limits, then the functor category K ⥤ C has finite limits.

Русский

Если C имеет конечные пределы, то категория функторов K ⥤ C имеет конечные пределы.

LaTeX

$$$\\text{HasFiniteLimits}(K \\;⥤\\; C).$$$

Lean4

instance [HasFiniteLimits C] : HasFiniteLimits (K ⥤ C) :=
  ⟨fun _ ↦ inferInstance⟩

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

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

Разделы

Аффилиация

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