isBinaryBilimitOfPreserves

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

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

Lean4

/-- A functor `F` preserves binary biproducts of `X` and `Y` if `F` maps every bilimit bicone over
`X` and `Y` to a bilimit bicone over `F.obj X` and `F.obj Y`. -/
def isBinaryBilimitOfPreserves {X Y : C} (F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBinaryBiproduct X Y F]
    {b : BinaryBicone X Y} (hb : b.IsBilimit) : (F.mapBinaryBicone b).IsBilimit :=
  (PreservesBinaryBiproduct.preserves hb).some

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

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

Разделы

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

Аффилиация

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