preservesLimits_preadditiveYoneda_obj

Mathlib.CategoryTheory.Preadditive.Yoneda.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.preservesLimits_preadditiveYoneda_obj

← MathLib Explorer

English

The preadditive Yoneda object functor at X preserves limits.

Русский

Функтор предадмитивного Yoneda в X сохраняет пределы.

LaTeX

$$$\text{PreservesLimits}(\text{preadditiveYoneda.obj } X)$$$

Lean4

instance preservesLimits_preadditiveYoneda_obj (X : C) : PreservesLimits (preadditiveYoneda.obj X) :=
  show PreservesLimits (preadditiveYonedaObj X ⋙ forget₂ _ _) from inferInstance

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

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

Разделы

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

Аффилиация

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