instIsRightAdjointOfMonadicRightAdjoint

Mathlib.CategoryTheory.Monad.Adjunction

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

English

If R is a MonadicRightAdjoint, then R is a right adjoint.

Русский

Если R является монадическим правым дополнителем, то R является правым сопряжённым.

LaTeX

$$$$R\\text{ is a right adjoint}$$$$

Lean4

instance (R : D ⥤ C) [MonadicRightAdjoint R] : R.IsRightAdjoint :=
  (monadicAdjunction R).isRightAdjoint

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

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

Разделы

Аффилиация

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