preservesLimits_preadditiveCoyoneda_obj

Mathlib.CategoryTheory.Preadditive.Yoneda.Limits

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

← MathLib Explorer

English

For X in C^op, the preadditiveCoyonedaObj X preserves limits.

Русский

Для X в C^op предадмитивный Coyoneda-объект X сохраняет пределы.

LaTeX

$$$\text{PreservesLimits}(\text{preadditiveCoyonedaObj } X)$$$

Lean4

instance preservesLimits_preadditiveCoyoneda_obj (X : Cᵒᵖ) : PreservesLimits (preadditiveCoyoneda.obj X) :=
  show PreservesLimits (preadditiveCoyonedaObj (unop X) ⋙ forget₂ _ _) from inferInstance

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

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

Разделы

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

Аффилиация

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