instIsRightAdjointCoreflector

Mathlib.CategoryTheory.Adjunction.Reflective

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

English

If j is Coreflective, then coreflector j is right adjoint to its coreflectorAdjunction.

Русский

Если j — ядроотражатель (coreflective), то coreflector j является правым сопряжённым к coreflectorAdjunction.

LaTeX

$$$\\text{coreflector j} \\\\dashv\\; j$$$

Lean4

instance [Coreflective j] : (coreflector j).IsRightAdjoint :=
  ⟨_, ⟨coreflectorAdjunction j⟩⟩

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

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

Разделы

Аффилиация

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