reflectsEpimorphisms_of_faithful

Mathlib.CategoryTheory.Functor.EpiMono

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

← MathLib Explorer

English

If F is faithful, then F reflects epimorphisms.

Русский

Если F верный, тогда F отражает эпиморфизмы.

LaTeX

$$ReflectsEpimorphisms F$$

Lean4

instance (priority := 100) reflectsEpimorphisms_of_faithful (F : C ⥤ D) [Faithful F] : ReflectsEpimorphisms F where
  reflects {X} {Y} f
    _ := ⟨fun {Z} g h hgh => F.map_injective ((cancel_epi (F.map f)).1 (by rw [← F.map_comp, hgh, F.map_comp]))⟩

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

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

Разделы

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

Аффилиация

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