instPreservesColimitsOfSizeOfIsLeftAdjoint

Mathlib.CategoryTheory.Adjunction.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint

English

If F is a left adjoint, it preserves colimits of size {v, u}.

Русский

Если F — левый сопряжённый, он сохраняет колимиты размера {v,u}.

LaTeX

$$$$[\\text{IsLeftAdjoint } F] \\Rightarrow \\operatorname{PreservesColimitsOfSize}.{v, u}\\; F.$$$$

Lean4

noncomputable instance [IsLeftAdjoint F] : PreservesColimitsOfSize.{v, u} F where

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

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

Разделы

Аффилиация

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