instIsLeftAdjointReflector

Mathlib.CategoryTheory.Adjunction.Reflective

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

English

If i is reflective, the reflector functor reflector i is left adjoint to i.

Русский

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

LaTeX

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

Lean4

instance [Reflective i] : (reflector i).IsLeftAdjoint :=
  ⟨_, ⟨reflectorAdjunction i⟩⟩

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

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

Разделы

Аффилиация

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