preservesMonomorphisms_of_isRightAdjoint

Mathlib.CategoryTheory.Functor.EpiMono

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

← MathLib Explorer

English

If F is left adjoint, then F preserves epimorphisms.

Русский

Если F является левым продолжением адъюнкции, то F сохраняет эпиморфизмы.

LaTeX

$$PreservesEpimorphisms F$$

Lean4

instance (priority := 100) preservesMonomorphisms_of_isRightAdjoint (F : C ⥤ D) [IsRightAdjoint F] :
    PreservesMonomorphisms F :=
  preservesMonomorphisms_of_adjunction (Adjunction.ofIsRightAdjoint F)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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