instIsLeftAdjointOfComonadicLeftAdjoint

Mathlib.CategoryTheory.Monad.Adjunction

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

English

If L is ComonadicLeftAdjoint, then L is a left adjoint.

Русский

Если L является ComonadicLeftAdjoint, то L является левым сопряжённым.

LaTeX

$$$$L\\text{ isLeftAdjoint}$$$$

Lean4

instance (L : C ⥤ D) [ComonadicLeftAdjoint L] : L.IsLeftAdjoint :=
  (comonadicAdjunction L).isLeftAdjoint

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

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

Разделы

Аффилиация

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