map_epi

Mathlib.CategoryTheory.Functor.EpiMono

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

English

If F preserves epimorphisms, then epi maps are preserved by F.

Русский

Если F сохраняет эпиморфизмы, то отображения эпи сохраняются F.

LaTeX

$$EpiPreserves := [F PreservesEpimorphisms] → [Epi f] ⇒ [Epi (F.map f)]$$

Lean4

instance map_epi (F : C ⥤ D) [PreservesEpimorphisms F] {X Y : C} (f : X ⟶ Y) [Epi f] : Epi (F.map f) :=
  PreservesEpimorphisms.preserves f

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

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

Разделы

Аффилиация

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