instIsRightAdjointOfReflective

Mathlib.CategoryTheory.Adjunction.Reflective

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

English

If i is a reflective functor, then i is a right adjoint to its reflector; i.e. reflector i ⊣ i.

Русский

Если i — отражательный функционор, то i является правым сопряжённым к своему отражателю; то есть reflector i ⊣ i.

LaTeX

$$$\\mathrm{reflector(i)} \\dashv i$$$

Lean4

instance [Reflective i] : i.IsRightAdjoint :=
  ⟨_, ⟨reflectorAdjunction i⟩⟩

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

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

Разделы

Аффилиация

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