final_of_isRightAdjoint

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.final_of_isRightAdjoint

English

If F has a Right Adjunction, then F is final.

Русский

Если у f есть правая смежность, то f — финальный функтор.

LaTeX

$$$$ \text{IsRightAdjoint}(F) \Rightarrow \operatorname{Final}(F). $$$$

Lean4

instance (priority := 100) final_of_isRightAdjoint (F : C ⥤ D) [IsRightAdjoint F] : Final F :=
  final_of_adjunction (Adjunction.ofIsRightAdjoint F)

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

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

Разделы

Аффилиация

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