instIsRightAdjointRightAdjoint

Mathlib.CategoryTheory.Adjunction.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint

English

If L is a left adjoint, then L.rightAdjoint is a right adjoint.

Русский

Если L — левый сопряжённый, то L.rightAdjoint является правым сопряжённым.

LaTeX

$$$\text{If } (L : C \to D) \text{ isLeftAdjoint}, \; L.rightAdjoint \text{ isRightAdjoint}$$$

Lean4

instance (L : C ⥤ D) [L.IsLeftAdjoint] : L.rightAdjoint.IsRightAdjoint :=
  (ofIsLeftAdjoint L).isRightAdjoint

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

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

Разделы

Аффилиация

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